ABSTRACT
This paper introduces GRASP (Generic seaRch Algorithm for the Satisfiability Problem), an integrated algorithmic framework for SAT that unifies several previously proposed search-pruning techniques and facilitates identification of additional ones. GRASP is premised on the inevitability of conflicts during 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 non-chronologically 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, including many from the field of test pattern generation, 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. Abram ovici, M .A .Breuer and A.D .Friedm an,Digtal Systems Testing and Testable Design computer Science Press, 1990.Google Scholar
- 2.S.T. Chakradhar, V. D . Agrawal and S. G. Rothweiler, "A Transitive C bsure Algorithm for Test Generation," IEEE Transitions on Coputer-Aided Design, vol. 12, no. 7, pp. 1015-1028, July 1993.Google ScholarDigital Library
- 3.M . Davis and H . Putnam, "A Computing Procedure for Quantification Theory," Journal of the Association for Computing Machinery, vol. 7, pp. 201-215,1960. Google ScholarDigital Library
- 4.DIMACS Challenge benchmarks in ftp://D in acsRutgers EDU/pub/challenge/sat/benchm arks/cnf. UCSC benchmarks in/pub/chllange/sat/contributed/UCSC.Google Scholar
- 5.J. W. Freeman, Improvements to Propositional Satisfiability Search Algorithms, Ph D . D issartation, Department of Com - puter and Information Science, University of Pennsylvania, May 1995. Google ScholarDigital Library
- 6.M . R. Garey and D . S. Johnson, Computers and Intractability. A Guide to the Theory of NP-Completeness, W. H . Freeman and Company, 1979. Google ScholarDigital Library
- 7.M . L. G insberg, "Dynamic Backtracking," Journal of Artificial Intelligence Research, vol. 1, pp. 25-46, August 1993.Google ScholarDigital Library
- 8.J . Girabli and M . L. Bushnell, "Search State Equivalence for Redundancy Identification and Test Generation," in Proceedings of the International Test Conference, pp. 184-193, 1991. Google ScholarDigital Library
- 9.W . Kunz and D . K. Pradhan, "Recursive Learning: An Attractive Alternative to the Decision Tree for Test Generation in Digital Circuits," in Proceedings of the International Test Conference, pp. 816-825, 1992. Google ScholarDigital Library
- 10.T. Larrabee, Efficient Generation of Test Patterns Using Bodeen Satisifiability, Ph D . Dissertation, Department of Computer Science, Stanford University, STAN -CS-90-1302, February 1990. Google ScholarDigital Library
- 11.T. Schiex and G . Verfaillie, "Nogood Recording for Static and Dynamic Constraint Satisfaction Problems," in Procedings of the International Conference on Tods with Artificial Intelligence pp. 48-55, 1993.Google Scholar
- 12.M . H . Schulz and E .Auth, "Improved Determ inistic TestPattern Generation with Applications to Redundancy Identification," IEEE Transactions on Computer-Aided Design, vol. 8, no. 7, pp. 811-816, July 1989.Google ScholarDigital Library
- 13.J. P. M . Silva and K. A. Sakallah, "Dynamic Search-Space Pruning Techniques in Path Sensitization," in Proc IEEE/ ACM Design Automation Conference (DAC), pp. 705-711, June 1994, San Diego, California. Google ScholarDigital Library
- 14.J. P. M . Silva, Search Algorithms for Satisfiability Problems in Combinational Switching Circuits Ph D . Dissertation, Department of Electrical Engineering and Computer Science, University of Michigan, May 1995.Google Scholar
- 15.J. P. M . Silva and K. A. Sakallah, "GRASP-A New Search Algorithm for Satisfiability," Technical Report TR -CSE-292- 96, University of Michigan, April 1996.Google Scholar
- 16.R. M . Stallman and G . J. Sussman, "Forward Reasoning and Dependency-Directed Backtracking in a System for Computer-Aided Circuit Analusis," Artificial Intelligence, vol. 9, pp. 135-196, October 1977.Google ScholarCross Ref
- 17.P. R. Stephan, R. K. Brayton and A. L. Sangiovanni-Vincentelli, "Combinational Test Generation Using Satisfiability," Memorandum no.UCB/ERLM 92/112, Department of Electrical Engineering and Computer Science, University of California at Berkeley, October 1992.Google Scholar
- 18.R. Zabih and D . A. McAllester, "A Rearrangement Search Strategy for Determining Propositional Satisfiability," in Proceedings of the National Conference on Artificial Intelligence, pp. 155-160, 1988.Google Scholar
Index Terms
GRASP—a new search algorithm for satisfiability
Recommendations
GRASP: A Search Algorithm for Propositional Satisfiability
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 ...
Conflict Analysis in Search Algorithms for Satisfiability
ICTAI '96: Proceedings of the 8th International Conference on Tools with Artificial IntelligenceThis paper introduces GRASP (Generic seaRch Algorithm for the Satisfiability Problem), a new search algorithm for Propositional Satisfiability (SAT). GRASP incorporates several search-pruning techniques, some of which are specific to SAT, whereas others ...
Satisfiability-Based Algorithms for Boolean Optimization
This paper proposes new algorithms for the Binate Covering Problem (BCP), a well-known restriction of Boolean Optimization. Binate Covering finds application in many areas of Computer Science and Engineering. In Artificial Intelligence, BCP can be used ...
Comments