×

zbMATH — the first resource for mathematics

Exploiting the real power of unit propagation lookahead. (English) Zbl 0990.90538
Kautz, Henry (ed.) et al., LICS 2001 workshop on theory and application of satisfiability testing (SAT 2001). Boston, MA, USA, June 14-15, 2001. Amsterdam: Elsevier, Electron. Notes Discrete Math. 9, no pag., electronic only (2001).
Summary: One of the best SAT solvers for random 3-SAT formulas, SATZ, is based on a heuristic called unit propagation lookahead (UPL). Unfortunately, it does not perform so well on specific structured instances, especially on the ones coming from an area where a huge interest for SAT has emerged in recent years: symbolic model checking (SMC). We claim that all the power of this heuristic is not used in SATZ, and that UPL can be extended to solve some real world structured problems, where the major competitors are using intelligent backtracking or specific deduction rules. We introduce a preprocessing technique that can be applied to simplify instances containing equivalent literals. This technique is based on UPL, so it can be easily added to any solver using this heuristic. We compare our approach to the new extension of SATZ for equivalency reasoning (EqSATZ) and another approach, the Stalmarck method, which is mainly used in SMC.
For the entire collection see [Zbl 0968.90001].

MSC:
90C27 Combinatorial optimization
Software:
Chaff; DIMACS; SatEx; SATO; Walksat
PDF BibTeX XML Cite
References:
[1] Davis, M.; Logemann, G.; Lovelan, D.: A machine program for theorem proving, communications of the ACM. 5, 394-397 (1962) · Zbl 0217.54002
[2] O. Dubois, P. André, Y. Boufkhad, J. Carlier, SAT versus UNSAT, in: Johnson and Trick [28], pp. 415-436. · Zbl 0864.90090
[3] Freema, J. W.: Improvements to prepositional satisfiability search algorithms, ph.d. Thesis, departement of computer and information science. (1995)
[4] Li, C. -M.; Anbulagan: Heuristics based on unit propagation for satisfiability problems, in: Proceedings of the fifteenth international joint conference on artificial intelligence (IJCAI’97). Nagoya (JAPAN), 366-371 (1997)
[5] Li, C. -M.: A constrained based approach to narrow search trees for satisfiability. Information processing letters 71, 75-80 (1999) · Zbl 1015.68518
[6] Zhan, H.: Sato: an efficient prepositional prover. Proceedings of the international conference on automated deduction (CADE’97), volume 1249 of LNAI, 272-275 (1997)
[7] Bayardo, R. J. J.; Schra, R. C.: Using CSP look-back techniques to solve real-world SAT instances. Proceedings of the fourteenth national conference on artificial intelligence (AAAI’97), providence, rhode island, 203-208 (1997)
[8] Marques-Silva, J. P.; Sakalla, K. A.: GRASP - A new search algorithm for satisfiability. Proceedings of IEEE/ACM international conference on computer-aided design, 220-227 (1996)
[9] Moskewicz, M. W.; Madigan, C. F.; Zhao, Y.; Zhang, L.; Mali, S.: Chaff: engineering an efficient SAT solver. Proceedings of the 38th design automation conference (DAC’01) (2001)
[10] J. F. Groote, J. P. Warners, The prepositional formula checker HeerHugo, in: Gent et al. [29], pp. 261-281. · Zbl 0979.68088
[11] Li, C. -M.: Integrating equivalency reasoning into Davis-Putnam procedure. Proceedings of AAAI’2000, 291-296 (2000)
[12] Selman, B.; Kautz, H. A.; Mcalleste, D. A.: Ten challenges in prepositional reasoning and search. Proceedings of the fifteenth international joint conference on artificial intelligence (IJCAI’97), 50-54 (1997)
[13] Warners, J. P.; Van-Maare, H.: A two phase algorithm for solving a class of hard satisfiability problems. Operations research letters 23, 81-88 (1998) · Zbl 0960.90100
[14] Stålmarck, G.: A system for determining prepositional logic theorems by applying values and rules to triplets that are generated from a formula, tech. Rep., European patent N 0403 454 (1995), US patent N 5 276 897. Swedish patent N 467 076 (1989) (1989)
[15] Harriso, J.: Stålmarck’s method as a HOL derived rule. Proceedings of the 9th international conference on theorem proving in higher order logics (TPHOLs’96), volume 1125 of lecture note in computer science, Finland, 221-234 (1996)
[16] Biere, A.; Cimatti, A.; Clarke, E. M.; Zh, Y.: Symbolic model checking without bdds, in: Proceedings of tools and algorithms for the analysis and construction of systems (TACAS’99), number 1579 in LNCS. (1999)
[17] Abdulla, P. A.; Bjesse, P.; Eén, N.: Symbolic reachability analysis based on SAT-solvers, in: Proceedings of the 6th international conference on tools and algorithms for the construction and analysis of systems (TACAS’2000). (2000) · Zbl 0971.68633
[18] L. Simon, P. Chatalic, SATEx: a Web-based Framework for SAT Experimentation, in: Proceedings of the Workshop on Theory and Applications of Satisfiability Testing (SAT2001) [30], http://www.lri.fr/simon/satex/satex.php3. · Zbl 0990.90549
[19] Davis, M.; Putna, H.: A computing procedure for quantification theory, journal of the ACM. 7, 201-215 (1960) · Zbl 0212.34203
[20] B. Jurkowiak, C.-M. Li, G. Utard, Parallelizing SATZ Using Dynamic Workload Balancing, in: Proceedings of the Workshop on Theory and Applications of Satisfiability Testing (SAT2001) [30], to appear. · Zbl 1086.68118
[21] C. P. Gomes, B. Selman, N. Crato, H. Kautz, Heavy-Taily Phenomena in Satisfiability, in: Gent et al. [29], pp. 15-41. · Zbl 0979.68049
[22] B. Selman, H. Kautz, B. Cohen, Local search strategies for satisfiability testing, in: Johnson and Trick [28], pp. 521-532. URL http://www.cs.Cornell.edu/home/selman/papers-ftp/96.dimacs.walksat.ps · Zbl 0864.90093
[23] Marques-Silva, J. P.; Glas, T.: Combinational equivalence checking using satisfiability and recursive learning. Proceedings of the IEEE/ACM design, automation and test in Europe conference (1999)
[24] Brafma, R. I.: A simplifier for prepositional formulas with many binary clauses. (2001)
[25] Aspvall, B.; Plass, M.; Tarja, R.: A linear-time algorithm for testing the truth of certain quantified Boolean formulas. Information processing letters 8, 121-123 (1979) · Zbl 0398.68042
[26] Marques-Silv, J. P.: Algebraic simplification techniques for prepositional satisfiability, in: Proceedings of the 6th international conference on principles and practice of constraint programming (CP’2000). (2000)
[27] Audemard, G.; Benhamou, B.; Siege, P.: AVAL: an enumerative method for SAT. Proceedings of the first international conference on computational logic (CL’00), londres, 373-383 (2000) · Zbl 0983.68530
[28] Johnson, D.; Trick, M.: Second DIMACS implementation challenge : cliques, coloring and satisfiability, vol. 26 of DIMACS series in discrete mathematics and theoretical computer science, American mathematical society. 26 (1996) · Zbl 0875.68678
[29] Gent, I.; Van Maaren, H.; Walsh, T.: SAT20000: highlights of satisfiability research in the year 2000, frontiers in artificial intelligence and applications. (2000) · Zbl 0963.00028
[30] Proceedings of the Workshop on Theory and Applications of Satisfiability Testing (SAT2001), to appear. URL http://www.cs.Washington.edu/homes/kautz/sat2001/
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.