
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
João P. MarquesSilva, Karem A. Sakallah, "GRASP: A Search Algorithm for Propositional Satisfiability," IEEE Transactions on Computers, vol. 48, no. 5, pp. 506521, May, 1999.  
BibTex  x  
@article{ 10.1109/12.769433, author = {João P. MarquesSilva and Karem A. Sakallah}, title = {GRASP: A Search Algorithm for Propositional Satisfiability}, journal ={IEEE Transactions on Computers}, volume = {48}, number = {5}, issn = {00189340}, year = {1999}, pages = {506521}, doi = {http://doi.ieeecomputersociety.org/10.1109/12.769433}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Computers TI  GRASP: A Search Algorithm for Propositional Satisfiability IS  5 SN  00189340 SP506 EP521 EPD  506521 A1  João P. MarquesSilva, A1  Karem A. Sakallah, PY  1999 KW  Satisfiability KW  search algorithms KW  conflict diagnosis KW  conflictdirected nonchronological backtracking KW  conflictbased equivalence KW  failuredriven assertions KW  unique implication points. VL  48 JA  IEEE Transactions on Computers ER   
Abstract—This paper introduces GRASP (Generic seaRch Algorithm for the Satisfiability Problem), a new search algorithm for Propositional Satisfiability (SAT). GRASP incorporates several searchpruning 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 DavisPutnam Based Enumeration Algorithm for Linear PseudoBoolean Optimization,” Technical Report MPII952003, MaxPlanckInstitut 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. 633645, 1986.
[4] M. Bruynooghe, “Analysis of Dependencies to Improve the Behaviour of Logic Programs,” Proc. Fifth Conf. Automated Deduction, pp. 293305, 1980.
[5] S.T. Chakradhar, V.D. Agrawal, and S.G. Rothweiler, "A Transitive Closure Algorithm for Test Generation," IEEE Trans. ComputerAided Design, vol. 12, pp. 1,0151,028, July 1993.
[6] J. Crawford and L. Auton, “Experimental Results on the CrossOver Point in Satisfiability Problems,” Proc. 11th Nat'l Conf. Artificial Intelligence (AAAI93), pp. 2228, 1993.
[7] M. Davis and H. Putnam, "A Computing Procedure for Quantification Theory," J. ACM, vol. 7, July 1960, pp. 201215.
[8] R. Dechter, “Enhancement Schemes for Constraint Processing: Backjumping, Learning, and Cutset Decomposition,” Artificial Intelligence, vol. 41, pp. 273312, 1989/90.
[9] J. de Kleer, “An AssumptionBased 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. 4561, 1989.
[13] M.R. Garey and D.S. Johnson, Computers and Intractability: A Guide to the Theory of NPCompleteness.New York: W.H. Freeman, 1979.
[14] J. Gaschnig, “Performance Measurement and Analysis of Certain Search Algorithms,” PhD dissertation, Dept. of Computer Science, CarnegieMellon Univ., CMUCS79124, May 1979.
[15] M.L. Ginsberg, “Dynamic Backtracking,” J. Artificial Intelligence Research, vol. 1, pp. 2546, Aug. 1993.
[16] J. Giraldi and M.L. Bushnell, “Search State Equivalence for Redundancy Identification and Test Generation,” Proc. Int'l Test Conf., pp. 184193, 1991.
[17] J.P. Hayes, Introduction to Digital Logic Design. AddisonWesley, 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 (AAAI94), pp. 162167, 1994.
[20] D.E. Knuth, “Estimating the Efficiency of Backtrack Programs,” Mathematics of Computation, vol. 29, no. 129, pp. 121136, 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. 816825, 1992.
[22] T. Larrabee, “Efficient Generation of Test Patterns Using Boolean Satisfiability,” PhD dissertation, Dept. of Computer Science, Stanford Univ., STANCS901302, Feb. 1990.
[23] S. Mallela and S. Wu, “A Sequential Circuit Test Generation System,” Proc. Int'l Test Conf., pp. 5761, 1985.
[24] J.P. MarquesSilva and K.A. Sakallah, “Efficient and Robust Test GenerationBased Timing Analysis,” Proc. IEEE Int'l Symp. Circuits and Systems (ISCAS), pp. 303306, London, June 1994.
[25] J.P. MarquesSilva and K.A. Sakallah, “Dynamic SearchSpace Pruning Techniques in Path Sensitization,” Proc. IEEE/ACM Design Automation Conf. (DAC), pp. 705711, San Diego, Calif., June 1994.
[26] J.P. MarquesSilva, “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. MarquesSilva and K.A. Sakallah, "Grasp: A New Search Algorithm for Satisfiability," Proc. Int'l Conf. ComputerAided Design (ICCAD 96), IEEE CS Press, 1996, pp. 220227.
[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. SangiovanniVincentelli,“Timing analysis and delayfault test generation using pathrecursive functions,” Proc. Int’l Conf. on ComputerAided Design, Nov. 1991, pp. 180183.
[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. 4855, 1993.
[32] M.H. Schulz and E. Auth, "Improved Deterministic Test Pattern Generation with Applications to Redundancy Identification," IEEE Trans. ComputerAided Design, vol. 8, pp. 811817, 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 (AAAI92), 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 DependencyDirected Backtracking in a System for ComputerAided Circuit Analysis,” Artificial Intelligence, vol. 9, pp. 135196, Oct. 1977.
[36] P.R. Stephan, R.K. Brayton, and A.L. SangiovanniVincentelli, “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. 6289, 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. 155160, 1988.