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  |  people  |  papers  |  software  |  benchmark problems   |  links |


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.



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


Benchmark Problems for SAT


Please send any questions, concerns or comments to Dave Tompkins