Dynamic Local Search for the Satisfiability Problem (DLS4SAT) Bioinformatics, and Empirical & Theoretical Algorithmics Laboratory (β-Lab) Department of Computer Science The University of British Columbia

Abstract

The Satisfiability problem (SAT) is an important subject of study in many areas of computer science. Since SAT is NP complete, there is little hope to develop a complete algorithm that scales well on all types of problem instances.  Some of the best known methods for SAT are Stochastic Local Search (SLS) algorithms; these are typically incomplete algorithms that cannot determine with certainty that a given formula is unsatisfiable, but often find models of satisfiable formulae surprisingly effectively.  As the name applies, SLS algorithms search a local (small) region of the search space, looking for a global minimum, escaping from local minima with stochastic methods.  Dynamic Local Search (DLS) methods are SLS algorithms that dynamically modify the space they are searching.  We are researching the behaviour of existing DLS algorithms, and developing new and improved methods of conducting DLS.

People

• Dave Tompkins, Postdoctoral Teaching Fellow (UBC)
• Holger Hoos, Professor (UBC)

Papers

For a list of papers we have published, consult Dave's Publication page.

Software

• UBCSAT
• SAPS Version 1.0
  Note: This is the software used for the 2002 SAPS paper (Hutter et al.).

Benchmark Problems for SAT

• SATLIB The Satisfiability Library
  (The instances used for the 2002 SAPS paper (Hutter et al.) can be found at SATLIB, but are also available here for your convenience)

Links

• SATLIB  The Satisfiability Library
• Sat Live!  Up-to-date links for the satisfiability problem
• Sat-Ex  The experimentation web site around the satisfiability problem
• Henry Kautz  The original WalkSAT code can be found here
• Dale Schuurmans  The ESG code can be found here

Please send any questions, concerns or comments to Dave Tompkins