SATenstein: automatically building local search SAT solvers from components. Designing high-performance solvers for computationally hard problems is a difficult and often time-consuming task. Although such design problems are traditionally solved by the application of human expertise, we argue instead for the use of automatic methods. In this work, we consider the design 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. The parameters of SATenstein determine which components are selected and how these components behave; they allow SATenstein to instantiate many high-performance solvers previously proposed in the literature, along with trillions of novel solver strategies. We used an automated algorithm configuration procedure to find instantiations of SATenstein that perform well on several well-known, challenging distributions of SAT instances. Our experiments show that SATenstein solvers achieved dramatic performance improvements as compared to the previous state of the art in SLS algorithms; for many benchmark distributions, our new solvers also significantly outperformed all automatically tuned variants of previous state-of-the-art algorithms.
Keywords for this software
References in zbMATH (referenced in 10 articles , 1 standard article )
Showing results 1 to 10 of 10.
- Ansótegui, Carlos; Gabàs, Joel; Malitsky, Yuri; Sellmann, Meinolf: MaxSAT by improved instance-specific algorithm configuration (2016)
- KhudaBukhsh, Ashiqur R.; Xu, Lin; Hoos, Holger H.; Leyton-Brown, Kevin: SATenstein: automatically building local search SAT solvers from components (2016)
- Núñez, Sergio; Borrajo, Daniel; Linares López, Carlos: Automatic construction of optimal static sequential portfolios for AI planning and beyond (2015)
- Liao, Tianjun; Stützle, Thomas; Montes de Oca, Marco A.; Dorigo, Marco: A unified ant colony optimization algorithm for continuous optimization (2014)
- López-Ibáñez, Manuel; Stützle, Thomas: Automatically improving the anytime behaviour of optimisation algorithms (2014)
- Montes de Oca, Marco A.; Aydın, Doğan; Stützle, Thomas: An incremental particle swarm for large-scale continuous optimization problems: An example of tuning-in-the-loop (re)design of optimization algorithms (2011)
- Tompkins, Dave A.D.; Balint, Adrian; Hoos, Holger H.: Captain Jack: new variable selection heuristics in local search for SAT (2011)
- Hutter, Frank; Hoos, Holger H.; Leyton-Brown, Kevin: Tradeoffs in the empirical evaluation of competing algorithm designs (2010)
- Tompkins, Dave A.D.; Hoos, Holger H.: Dynamic scoring functions with variable expressions: new SLS methods for solving SAT (2010)
- Hutter, F.; Hoos, H.H.; Leyton-Brown, K.; Stuetzle, T.: Paramils: an automatic algorithm configuration framework (2009)