Boolean Equi-propagation for Optimized SAT Encoding
Boolean Equi-propagation for Optimized SAT Encoding
复制标题
用于优化 SAT 编码的布尔等传播
DOI：
10.1007/978-3-642-23786-7_47
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
Peter James Stuckey
中科院分区：
文献类型：
--
作者：
Amit Metodi;M. Codish;Vitaly Lagoon;Peter James Stuckey
我们提出了一种基于传播的SAT编码方法，布尔等传播，其中约束被建模为布尔函数，传播布尔文字之间的相等信息。然后，将此信息作为部分评估的形式应用于简化约束，然后将其编码为CNF公式。我们证明了各种基准测试，我们的方法导致相当大的减少CNF编码的大小和随后的SAT求解时间的加速。
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 considerable reduction in the size of CNF encodings and subsequent speed-ups in SAT solving times.