Equi-propagation for Optimized SAT Encoding

Amit Metodi, Michael Codish, Vitaly Lagoon and Peter Stuckey   

Proceedings of CP 2011; 2011


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

© copyright notice