Formalizing CNF SAT Symmetry Breaking in PVS

被引：1

作者：

Narvaez, David E. ^{[1
]}

机构：

[1] Rochester Inst Technol, Golisano Coll Comp & Informat Sci, Rochester, NY 14623 USA

来源：

NASA FORMAL METHODS (NFM 2019) | 2019年 / 11460卷

关键词：

SAT; PVS; Symmetry breaking; SATISFIABILITY; VERIFICATION; SOLVER;

D O I：

10.1007/978-3-030-20652-9_23

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

The Boolean satisfiability problem (SAT) remains a central problem to theoretical as well as practical computer science. Recently, the need to trust the results obtained by SAT solvers has led to research in formalizing these. Nevertheless, tools in the ecosystem of SAT problems (such as preprocessors, model counters, etc.) would need to be verified as well in order for the results to be trusted. In this paper we explore a step towards a formalized symmetry breaking tool for SAT: formalizing SAT symmetry breaking for formulas in conjunctive normal form (CNF) using the Prototype Verification System (PVS).

引用

页码：341 / 354

页数：14

共 16 条

[1] Efficient symmetry breaking for Boolean satisfiability [J].

Aloul, FA ;

Sakallah, KA ;

Markov, IL .

IEEE TRANSACTIONS ON COMPUTERS, 2006, 55 (05) :549-558

[2] Solving difficult instances of Boolean satisfiability in the presence of symmetry [J].

Aloul, FA ;

Ramani, A ;

Markov, IL ;

Sakallah, KA .

IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2003, 22 (09) :1117-1137

[3] A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality [J].

Blanchette, Jasmin Christian ;

Fleury, Mathias ;

Lammich, Peter ;

Weidenbach, Christoph .

JOURNAL OF AUTOMATED REASONING, 2018, 61 (1-4) :333-365

[4]

Cook S. A., 1971, Proceedings of the 3rd annual ACM symposium on theory of computing, P151

[5]

Crawford J, 1996, MOR KAUF R, P148

[6]

Crawford JamesM., 1992, AAAI Workshop on Tractable Reasoning, P17

[7] On local domain symmetry for model expansion [J].

Devriendt, Jo ;

Bogaerts, Bart ;

Bruynooghe, Maurice ;

Denecker, Marc .

THEORY AND PRACTICE OF LOGIC PROGRAMMING, 2016, 16 :636-652

[8] Improved Static Symmetry Breaking for SAT [J].

Devriendt, Jo ;

Bogaerts, Bart ;

Bruynooghe, Maurice ;

Denecker, Marc .

THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2016, 2016, 9710 :104-122

[9]

Heule Marijn J. H., 2016, 2016 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), P149, DOI 10.1109/SYNASC.2016.034

[10] The Science of Brute Force [J].

Heule, Marijn J. H. ;

Kullmann, Oliver .

COMMUNICATIONS OF THE ACM, 2017, 60 (08) :70-79

← 1 2 →