Equi-propagation for Optimized SAT Encoding
Proceedings of CP 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
The Department of Computer Science
Ben-Gurion University of the Negev
PoB 653, Beer-Sheva, 84105, Israel