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.

• Type: Journal
• Year: 2015
• Where: CADE
• Authors: Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler
• Keywords: CADE 2015, Logical Reasoning