SAT-solving based on boundary point elimination

Abstract

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. © 2011 Springer-Verlag Berlin Heidelberg.