SAT-Solving Based on Boundary Point Elimination
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.
KeywordsBoundary Point Equivalence Check Satisfying Assignment Partial Assignment Complete Assignment
Unable to display preview. Download preview PDF.
- 7.Dechter, R., Rish, I.: Directional resolution: The davis-putnam procedure, revisited. In: KR, pp. 134–145 (1994)Google Scholar
- 10.Marques-Silva, J., Sakallah, K.: Grasp—a new search algorithm for satisfiability. In: ICCAD 1996, Washington, DC, USA, pp. 220–227 (1996)Google Scholar
- 11.Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient sat solver. In: DAC 2001, New York, NY, USA, pp. 530–535 (2001)Google Scholar
- 12.Williams, R., Gomes, C.P., Selman, B.: Backdoors to typical case complexity. In: IJCAI, pp. 1173–1178 (2003)Google Scholar
- 13.Zhang, L., Malik, S.: Conflict driven learning in a quantified boolean satisfiability solver. In: ICCAD, pp. 442–449 (2002)Google Scholar