By Dave A.D. Tompkins
The propositional satisfiability problem (SAT) is an important subject of study in many areas of computer science (including Computational Intelligence) and is the prototypical NP-complete problem. Some of the best known methods for solving certain types of SAT instances are Stochastic Local Search (SLS) algorithms.
In this talk we introduce UBCSAT, a new implementation and experimentation environment for SLS algorithms for SAT. Based on a novel triggered procedure architecture, UBCSAT provides implementations of numerous well-known and widely used SLS algorithms for SAT, including GSAT, WalkSAT, and SAPS; these implementations generally match or exceed the efficiency of the respective original reference implementations. Through numerous reporting and statistical features, including the measurement of run-time distributions, UBCSAT facilitates the advanced empirical analysis of these algorithms. New algorithm variants, SLS algorithms, and reporting features can be added to UBCSAT in a straightforward and efficient way. UBCSAT is implemented in C and runs on numerous platforms and operating systems; it is publicly and freely available at http://www.satlib.org/ubcsat.