SATenstein: Automatically Building Local Search SAT Solvers From
Components
By Ashiqur KhudaBukhsh
Designing high-performance algorithms for computationally hard problems is a
difficult and often time-consuming task. In this work, we demonstrate that
this task can be automated in the context of stochastic local search (SLS)
solvers for the propositional satisfiability problem (SAT). We first
introduce a generalised, highly parameterised solver framework, dubbed
SATenstein, that includes components gleaned from or inspired by existing
high-performance SLS algorithms for SAT. The parameters of SATenstein
control the selection of components used in any specific instantiation and
the behaviour of these components. SATenstein can be configured to
instantiate a broad range of existing high-performance SLS-based SAT
solvers, and also over 10^23 novel algorithms. We used an automated
algorithm configuration procedure to find instantiations of SATenstein that
perform well on several well-known, challenging distributions of SAT
instances. Overall, we consistently obtained significant improvements over
the previously best-performing SLS algorithms, despite expending minimal
manual effort.
Visit the LCI Forum page