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.

Download SATenstein

Source code for computing transformation cost between SATenstein configurations presented in LION'16 (download)

Most up to date version (github link)

Source code for SATenstein2.0 presented in AIJ'16 (download)

Source code for SATenstein presented in IJCAI'09 (also referenced in AIJ'16) (download)

Quick start guide (PDF)

Data (Instance Sets)

More about SATenstein

Our papers about SATenstein:

Useful Links

Please send us your feedback to khudabukhsh@gmail.com