Extending Clause Learning of SAT Solvers with Boolean Gröbner Bases

  • Christoph Zengler
  • Wolfgang Küchlin
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6244)


We extend clause learning as performed by most modern SAT Solvers by integrating the computation of Boolean Gröbner bases into the conflict learning process. Instead of learning only one clause per conflict, we compute and learn additional binary clauses from a Gröbner basis of the current conflict. We used the Gröbner basis engine of the logic package Redlog contained in the computer algebra system Reduce to extend the SAT solver MiniSAT with Gröbner basis learning. Our approach shows a significant reduction of conflicts and a reduction of restarts and computation time on many hard problems from the SAT 2009 competition.


Computer Algebra System Conjunctive Normal Form Decision Node Unit Clause Bound Model Check 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Lynce, I., Marques da Silva, J.P.: SAT in bioinformatics: Making the case with haplotype inference. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 136–141. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  2. 2.
    Bonet, M.L., John, K.S.: Efficiently calculating evolutionary tree measures using SAT. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 4–17. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  3. 3.
    Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods in System Design 19(1), 7–34 (2001)CrossRefzbMATHGoogle Scholar
  4. 4.
    Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. In: Zelkowitz, M. (ed.) Highly Dependable Software. Advances in Computers, vol. 58. Academic Press, San Diego (2003)Google 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.
    Buchberger, B.: Ein Algorithmus zum Auffinden der Basiselemente des Restklassenringes nach einem nulldimensionalen Polynomideal. PhD thesis, Universität Innsbruck (1965)Google Scholar
  7. 7.
    Kapur, D., Narendran, P.: An equational approach to theorem proving in first-order predicate calculus. ACM SIGSOFT Notes 10(4), 63–66 (1985)CrossRefGoogle Scholar
  8. 8.
    Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam (2009)zbMATHGoogle Scholar
  9. 9.
    Van Gelder, A.: Combining preorder and postorder resolution in a satisfiability solver. Electronic Notes in Discrete Mathematics 9, 115–128 (2001)CrossRefzbMATHGoogle Scholar
  10. 10.
    Bacchus, F.: Enhancing davis putnam with extended binary clause reasoning. In: 18th National Conference on Artificial Intelligence, pp. 613–619. AAAI Press, Menlo Park (2002)Google Scholar
  11. 11.
    Condrat, C., Kalla, P.: A gröbner basis approach to CNF-formulae preprocessing. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 618–631. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  12. 12.
    Dershowitz, N., Hsiang, J., Huang, G.S., Kaiss, D.: Boolean rings for intersection-based satisfiability. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 482–496. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  13. 13.
    Seidl, A.M., Sturm, T.: Boolean quantification in a first-order context. In: Proceedings of the CASC 2003. Institut für Informatik, Technische Universität München, Garching, pp. 329–345 (2003)Google Scholar
  14. 14.
    Beame, P., Kautz, H., Sabharwal, A.: Towards understanding and harnessing the potential of clause learning. JAIR 22(1), 319–351 (2004)MathSciNetzbMATHGoogle Scholar
  15. 15.
    Stone, M.H.: The theory of representations for boolean algebras. Transactions of the American Mathematical Society 40, 37–111 (1936)MathSciNetzbMATHGoogle Scholar
  16. 16.
    Brickenstein, M., Dreyer, A., Greuel, G.M., Wedler, M.: New developments in the theory of gröbner bases and applications to formal verification. Journal of Pure and Applied Algebra 213, 1612–1635 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Küchlin, W.: Canonical hardware representation using Gröbner bases. In: Proceedings of the A3L 2005, Passau, Germany, pp. 147–154 (2005)Google Scholar
  18. 18.
    Becker, T., Weispfenning, V.: Gröbner Bases: A Computational Approach to Commutative Algebra. Springer, New York (1993)CrossRefzbMATHGoogle Scholar
  19. 19.
    Cox, D., Little, J., O’Shea, D.: Ideals, Varieties, and Algorithms, 3rd edn. Springer, New York (2007)CrossRefzbMATHGoogle Scholar
  20. 20.
    Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  21. 21.
    Dolzmann, A., Sturm, T.: Redlog: Computer algebra meets computer logic. ACM SIGSAM Bulletin 31(2), 2–9 (1997)CrossRefGoogle Scholar
  22. 22.
    Sturm, T., Zengler, C.: Parametric quantified SAT solving. In: Proceedings of the ISSAC 2010. ACM, New York (2010)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2010

Authors and Affiliations

  • Christoph Zengler
    • 1
  • Wolfgang Küchlin
    • 1
  1. 1.Symbolic Computation Group, W. Schickard-Institute for InformaticsUniversität TübingenGermany

Personalised recommendations