Captain Jack: New variable selection heuristics in local search for SAT

Abstract

Stochastic local search (SLS) methods are well known for their ability to find models of randomly generated instances of the propositional satisfiability problem (SAT) very effectively. Two well-known SLS-based SAT solvers are Sparrow, one of the best-performing solvers for random 3-SAT instances, and VE-Sampler, which achieved significant performance improvements over previous SLS solvers on SAT-encoded software verification problems. Here, we introduce a new highly parametric algorithm, Captain Jack, which extends the parameter space of Sparrow to incorporate elements from VE-Sampler and introduces new variable selection heuristics. Captain Jack has a rich design space and can be configured automatically to perform well on various types of SAT instances. We demonstrate that the design space of Captain Jack is easy to interpret and thus facilitates valuable insight into the configurations automatically optimized for different instance sets. We provide evidence that Captain Jack can outperform well-known SLS-based SAT solvers on uniform random k-SAT and 'industrial-like' random instances. © 2011 Springer-Verlag.