Sciweavers

Share
ICCAD
1996
IEEE

GRASP - a new search algorithm for satisfiability

8 years 7 months ago
GRASP - a new search algorithm for satisfiability
This paper introduces GRASP (Generic seaRch Algorithm for the Satisfiability Problem), an integrated algorithmic framework for SAT that unifies several previously proposed searchpruning 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 n...
João P. Marques Silva, Karem A. Sakallah
Added 07 Aug 2010
Updated 07 Aug 2010
Type Conference
Year 1996
Where ICCAD
Authors João P. Marques Silva, Karem A. Sakallah
Comments (0)
books