Advertisement

SAT-Solving Based on Boundary Point Elimination

  • Eugene Goldberg
  • Panagiotis Manolios
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6504)

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.

Keywords

Boundary Point Equivalence Check Satisfying Assignment Partial Assignment Complete Assignment 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Alekhnovich, M., Razborov, A.: Resolution is not automatizable unless w[p] is tractable. SIAM J. Comput. 38(4), 1347–1363 (2008)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I ch. 2, pp. 19–99. North-Holland, Amsterdam (2001)CrossRefGoogle Scholar
  3. 3.
    Berman, L.: Circuit width, register allocation, and ordered binary decision diagrams. IEEE Trans. on CAD of Integr. Circ. and Syst. 10(8), 1059–1066 (1991)CrossRefGoogle Scholar
  4. 4.
    Biere, A.: Picosat essentials. JSAT 4(2-4), 75–97 (2008)zbMATHGoogle Scholar
  5. 5.
    Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Communications of the ACM 5(7), 394–397 (1962)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM 7(3), 201–215 (1960)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Dechter, R., Rish, I.: Directional resolution: The davis-putnam procedure, revisited. In: KR, pp. 134–145 (1994)Google Scholar
  8. 8.
    Goldberg, E.: Boundary points and resolution. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 147–160. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  9. 9.
    Pipatsrisawat, K., Darwiche, A.: On the power of clause-learning SAT solvers with restarts. In: Gent, I.P. (ed.) CP 2009. LNCS, vol. 5732, pp. 654–668. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  10. 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. 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. 12.
    Williams, R., Gomes, C.P., Selman, B.: Backdoors to typical case complexity. In: IJCAI, pp. 1173–1178 (2003)Google Scholar
  13. 13.
    Zhang, L., Malik, S.: Conflict driven learning in a quantified boolean satisfiability solver. In: ICCAD, pp. 442–449 (2002)Google Scholar
  14. 14.

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Eugene Goldberg
    • 1
  • Panagiotis Manolios
    • 1
  1. 1.Northeastern UniversityUSA

Personalised recommendations