The Quest for Efficient Boolean Satisfiability Solvers (Презентации лекций), страница 6

In [42], the authors propose the use of ZBDDs to represent clauses in aresolution-based solver and utilize the compression power of decision diagrams tocontrol the memory blowup. Their experiment shows that for certain classes of SATproblems, the resolution-based approach shows very good results.Stalmärck’s algorithm [9] is a patented proprietary algorithm for solving SAT.Stalmärck’s algorithm use breath-first search in contrast to the depth-first searchemployed by DPLL. There are commercial implementations of SAT solvers based onthis algorithm [50]. HeerHugo [51] is a publicly available solver that claims to beusing an algorithm similar to the Stalmärk’s algorithm.Another approach is to use stochastic algorithms.

Stochastic algorithms cannotprove a SAT instance to be unsatisfiable. However, for some hard satisfiableinstances, stochastic methods may find solutions very quickly. Currently, two of themore successful approaches to the stochastic method are random walk basedalgorithms such as walksat [7] and Discrete Lagrangian-Based global search methodssuch as DLM [52].For more about other SAT solving techniques, we refer the readers to a survey[10].5. Conclusions and Future WorksIn this paper, we briefly discussed some of the techniques employed in modernBoolean Satisfiability solvers. In particular, we concentrated on the procedure basedon the DPLL search algorithm.

In recent years, SAT solvers based on DPLL searchhave made phenomenal progress. Efficient SAT solvers such as Chaff [20] aredeployed in industrial strength applications for hardware verification and debugging.In these environments, the SAT solver routinely encounters instances with thousandsor even millions of variables. Therefore, it is of great importance to increase thecapacity and efficiency of the SAT solver.Even though researchers have been working on SAT engines for quite a long time,there is still a lot of work that remains to be done. First of all, the overallunderstanding of SAT instances is still quite limited.

For example, though there existsome rough ideas about the difficulty of SAT problems (e.g. [53, 54]), it is still notclear how can we estimate the hardness of a given problem without actually solving it.Experimental evaluation of different SAT solving algorithms is more like an art than ascience because it is easy to tune a solver to a given set of benchmarks, but theparameters may not work for the same benchmarks with some simple permutation(e.g.[55]). On the application side, currently most of the applications use SAT solversas blackboxes and no interaction is possible between the applications and the SATsolvers. Application specific knowledge can help a lot in the solving process asdemonstrated in [56].

For a particular application, custom implementation of a SATsolver may also be helpful (e.g. [57]). All in all, we believe there are still manyresearch topics to be explored. As more and more applications utilize SAT solvers asdeduction and reasoning engine, we believe many new algorithms will emerge andpush the envelope for efficient implementations even further.AcknowledgmentsThe authors would like to thank Dr. Aarti Gupta for suggestions and help inimproving the paper.6.

References[1] S. A. Cook, "The complexity of theorem-proving procedures," presented at Third AnnualACM Symposium on Theory of Computing, 1971.[2] H. Kautz and B. Selman, "Planning as Satisfiability," presented at European Conference onArtificial Intelligence(ECAI-92), 1992.[3] P. Stephan, R. Brayton, and A. Sangiovanni-Vencentelli, "Combinational Test GenerationUsing Satisfiability," IEEE Transactions on Computer-Aided Design of Integrated Circuitsand Systems, vol. 15, pp.

1167-1176, 1996.[4] D. Jackson and M. Vaziri, "Finding Bugs with a Constraint Solver," presented atInternational Symposium on Software Testing and Analysis, Portland, OR, 2000.[5] M. Davis and H. Putnam, "A computing procedure for quantification theory," Journal ofACM, vol. 7, pp. 201-215, 1960.[6] M. Davis, G. Logemann, and D. Loveland, "A machine program for theorem proving,"Communications of the ACM, vol. 5, pp. 394-397, 1962.[7] B. Selman, H. Kautz, and B. Cohen, "Local Search Strategies for Satisfiability Testing," inCliques, Coloring, and Satisfiability: Second DIMACS Implementation Challenge, DIMACSSeries in Discrete Mathematics and Theoretical Computer Science, vol.

26, D. S. Johnsonand M. A. Trick, Eds.: American Methematical Society, 1996.[8] R. E. Bryant, "Graph-Based Algorithms for Boolean Function Manipulation," IEEETransactions on Computers, vol. C-35, pp. 677-691, 1986.[9] G. Stålmarck, "A system for determining prepositional logic theorems by applying valuesand rules to triplets that are generated from a formula." US Patent N 5 27689, 1995.[10] J.

Gu, P. W. Purdom, J. Franco, and B. W. Wah, "Algorithms for the Satisfiability (SAT)Problem: A Survey," in DIMACS Series in Discrete Mathematics and Theoretical ComputerScience: American Mathematical Society, 1997.[11] G.-J. Nam, K. A. Sakallah, and R. A. Rutenbar, "Satisfiability-Based Layout Revisited:Detailed Routing of Complex FPGAs Via Search-Based Boolean SAT," presented atACM/SIGDA International Symposium on Field-Programmable Gate Arrays (FPGA'99),Monterey, California, 1999.[12] A.

Biere, A. Cimatti, E. M. Clarke, and Y. Zhu, "Symbolic Model Checking withoutBDDs," presented at Tools and Algorithms for the Analysis and Construction of Systems(TACAS'99), 1999.[13] J. Crawford and L. Auton, "Experimental results on the cross-over point in satisfiabilityproblems," presented at National Conference on Artificial Intelligence (AAAI), 1993.[14] J. W. Freeman, "Improvements to Propositional Satisfiability Search Algorithms," inPh.D. Thesis, Department of Computer and Information Science: University ofPennsylvania, 1995.[15] A. V.

Gelder and Y. K. Tsuji, "Satisfiability Testing with more Reasoning and Lessguessing," in Cliques, Coloring and Satisfiability: Second DIMACS ImplementationChallenge, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, M.Trick, Ed.: American Mathematical Society, 1995.[16] O. Dubois, P. Andre, Y. Boufkhad, and J. Carlier, "SAT v.s. UNSAT," in Cliques,Coloring and Satisfiability: Second DIMACS Implementation Challenge, DIMACS Series inDiscrete Mathematics and Theoretical Computer Science, D. S.

Johnson and M. Trick, Eds.,1993.[17] J. P. Marques-Silva and K. A. Sakallah, "Conflict Analysis in Search Algorithms forPropositional Satisfiability," presented at IEEE International Conference on Tools withArtificial Intelligence, 1996.[18] R. Bayardo and R.

Schrag, "Using CSP look-back techniques to solve real-world SATinstances," presented at National Conference on Artificial Intelligence (AAAI), 1997.[19] H. Zhang, "SATO: An efficient propositional prover," presented at InternationalConference on Automated Deduction (CADE), 1997.[20] M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S.

Malik, "Chaff: Engineering anEfficient SAT Solver," presented at 39th Design Automation Conference, 2001.[21] E. Goldberg and Y. Novikov, "BerkMin: a Fast and Robust SAT-Solver," presented atDesign Automation & Test in Europe (DATE 2002), 2002.[22] C. M. Li and Anbulagan, "Heuristics based on unit propagation for satisfiabilityproblems," presented at the fifteenth International Joint Conference on Artificial Intelligence(IJCAI'97), Nagayo, Japan, 1997.[23] O. Dubois and G. Dequen, "A backbone-search heuristic for efficient solving of hard 3SAT formulae," presented at International Joint Conference on Artificial Intelligence(IJCAI), 2001.[24] D. A.

Plaisted and S. Greenbaum, "A Stucture-preserving Clause Form Translation,"Journal of Symbolic Computation, vol. 2, pp. 293-304, 1986.[25] J. P. Marques-Silva and K. A. Sakallah, "GRASP -- A New Search Algorithm forSatisfiability," presented at IEEE International Conference on Tools with ArtificialIntelligence, 1996.[26] J. P. Marques-Silva, "The Impact of Branching Heuristics in Propositional SatisfiabilityAlgorithms," presented at the 9th Portuguese Conference on Artificial Intelligence (EPIA),1999.[27] J.