Sciweavers

Share
CADE
2015
Springer

Expressing Symmetry Breaking in DRAT Proofs

4 years 7 months ago
Expressing Symmetry Breaking in DRAT Proofs
An effective SAT preprocessing technique is the addition of symmetry-breaking predicates: auxiliary clauses that guide a SAT solver away from needless exploration of isomorphic sub-problems. Symmetrybreaking predicates have been in use for over a decade. However, it was not known how to express the addition of these predicates in proofs of unsatisfiability. Hence, results obtained by symmetry breaking cannot be validated by existing proof checkers. We present a method to express the addition of symmetry-breaking predicates in DRAT, a clausal proof format supported by top-tier solvers. We applied this method to generate SAT problems that have not been previously solved without symmetrybreaking predicates. We validated these proofs with an ACL2-based, mechanically-verified DRAT proof checker and the proof-checking tool of SAT Competition 2014.
Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler
Added 17 Apr 2016
Updated 17 Apr 2016
Type Journal
Year 2015
Where CADE
Authors Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler
Comments (0)
books