UBC Theses and Dissertations

UBC Theses Logo

UBC Theses and Dissertations

SATenstein : automatically building local search SAT solvers from components Khudabukhsh, Ashiqur Rahman

Abstract

Designing high-performance solvers for computationally hard problems is a difficult and often time-consuming task. It is often the case that a new solver is created by augmenting an existing algorithm with a mechanism found in a different algorithm or by combining components from different algorithms. 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 drawn from or inspired by existing high-performance SLS algorithms for SAT. In SATenstein, we exposed several design elements in the form of parameters that control both the selection and the behavior of components. We also exposed some parameters that were hard-coded into the implementations of the algorithms we studied. By setting these parameters, SATenstein can be instantiated as a huge number of different solvers, including many known high-performance solvers and trillions of solvers never studied before. 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 previous best-performing SLS algorithms, despite expending minimal manual effort.

Item Citations and Data

Rights

Attribution-NonCommercial-NoDerivatives 4.0 International