Boolean Equi-propagation for Optimized SAT Encoding
Artificial Intelligence
2015-03-19 v1 Data Structures and Algorithms
Logic in Computer Science
Abstract
We present an approach to propagation based solving, Boolean equi-propagation, where constraints are modelled as propagators of information about equalities between Boolean literals. Propagation based solving applies this information as a form of partial evaluation resulting in optimized SAT encodings. We demonstrate for a variety of benchmarks that our approach results in smaller CNF encodings and leads to speed-ups in solving times.
Keywords
Cite
@article{arxiv.1104.4617,
title = {Boolean Equi-propagation for Optimized SAT Encoding},
author = {Amit Metodi and Michael Codish and Vitaly Lagoon and Peter J. Stuckey},
journal= {arXiv preprint arXiv:1104.4617},
year = {2015}
}