 |
Equi-propagation for Optimized SAT Encoding
Amit Metodi, Michael Codish, Vitaly Lagoon and Peter Stuckey
Proceedings of CP 2011;
2011
Abstract:
We present an approach to propagation based SAT encoding, Boolean equi-propagation, where constraints are modelled as Boolean functions which propagate information about equalities between Boolean literals. This information is then applied as a form of partial evaluation to simplify constraints prior to their encoding as CNF formulae. We demonstrate for a variety of benchmarks that our approach leads to a considerabe reduction in the size of CNF encodings and subsequent speed-ups in SAT solving times.Available: bibtex entry
Related sites: available on arxiv
Michael Codish
The Department of Computer Science
Ben-Gurion University of the Negev
PoB 653, Beer-Sheva, 84105, Israel
mcodish@cs.bgu.ac.il