GRASP - A New Search Algorithm for Satisfiability

This paper introduces GRASP (Generic seaRch Algorithm for the Satisjiability Problem), an integrated algorithmic framework for SAT that un.$es several previously proposed searchpruning techniques and facilitates ident$cation of additional ones. GRASP is premised on the inevitability of confzicts during search and its most distinguishing feature is the augmentation of basic backtracking search with a powerfil confzict analysis procedure. Analyzing confzicts to determine their cawes 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 andpreempt the occurrence of similar conficts later on in the search. Finally, straightjwward bookkeeping of the causality chains leading up to conflicts allows GRASP to identifi assignments that are necessary for a solution to be found. fiperimental results obtained from a large number of benchmarks, including many from the $eld of test pattern generation, indicate that application of the proposed confzict analysis techniques to SATalgorithm can be extremely effectivefor a large number of representative classes of SAT instances. 1