skip to main content
10.5555/244522.244560acmconferencesArticle/Chapter ViewAbstractPublication PagesiccadConference Proceedingsconference-collections
Article
Free Access

GRASP—a new search algorithm for satisfiability

Published:01 January 1997Publication History

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.

References

  1. 1.M. Abram ovici, M .A .Breuer and A.D .Friedm an,Digtal Systems Testing and Testable Design computer Science Press, 1990.Google ScholarGoogle Scholar
  2. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  3. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  4. 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 ScholarGoogle Scholar
  5. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  6. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  7. 7.M . L. G insberg, "Dynamic Backtracking," Journal of Artificial Intelligence Research, vol. 1, pp. 25-46, August 1993.Google ScholarGoogle ScholarDigital LibraryDigital Library
  8. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  9. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  10. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  11. 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 ScholarGoogle Scholar
  12. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  13. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  14. 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 ScholarGoogle Scholar
  15. 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 ScholarGoogle Scholar
  16. 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 ScholarGoogle ScholarCross RefCross Ref
  17. 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 ScholarGoogle Scholar
  18. 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 ScholarGoogle Scholar

Index Terms

  1. GRASP—a new search algorithm for satisfiability

            Recommendations

            Comments

            Login options

            Check if you have access through your login credentials or your institution to get full access on this article.

            Sign in

            PDF Format

            View or Download as a PDF file.

            PDF

            eReader

            View online with eReader.

            eReader