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.

References in zbMATH (referenced in 19 articles , 1 standard article )

Showing results 1 to 19 of 19.
Sorted by year (citations)

  1. de Souza, Marcelo; Ritt, Marcus; López-Ibáñez, Manuel: Capping methods for the automatic configuration of optimization algorithms (2022)
  2. Hall, George T.; Oliveto, Pietro S.; Sudholt, Dirk: On the impact of the performance metric on efficient algorithm configuration (2022)
  3. Alfaro-Fernández, Pedro; Ruiz, Rubén; Pagnozzi, Federico; Stützle, Thomas: Automatic algorithm design for hybrid flowshop scheduling problems (2020)
  4. Franzin, Alberto; Stützle, Thomas: Revisiting simulated annealing: a component-based analysis (2019)
  5. Pagnozzi, Federico; Stützle, Thomas: Automatic design of hybrid stochastic local search algorithms for permutation flowshop problems (2019)
  6. Hutter, Frank; Lindauer, Marius; Balint, Adrian; Bayless, Sam; Hoos, Holger; Leyton-Brown, Kevin: The configurable SAT solver challenge (CSSC) (2017)
  7. Lindauer, Marius; Hoos, Holger; Leyton-Brown, Kevin; Schaub, Torsten: Automatic construction of parallel portfolios via algorithm configuration (2017)
  8. Ansótegui, Carlos; Gabàs, Joel; Malitsky, Yuri; Sellmann, Meinolf: MaxSAT by improved instance-specific algorithm configuration (2016)
  9. KhudaBukhsh, Ashiqur R.; Xu, Lin; Hoos, Holger H.; Leyton-Brown, Kevin: SATenstein: automatically building local search SAT solvers from components (2016)
  10. Liberto, Giovanni Di; Kadioglu, Serdar; Leo, Kevin; Malitsky, Yuri: DASH: dynamic approach for switching heuristics (2016)
  11. Falkner, Stefan; Lindauer, Marius; Hutter, Frank: \textttSpySMAC: automated configuration and performance analysis of SAT solvers (2015)
  12. Núñez, Sergio; Borrajo, Daniel; Linares López, Carlos: Automatic construction of optimal static sequential portfolios for AI planning and beyond (2015)
  13. Liao, Tianjun; Stützle, Thomas; Montes de Oca, Marco A.; Dorigo, Marco: A unified ant colony optimization algorithm for continuous optimization (2014)
  14. López-Ibáñez, Manuel; Stützle, Thomas: Automatically improving the anytime behaviour of optimisation algorithms (2014)
  15. 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) ioport
  16. Tompkins, Dave A. D.; Balint, Adrian; Hoos, Holger H.: Captain Jack: new variable selection heuristics in local search for SAT (2011)
  17. Hutter, Frank; Hoos, Holger H.; Leyton-Brown, Kevin: Tradeoffs in the empirical evaluation of competing algorithm designs (2010) ioport
  18. Tompkins, Dave A. D.; Hoos, Holger H.: Dynamic scoring functions with variable expressions: new SLS methods for solving SAT (2010)
  19. Hutter, F.; Hoos, H. H.; Leyton-Brown, K.; Stuetzle, T.: Paramils: an automatic algorithm configuration framework (2009)