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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abramovici, M., Breuer, M. A., and Friedman, A. D. (1990). Digital Systems Testing and Testable Design. Computer Science Press.
Chakradhar, S. T., Agrawal, V. D., and Rothweiler, S. G. (1993). A Transitive Closure Algorithm for Test Generation. IEEE Transactions on Computer-Aided Design, 12(7): 1015–1028.
Davis, M. and Putnam, H. (1960). A Computing Procedure for Quantification Theory. Journal of the Association for Computing Machinery, 7:201–215.
DIMACS Challenge (1993). Dimacs benchmarks in ftp://dimacs.rutgers.edu/pub/-challenge/sat/benchmarks/cnf. UCSC benchmarks in in ftp://Dimacs.Rutgers.EDU/pub/-challenge/sat/benchmarks/cnf.
Freeman, J. W. (1995). Improvements to Propositional Satisfiability Search Algorithms. PhD thesis, University of Pennsylvania, Philadelphia, PA.
Garey, M. R. and Johnson, D. S. (1979). Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman and Company.
Ginsberg, M. (1993). Dynamic Backtracking. Journal of Artificial Intelligence Research, 1:25–46.
Giraldi, J. and Bushnell, M. L. (1991). Search State Equivalence for Redundancy Identification and Test Generation. In Proceedings of the International Test Conference, pages 184–193.
Kunz, W. and Pradhan, D. (1992). Recursive Learning: An Attractive Alternative to the Decision Tree for Test Generation in Digital Circuits. In Proceedings of the International Test Conference, pages 816–825.
Larrabee, T. (1990). Efficient Generation of Test Patterns Using Boolean Satisfiability. PhD thesis, Department of Computer Science, Stanford University. Technical Report STAN-CS-90-1302.
Schiex, T. and Verfaillie, G. (1993). Nogood Recording for Static and Dynamic Constraint Satisfaction Problems. In Proceedings of the International Conference on Tools with Artificial Intelligence, pages 48–55.
Schulz, M. H. and Auth, E. (1989). Improved Deterministic Test Pattern Generation with Applications to Redundancy Identification. IEEE Transactions on Computer-Aided Design, 8(7):811–816.
Silva, J. P. M. and Sakallah, K. A. (1994). Dynamic Search-Space Pruning Techniques in Path Sensitization. In Proceedings of the Design Automation Conference, pages 705–711.
Silva, J. P. M. (1995). Search Algorithms for Satisfiability Problems in Combinational Switching Circuits. PhD thesis, University of Michigan.
Silva, J. P. M. and Sakallah, K. A. (1996). GRASP-A New Search Algorithm for Satisfiability. Technical Report CSE-TR-292–96, University of Michigan.
Stallman, R. M. and Sussman, G. J. (1977). Forward Reasoning and Dependency-Directed Backtracking in a System for Computer-Aided Circuit Analysis. Artificial Intelligence, 9:135–196.
Stephan, P. R., Brayton, R. K., and Sangiovanni-Vincen-telli, A. L. (1992). Combinational Test Generation Using Satisfiability. Technical Report UCB/ERL M92/112, Department of Electrical Engineering and Computer Sciences, University of California at Berkeley.
Zabih, R. and McAllester, D. A. (1988). A Rearrangement Search Strategy for Determining Propositional Satisfiability. In Proceedings of the National Conference on Artificial Intelligence, pages 155–160.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer Science+Business Media New York
About this chapter
Cite this chapter
Marques Silva, J.P., Sakallah, K.A. (2003). Grasp—A New Search Algorithm for Satisfiability. In: Kuehlmann, A. (eds) The Best of ICCAD. Springer, Boston, MA. https://doi.org/10.1007/978-1-4615-0292-0_7
Download citation
DOI: https://doi.org/10.1007/978-1-4615-0292-0_7
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4613-5007-1
Online ISBN: 978-1-4615-0292-0
eBook Packages: Springer Book Archive