This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
GRASP: A Search Algorithm for Propositional Satisfiability
May 1999 (vol. 48 no. 5)
pp. 506-521

Abstract—This paper introduces GRASP (Generic seaRch Algorithm for the Satisfiability Problem), a new search algorithm for Propositional Satisfiability (SAT). GRASP incorporates several search-pruning techniques that proved to be quite powerful on a wide variety of SAT problems. Some of these techniques are specific to SAT, whereas others are similar in spirit to approaches in other fields of Artificial Intelligence. GRASP is premised on the inevitability of conflicts during the search and its most distinguishing feature is the augmentation of basic backtracking search with a powerful conflict analysis procedure. Analyzing conflicts to determine their causes enables GRASP to backtrack nonchronologically to earlier levels in the search tree, potentially pruning large portions of the search space. In addition, by “recording” the causes of conflicts, GRASP can recognize and preempt the occurrence of similar conflicts later on in the search. Finally, straightforward bookkeeping of the causality chains leading up to conflicts allows GRASP to identify assignments that are necessary for a solution to be found. Experimental results obtained from a large number of benchmarks indicate that application of the proposed conflict analysis techniques to SAT algorithms can be extremely effective for a large number of representative classes of SAT instances.

[1] M. Abramovici, M.A. Breuer, and A.D. Friedman, Digital Systems Testing and Testable Design. Computer Science Press, 1990.
[2] P. Barth, “A Davis-Putnam Based Enumeration Algorithm for Linear Pseudo-Boolean Optimization,” Technical Report MPI-I-95-2-003, Max-Planck-Institut für Informatik, 1995.
[3] C.E. Blair, R.G. Jeroslow, and J.K. Lowe, "Some results and experiments in programming techniques for propositional logic," Computers and Operations Research, vol. 55, pp. 633-645, 1986.
[4] M. Bruynooghe, “Analysis of Dependencies to Improve the Behaviour of Logic Programs,” Proc. Fifth Conf. Automated Deduction, pp. 293-305, 1980.
[5] S.T. Chakradhar, V.D. Agrawal, and S.G. Rothweiler, "A Transitive Closure Algorithm for Test Generation," IEEE Trans. Computer-Aided Design, vol. 12, pp. 1,015-1,028, July 1993.
[6] J. Crawford and L. Auton, “Experimental Results on the Cross-Over Point in Satisfiability Problems,” Proc. 11th Nat'l Conf. Artificial Intelligence (AAAI-93), pp. 22-28, 1993.
[7] M. Davis and H. Putnam, "A Computing Procedure for Quantification Theory," J. ACM, vol. 7, July 1960, pp. 201-215.
[8] R. Dechter, “Enhancement Schemes for Constraint Processing: Backjumping, Learning, and Cutset Decomposition,” Artificial Intelligence, vol. 41, pp. 273-312, 1989/90.
[9] J. de Kleer, “An Assumption-Based tms,” Artificial Intelligence, pp. 127–162, 1986.
[10] O. Dubois, P. Andre, Y. Boufkhad, and J. Carlier, “SAT versus UNSAT,” Second DIMACS Implementation Challenge, D.S. Johnson and M.A. Trick, eds., 1993.
[11] J.W. Freeman, “Improvements to Propositional Satisfiability Search Algorithms,” PhD dissertation, Dept. of Computer and Information Science, Univ. of Pennsylvania, May 1995.
[12] G. Gallo and G. Urbani, “Algorithms for Testing the Satisfiability of Propositional Formulae,” J. Logic Programming, vol. 7, pp. 45-61, 1989.
[13] M.R. Garey and D.S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness.New York: W.H. Freeman, 1979.
[14] J. Gaschnig, “Performance Measurement and Analysis of Certain Search Algorithms,” PhD dissertation, Dept. of Computer Science, Carnegie-Mellon Univ., CMU-CS-79-124, May 1979.
[15] M.L. Ginsberg, “Dynamic Backtracking,” J. Artificial Intelligence Research, vol. 1, pp. 25-46, Aug. 1993.
[16] J. Giraldi and M.L. Bushnell, “Search State Equivalence for Redundancy Identification and Test Generation,” Proc. Int'l Test Conf., pp. 184-193, 1991.
[17] J.P. Hayes, Introduction to Digital Logic Design. Addison-Wesley, 1993.
[18] D.S. Johnson and M.A. Trick eds. Second DIMACS Implementation Challenge, 1993. DIMACS benchmarks available atftp://Dimacs.Rutgers.EDU/pub/challenge/sat/ benchmarkscnf. UCSC benchmarks available atftp://Dimacs.Rutgers.EDU/pub/challenge/sat/ contributedUCSC.
[19] S. Kim, and H. Zhang, “ModGen: Theorem Proving by Model Generation,” Proc. 12th Nat'l Conf. Am. Assoc. Artificial Intelligence (AAAI-94), pp. 162-167, 1994.
[20] D.E. Knuth, “Estimating the Efficiency of Backtrack Programs,” Mathematics of Computation, vol. 29, no. 129, pp. 121-136, Jan. 1975.
[21] W. Kunz and D.K. Pradhan, “Recursive Learning: An Attractive Alternative to the Decision Tree for Test Generation in Digital Circuits,” Proc. Int'l Test Conf., pp. 816-825, 1992.
[22] T. Larrabee, “Efficient Generation of Test Patterns Using Boolean Satisfiability,” PhD dissertation, Dept. of Computer Science, Stanford Univ., STAN-CS-90-1302, Feb. 1990.
[23] S. Mallela and S. Wu, “A Sequential Circuit Test Generation System,” Proc. Int'l Test Conf., pp. 57-61, 1985.
[24] J.P. Marques-Silva and K.A. Sakallah, “Efficient and Robust Test Generation-Based Timing Analysis,” Proc. IEEE Int'l Symp. Circuits and Systems (ISCAS), pp. 303-306, London, June 1994.
[25] J.P. Marques-Silva and K.A. Sakallah, “Dynamic Search-Space Pruning Techniques in Path Sensitization,” Proc. IEEE/ACM Design Automation Conf. (DAC), pp. 705-711, San Diego, Calif., June 1994.
[26] J.P. Marques-Silva, “Search Algorithms for Satisfiability Problems in Combinational Switching Circuits,” PhD dissertation, Dept. of Electrical Eng. and Computer Science, Univ. of Michigan, May 1995.
[27] J.P. Marques-Silva and K.A. Sakallah, "Grasp: A New Search Algorithm for Satisfiability," Proc. Int'l Conf. Computer-Aided Design (ICCAD 96), IEEE CS Press, 1996, pp. 220-227.
[28] D.A. McAllester, “An Outlook on Truth Maintenance,” AI Memo 551, MIT AI Laboratory, Aug. 1980.
[29] P.C. McGeer,A. Saldanha,P.R. Stephan,R.K. Brayton,, and A.L. Sangiovanni-Vincentelli,“Timing analysis and delay-fault test generation using path-recursive functions,” Proc. Int’l Conf. on Computer-Aided Design, Nov. 1991, pp. 180-183.
[30] D. Pretolani, “Efficiency and Stability of Hypergraph SAT Algorithms,” Second DIMACS Implementation Challenge, D.S. Johnson and M.A. Trick, eds., 1993.
[31] T. Schiex and G. Verfaillie, “Nogood Recording for Static and Dynamic Constraint Satisfaction Problems,” Proc. Int'l Conf. Tools with Artificial Intelligence, pp. 48-55, 1993.
[32] M.H. Schulz and E. Auth, "Improved Deterministic Test Pattern Generation with Applications to Redundancy Identification," IEEE Trans. Computer-Aided Design, vol. 8, pp. 811-817, July 1989.
[33] B. Selman, H.J. Levesque, and D. Mitchell, “A New Method for Solving Hard Satisfiability Problems,” Proc. 10th Nat'l Conf. Artificial Intelligence (AAAI-92), 1992.
[34] E.M. Sentovich et al., “SIS: An Environment to Sequential Circuit Synthesis,” Memorandum no. UCB/ERL M92/41, Dept. of Electrical Eng. and Computer Sciences, Univ. of California at Berkeley, May 1992.
[35] R.M. Stallman and G.J. Sussman, “Forward Reasoning and Dependency-Directed Backtracking in a System for Computer-Aided Circuit Analysis,” Artificial Intelligence, vol. 9, pp. 135-196, Oct. 1977.
[36] P.R. Stephan, R.K. Brayton, and A.L. Sangiovanni-Vincentelli, “Combinational Test Generation Using Satisfiability,” Memorandum no. UCB/ERL M92/112, Dept. of Electrical Eng. and Computer Sciences, Univ. of California at Berkeley, Oct. 1992.
[37] R.E. Tarjan, “Finding Dominators in Directed Graphs,” SIAM J. Computing, vol. 3, no. 1, pp. 62-89, Mar 1974.
[38] A. Van Gelder and Y.K. Tsuji, “Satisfiability Testing with More Reasoning and Less Guessing,” Second DIMACS Implementation Challenge, D.S. Johnson and M.A. Trick, eds., 1993.
[39] R. Zabih and D.A. McAllester, “A Rearrangement Search Strategy for Determining Propositional Satisfiability,” Proc. Nat'l Conf. Artificial Intelligence, pp. 155-160, 1988.

Index Terms:
Satisfiability, search algorithms, conflict diagnosis, conflict-directed nonchronological backtracking, conflict-based equivalence, failure-driven assertions, unique implication points.
Citation:
João P. Marques-Silva, Karem A. Sakallah, "GRASP: A Search Algorithm for Propositional Satisfiability," IEEE Transactions on Computers, vol. 48, no. 5, pp. 506-521, May 1999, doi:10.1109/12.769433
Usage of this product signifies your acceptance of the Terms of Use.