CSE 573 -- Artificial Intelligence -- Autumn 1999
TERM PROJECT #1

An Empirical Study of Satisfiability Solvers and Refinements to DPLL

AUTHORS: Daniel Grossman, Tammy VanDeGrift

Abstract

The satisfiability problem, a core problem in the field of computer science, especially artificial intelligence, is generally solved either deterministically or stochastically. In this paper we investigate the hard problems for the stochastic Walksat algorithm as well as the deterministic Davis-Putnam-Logemann-Loveland algorithm. After comparing these two algorithms, we introduce two new branching heuristics for the DPLL algorithm. This paper shows that the choice for the splitting variable in DPLL is crucial to the efficiency of finding solutions, and we demonstrate the superior efficiency of our algorithm (the Most Occurrences algorithm) with respect to the most commonly used heuristic, "Moms".

Please download our paper here:   Most.ps

References

  1. Stephen A. Cook and David G. Mitchell. "Finding Hard Instances of the Satisfiability Problem: A Survey". DIMACS Series in Discrete Mathematics and Theoretical Computer Science, #5, 1997.
  2. Douglas D. Edwards. "Research Summary". http://www.sitewrite.com/dde/ucb/research-summary.html, December 1996.
  3. Pascal Van Hentenryck and Vijay Saraswat, et al. "Strategic Directions in Constraint Programming". ACM Computing Surveys, Vol. 28(#4), December 1996.
  4. David G. Mitchell and Hector J. Levesque. "Some Pitfalls for Experimenters with Random SAT". Elsevier Science, 1995.
  5. Ming Ouyang. "How good are branching rules in DPLL?". Technical Report #96-38, Rutgers University, September 1996.
  6. William M. Spears. "Simulated Annealing for Hard Satisfiability Problems". Technical report, AI Center, Naval Research Laboratory, 1993.
  7. Daniel S. Weld. Recent Advances in AI Planning. AI Magazine, 1999.
This page last updated: Tuesday, June 27, 2000.
E-mail the authors: Daniel Grossman, Tammy VanDeGrift.