zbMATH — the first resource for mathematics

Extending clause learning of SAT solvers with Boolean Gröbner bases. (English) Zbl 1290.68141
Gerdt, Vladimir P. (ed.) et al., Computer algebra in scientific computing. 12th international workshop, CASC 2010, Tsakhkadzor, Armenia, September 6–12, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-15273-3/pbk). Lecture Notes in Computer Science 6244, 293-302 (2010).
Summary: 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.
For the entire collection see [Zbl 1195.68004].

68W30 Symbolic computation and algebraic computation
68Q32 Computational learning theory
Redlog; MiniSAT
Full Text: DOI
[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) · Zbl 05187221
[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) · Zbl 1247.68247
[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) · Zbl 0985.68038
[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)
[5] Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Communications of the ACM 5(7), 394–397 (1962) · Zbl 0217.54002
[6] Buchberger, B.: Ein Algorithmus zum Auffinden der Basiselemente des Restklassenringes nach einem nulldimensionalen Polynomideal. PhD thesis, Universität Innsbruck (1965) · Zbl 1245.13020
[7] Kapur, D., Narendran, P.: An equational approach to theorem proving in first-order predicate calculus. ACM SIGSOFT Notes 10(4), 63–66 (1985)
[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) · Zbl 1183.68568
[9] Van Gelder, A.: Combining preorder and postorder resolution in a satisfiability solver. Electronic Notes in Discrete Mathematics 9, 115–128 (2001) · Zbl 0990.90534
[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)
[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) · Zbl 1186.68576
[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) · Zbl 1165.03312
[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)
[14] Beame, P., Kautz, H., Sabharwal, A.: Towards understanding and harnessing the potential of clause learning. JAIR 22(1), 319–351 (2004) · Zbl 1080.68651
[15] Stone, M.H.: The theory of representations for boolean algebras. Transactions of the American Mathematical Society 40, 37–111 (1936) · Zbl 0014.34002
[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) · Zbl 1164.68019
[17] Küchlin, W.: Canonical hardware representation using Gröbner bases. In: Proceedings of the A3L 2005, Passau, Germany, pp. 147–154 (2005)
[18] Becker, T., Weispfenning, V.: Gröbner Bases: A Computational Approach to Commutative Algebra. Springer, New York (1993) · Zbl 0772.13010
[19] Cox, D., Little, J., O’Shea, D.: Ideals, Varieties, and Algorithms, 3rd edn. Springer, New York (2007)
[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) · Zbl 1204.68191
[21] Dolzmann, A., Sturm, T.: Redlog: Computer algebra meets computer logic. ACM SIGSAM Bulletin 31(2), 2–9 (1997)
[22] Sturm, T., Zengler, C.: Parametric quantified SAT solving. In: Proceedings of the ISSAC 2010. ACM, New York (2010) · Zbl 1321.68322
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.