SAT-Solving Based on Boundary Point Elimination
Eugene Goldberg and Panagiotis Manolios. HVC: Haifa Verification Conference, © Springer
We study the problem of building structure-aware
SAT-solvers based on resolution. In this study, we use the idea of treating
a resolution proof as a process of Boundary Point Elimination (BPE).
We identify two problems of using SAT-algorithms with Conflict Driven
Clause Learning (CDCL) for structure-aware SAT-solving. We introduce
a template of resolution based SAT-solvers called BPE-SAT that is based
on a few generic implications of the BPE concept. BPE-SAT can be
viewed as a generalization of CDCL SAT-solvers and is meant for building new structure-aware SAT-algorithms. We give experimental results
substantiating the ideas of the BPE approach. In particular, to show the
importance of structural information we compare an implementation of
BPE-SAT and state-of-the-art SAT-solvers on narrow CNF formulas.
PDF (242K) © Springer