EECS 298-11: CAD Seminar
Tuesday, June 11, 1996, 5pm
Cory Hall--Hogan Room

  GRASP -- A New Search Algorithm for Satisfiability
  Joao P. Marques Silva and Karem A. Sakallah
  INESC, Portugal

In this talk I will describe 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.