×

zbMATH — the first resource for mathematics

Formalization and implementation of modern SAT solvers. (English) Zbl 1187.68557
Summary: Most, if not all, state-of-the-art complete SAT solvers are complex variations of the DPLL procedure described in the early 1960’s. Published descriptions of these modern algorithms and related data structures are given either as high-level state transition systems or, informally, as (pseudo) programming language code. The former, although often accompanied with (informal) correctness proofs, are usually very abstract and do not specify many details crucial for efficient implementation. The latter usually do not involve any correctness argument and the given code is often hard to understand and modify. This paper aims to bridge this gap by presenting SAT solving algorithms that are formally proved correct and also contain information required for efficient implementation. We use a tutorial, top-down, approach and develop a SAT solver, starting from a simple design that is subsequently extended, step-by-step, with a requisite series of features. The heuristic parts of the solver are abstracted away, since they usually do not affect solver correctness (although they are very important for efficiency). All algorithms are given in pseudo-code and are accompanied with correctness conditions, given in Hoare logic style. The correctness proofs are formalized within the Isabelle theorem proving system and are available in the extended version of this paper. The given pseudo-code served as a basis for our SAT solver argo-sat.

MSC:
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68Q60 Specification and verification (program logics, model checking, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Barrett, C.: Checking validity of quantifier-free formulas in combinations of first-order theories. Ph.D. thesis, Stanford University (2003)
[2] Biere, A.: PicoSAT essentials. JSAT 4, 75–97 (2008)
[3] Bordeaux, L., Hamadi, Y., Zhang, L.: Propositional satisfiability and constraint programming: a comparative survey. ACM Comput. Surv. 38(4) (2006)
[4] Beame, P., Kautz, H., Sabharwal, A.: Towards understanding and harnessing the potential of clause learning. JAIR 22, 319–351 (2004) · Zbl 1080.68651
[5] Baptista, L., Marques-Silva, J.P.: Using randomization and learning to solve hard real-world instances of satisfiability. In: CP ’00. LNCS 1894, pp. 489–494, Singapore, 18–22 September 2000 · Zbl 1044.68736
[6] Bayardo, R.J. Jr., Schrag, R.C.: Using CSP look-back techniques to solve real-world SAT instances. In: 14th AAAI, pp. 203–208, Providence, 27–31 July 1997
[7] Cook, S.A.: The complexity of theorem-proving procedures. In: 3rd STOC, pp. 151–158. ACM, New York (1971) · Zbl 0253.68020
[8] Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5(7), 394–397 (1962) · Zbl 0217.54002 · doi:10.1145/368273.368557
[9] Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201–215 (1960) · Zbl 0212.34203 · doi:10.1145/321033.321034
[10] Een, N., Sorensson, N.: An extensible SAT solver. In: Ligure, S.M. (ed.) SAT ’03. LNCS 2919, pp. 502–518. Springer, New York (2003)
[11] Gomes, C.P., Kautz, H., Sabharwal, A., Selman, B.: Satisfiability solvers. In: Handbook of Knowledge Representation. Elsevier, Amsterdam (2007)
[12] Goldberg, E., Novikov, Y.: Berkmin: a rast and robust SAT solver. In: DATE’02, pp. 142–149. Paris (2002)
[13] Gomes, C., Selman, B., Kautz, H.: Boosting combinatorial search through randomization. In: 15th AAAI, pp. 431–437, Madison, 26–30 July 1998
[14] Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969) · Zbl 0179.23105 · doi:10.1145/363235.363259
[15] Huang, J.: A case for simple SAT solvers. In: CP ’07. LNCS 4741, pp. 839–846, Providence, September 2007
[16] Huang, J.: The effect of restarts on the efficiency of clause learning. In: IJCAI ’07, pp. 2318–2323, Hyderabad, 6–12 January 2007
[17] Krstić, S., Goel, A.: Architecting solvers for SAT modulo theories: Nelson-Oppen with DPLL. In: FroCos ’07. LNCS 4720, pp. 1–27, Liverpool, 10–12 September 2007 · Zbl 1148.68466
[18] Marić, F.: SAT solver verification. The archive of formal proofs. http://afp.sf.net/entries/SATSolverVerification.shtml (2008)
[19] Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: DAC ’01, pp. 530–535, Las Vegas, 18–22 June 2001
[20] Marques-Silva, J.P.: The impact of branching heuristics in propositional satisfiability algorithms. In: EPIA ’99. LNCS 1695, pp. 62–74, Évora, September 1999
[21] Marques-Silva, J.P., Sakallah, K.A.: Grasp: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506–521 (1999) · Zbl 01935259 · doi:10.1109/12.769433
[22] Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53(6), 937–977 (2006) · Zbl 05426573 · doi:10.1145/1217856.1217859
[23] Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL–A Proof Assistant for Higher-Order Logic, LNCS 2283. Springer, New York (2002) · Zbl 0994.68131
[24] Pipatsrisawat, K., Darwiche, A.: A lightweight component caching scheme for satisfiability solvers. In: SAT ’07. LNCS 4501, pp. 294–299, Lisbon, May 2007
[25] Marques Silva, J.P., Sakallah, K.A.: Conflict analysis in search algorithms for satisfiability. In: 8th ICTAI, pp. 467–469, Toulouse, 16–19 November 1996
[26] Wiedijk, F.: Comparing mathematical provers. In: MKM 03. LNCS 2594, pp. 188–202, Bertinoro, February 2003 · Zbl 1022.68623
[27] Zhang, H.: SATO: an efficient propositional prover. In: CADE-14. LNCS 1249, pp. 272–275, Townsville (1997)
[28] Zhang, L., Malik, S.: The quest for efficient Boolean satisfiability solvers. In: CAV ’02. LNCS 2404, pp. 17–36, Copenhagen (2002) · Zbl 1010.68530
[29] Zhang, L., Malik, S.: Validating SAT solvers using independent resolution-based checker. In: DATE ’03, pp. 10880–10885, Münich (2003)
[30] Zhang, L., Madigan, C.F., Moskewicz, M.H., Malik, S.: Efficient conflict driven learning in a Boolean satisfiability solver. In: ICCAD ’01, pp. 279–285, San Jose (2001)
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.