Introduction of SATenstein
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
generalized, highly parameterized 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 billions of 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.