VOL. 48, NO. 5, MAY 1999 | João P. Marques-Silva, Member, IEEE, and Karem A. Sakallah, Fellow, IEEE
This paper introduces GRASP (Generic Search Algorithm for the Satisfiability Problem), a new search algorithm for Propositional Satisfiability (SAT). GRASP incorporates several search-pruning techniques, including conflict analysis, to enhance the efficiency of SAT solving. The core of GRASP is its ability to perform nonchronological backtracking by analyzing conflicts, which allows it to backtrack to earlier levels in the search tree and prune large portions of the search space. Additionally, GRASP can recognize and prevent similar conflicts in the future by recording the causes of conflicts. The paper also discusses the implementation of these techniques and presents experimental results showing that GRASP outperforms several state-of-the-art SAT algorithms on a wide range of benchmarks. The results suggest that GRASP is particularly effective for practical classes of SAT instances, especially those likely to be unsatisfiable, such as those encountered in Automated Theorem Proving and Electronic Design Automation tasks. The paper concludes with suggestions for further research, including heuristic control of clause database growth and improvements to the deduction engine.This paper introduces GRASP (Generic Search Algorithm for the Satisfiability Problem), a new search algorithm for Propositional Satisfiability (SAT). GRASP incorporates several search-pruning techniques, including conflict analysis, to enhance the efficiency of SAT solving. The core of GRASP is its ability to perform nonchronological backtracking by analyzing conflicts, which allows it to backtrack to earlier levels in the search tree and prune large portions of the search space. Additionally, GRASP can recognize and prevent similar conflicts in the future by recording the causes of conflicts. The paper also discusses the implementation of these techniques and presents experimental results showing that GRASP outperforms several state-of-the-art SAT algorithms on a wide range of benchmarks. The results suggest that GRASP is particularly effective for practical classes of SAT instances, especially those likely to be unsatisfiable, such as those encountered in Automated Theorem Proving and Electronic Design Automation tasks. The paper concludes with suggestions for further research, including heuristic control of clause database growth and improvements to the deduction engine.