×

SATenstein

swMATH ID: 14233
Software Authors: KhudaBukhsh, Ashiqur R.; Xu, Lin; Hoos, Holger H.; Leyton-Brown, Kevin
Description: 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.
Homepage: http://www.cs.ubc.ca/labs/beta/Projects/SATenstein/
Keywords: SAT; stochastic local search; automatic algorithm configuration
Related Software: Paramils; SMAC; irace; SPOT; SATzilla; MiniSat; UBCSAT; emili; Lingeling; SAT competition; PicoSAT; AClib; ACOTSP; DIMACS; SCIP; ParaDisEO; aspeed; Auto-WEKA; Treengeling; Plingeling
Cited in: 17 Publications

Standard Articles

1 Publication describing the Software, including 1 Publication in zbMATH Year
SATenstein: automatically building local search SAT solvers from components. Zbl 1351.68255
KhudaBukhsh, Ashiqur R.; Xu, Lin; Hoos, Holger H.; Leyton-Brown, Kevin
2016
all top 5

Cited by 34 Authors

6 Hoos, Holger H.
6 Stützle, Thomas G.
4 Leyton-Brown, Kevin
3 Hutter, Frank
3 Lindauer, Marius
2 Balint, Adrian
2 López-Ibáñez, Manuel
2 Malitsky, Yuri
2 Pagnozzi, Federico
2 Tompkins, Dave A. D.
1 Alfaro-Fernández, Pedro
1 Ansótegui, Carlos
1 Bayless, Sam
1 Borrajo, Daniel
1 Dorigo, Marco
1 Falkner, Stefan
1 Franzin, Alberto
1 Gabàs, Joel
1 Hall, George T.
1 Kadioglu, Serdar
1 KhudaBukhsh, Ashiqur R.
1 Leo, Kevin
1 Liao, Tianjun
1 Liberto, Giovanni Di
1 Linares López, Carlos
1 Montes de Oca, Marco A.
1 Núñez, Sergio
1 Oliveto, Pietro Simone
1 Ritt, Marcus
1 Ruiz, Rubén
1 Schaub, Torsten H.
1 Sellmann, Meinolf
1 Sudholt, Dirk
1 Xu, Lin

Cited in 4 Serials

6 Artificial Intelligence
5 European Journal of Operational Research
2 Computers & Operations Research
1 The Journal of Artificial Intelligence Research (JAIR)

Cited in 4 Fields

12 Computer science (68-XX)
7 Operations research, mathematical programming (90-XX)
1 Mathematical logic and foundations (03-XX)
1 Numerical analysis (65-XX)

Citations by Year