SATzilla: portfolio-based algorithm selection for SAT. It has been widely observed that there is no single ”dominant” SAT solver; instead, different solvers perform best on different instances. Rather than following the traditional approach of choosing the best solver for a given class of instances, we advocate making this decision online on a per-instance basis. Building on previous work, we describe SATzilla, an automated approach for constructing per-instance algorithm portfolios for SAT that use so-called empirical hardness models to choose among their constituent solvers. This approach takes as input a distribution of problem instances and a set of component solvers, and constructs a portfolio optimizing a given objective function (such as mean runtime, percent of instances solved, or score in a competition). The excellent performance of SATzilla was independently verified in the 2007 SAT Competition, where our SATzilla07 solvers won three gold, one silver and one bronze medal. In this article, we go well beyond SATzilla07 by making the portfolio construction scalable and completely automated, and improving it by integrating local search solvers as candidate solvers, by predicting performance score instead of runtime, and by using hierarchical hardness models that take into account different types of SAT instances. We demonstrate the effectiveness of these new techniques in extensive experimental results on data sets including instances from the most recent SAT competition.

References in zbMATH (referenced in 50 articles )

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

1 2 3 next

  1. Amadini, Roberto; Gabbrielli, Maurizio; Mauro, Jacopo: Portfolio approaches for constraint optimization problems (2016)
  2. Ansótegui, Carlos; Gabàs, Joel; Malitsky, Yuri; Sellmann, Meinolf: MaxSAT by improved instance-specific algorithm configuration (2016)
  3. Bischl, Bernd; Kerschke, Pascal; Kotthoff, Lars; Lindauer, Marius; Malitsky, Yuri; Fréchette, Alexandre; Hoos, Holger; Hutter, Frank; Leyton-Brown, Kevin; Tierney, Kevin; Vanschoren, Joaquin: ASlib: a benchmark library for algorithm selection (2016)
  4. Cauwet, Marie-Liesse; Liu, Jialin; Rozière, Baptiste; Teytaud, Olivier: Algorithm portfolios for noisy optimization (2016)
  5. KhudaBukhsh, Ashiqur R.; Xu, Lin; Hoos, Holger H.; Leyton-Brown, Kevin: SATenstein: automatically building local search SAT solvers from components (2016)
  6. Balint, Adrian; Belov, Anton; Järvisalo, Matti; Sinz, Carsten: Overview and analysis of the SAT challenge 2012 solver competition (2015)
  7. Botana, Francisco; Hohenwarter, Markus; Janičić, Predrag; Kovács, Zoltán; Petrović, Ivan; Recio, Tomás; Weitzhofer, Simon: Automated theorem proving in GeoGebra: current achievements (2015)
  8. Kühlwein, Daniel; Urban, Josef: MaLeS: A framework for automatic tuning of automated theorem provers (2015)
  9. Núñez, Sergio; Borrajo, Daniel; Linares López, Carlos: Automatic construction of optimal static sequential portfolios for AI planning and beyond (2015)
  10. Bridge, James P.; Holden, Sean B.; Paulson, Lawrence C.: Machine learning for first-order theorem proving (2014)
  11. Caraffini, Fabio; Neri, Ferrante; Picinali, Lorenzo: An analysis on separability for memetic computing automatic design (2014)
  12. Hurley, Barry; Kotthoff, Lars; Malitsky, Yuri; O’Sullivan, Barry: Proteus: a hierarchical portfolio of solvers and transformations (2014)
  13. Hutter, Frank; Xu, Lin; Hoos, Holger H.; Leyton-Brown, Kevin: Algorithm runtime prediction: methods & evaluation (2014)
  14. Messelis, Tommy; De Causmaecker, Patrick: An automatic algorithm selection approach for the multi-mode resource-constrained project scheduling problem (2014)
  15. Sagarna, Ramón; Mendiburu, Alexander; Inza, Iñaki; Lozano, Jose A.: Assisting in search heuristics selection through multidimensional supervised classification: a case study on software testing (2014)
  16. Smith-Miles, Kate; Baatar, Davaatseren: Exploring the role of graph spectra in graph coloring algorithm performance (2014)
  17. Stojadinović, Mirko; Marić, Filip: meSAT: multiple encodings of CSP to SAT (2014)
  18. Burns, Ethan; Ruml, Wheeler: Iterative-deepening search with on-line tree size prediction (2013)
  19. Cai, Shaowei; Su, Kaile: Local search for Boolean satisfiability with configuration checking and subscore (2013)
  20. Guo, Wen-Sheng; Yang, Guo-Wu; Hung, William N.N.; Song, Xiaoyu: Complete Boolean satisfiability solving algorithms based on local search (2013)

1 2 3 next