Expressing Symmetry Breaking in Propositional Proofs
Marijn Heule
ACL2 Seminar, Nov. 2, 2015

An effective preprocessing technique used in satisfiability solvers is
the addition of symmetry-breaking predicates, i.e., auxiliary clauses
that guide a solver away from needless exploration of isomorphic
sub-problems. Although symmetry-breaking predicates have been in use
for over a decade, it was not known how to express them in proofs of
unsatisfiability. Consequently, results obtained by symmetry breaking
cannot be validated by existing proof checkers.  We present a method
to express symmetry-breaking predicates in DRAT, a format for
propositional proofs that is supported by the top-tier solvers. We
applied this method to generate proofs of problems that have not been
solved without symmetry-breaking predicates. We validated these proofs
with both an ACL2-based, mechanically-verified checker and the SAT
Competition 2014 proof-checking tool.