SATzilla: Portfolio-based Algorithm Selection for SAT

By Lin Xu, Frank Hutter, Holger H. Hoos, Kevin Leyton-Brown. 2008

1,047 citations recorded by the source corpus.

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.

Subfields: Artificial Intelligence, Computer Networks and Communications

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computer Networks and Communications

Citations in the corpus

Optimal Decision Trees for the Algorithm Selection Problem: Integer Programming Based Approaches (2019, background): “Another approach is to model the ASP as a regression problem, in which one tries to predict the performance of each algorithm for a given instance and the best one is selected (Xu et al., 2008; Leyton-Brown et al., 2003b; Battistutta et al., 2017).”
ParamILS: An Automatic Algorithm Configuration Framework (2014, background): “For approaches that try to choose the best algorithm on a per-instance basis, see (Leyton-Brown et al., 2002; Carchrae and Beck, 2005; Gebruers et al., 2005; Gagliolo and Schmidhuber, 2006; Xu et al., 2008).”
Learning a SAT Solver from Single-Bit Supervision (2018, methodology): “ing are described in Knuth (2015). 8 Published as a conference paper at ICLR 2019 Grozea & Popescu, 2014; Flint & Blaschko, 2012), parameter tuning (Singh et al., 2009), and solver selection (Xu et al., 2008). None of these approaches use neural networks, and instead make use of both generic”
Venture: a higher-order probabilistic programming platform with programmable inference (2014, background): “Machine learning schemes for algorithm selection (Xu et al., 2008) and reinforcement-learning-based meta-computation (Lagoudakis and Littman, 2001) can be viewed as natural special cases.”
Hydra-MIP : Automated Algorithm Configuration and Selection for Mixed Integer Programming (2011, methodology): “Table 2 shows that by using our new cost-sensitive decision forest, we improved SATZILLA’s performance 29% (in average over three categories) in terms of PAR over the previous (competition-winning) version of SATZILLA; for the important industrial category, we observed PAR improvements of 34%.”
Potassco: The Potsdam Answer Set Solving Collection (2011, positive): “Inspired by satzilla [99], we address the parameter sensitivity in ASP solving by exploring a portfoliobased approach.”
Answer Set Solving in Practice (2012, positive): “, 2011d) is inspired by satzilla (Xu et al., 2008).”
Scalable Gaussian process-based transfer surrogates for hyperparameter optimization (2017, methodology): “Application domains include hard combinatorial problems such as SAT (Xu et al. 2008) and TSP (Kanda et al.”
Algorithm runtime prediction: Methods & evaluation (2012, methodology): “While the models were certainly not perfect, note that even the relatively poor predictions of ridge regression variant RR tended to be accurate within about an order of magnitude, which was enough to enable the portfolio-based algorithm selector SATzilla [119] to win ﬁve medals in each of the 2007 ”
Instance-Specific Algorithm Configuration (2014, methodology): “However, in preliminary experiments it is found that the local search features mentioned in [126] take a considerable amount of time to compute and are not imperative to finding a good clustering of instances.”
Algorithm Runtime Prediction: Methods and Evaluation (Extended Abstract) (2015, methodology): “• RR: ridge regression with quadratic basis function expansion and forward selection as in early versions of SATzilla [Leyton-Brown et al., 2009; Xu et al., 2008]);”
Hyperparameter optimization: Foundations, algorithms, best practices, and open challenges (2021, background): “AC is much broader than HPO, and has a particularly rich history regarding the configuration of discrete optimization solvers (Xu et al., 2008).”
Automated Algorithm Configuration and Parameter Tuning (2012, methodology): “…properties of that instance determined just before attempting to solve it (see, e.g., Rice, 1976; Leyton-Brown et al, 2003; Guerri and Milano, 2004; Xu et al, 2007, 2008); similarly, per-instance algorithm configuration methods use instance properties to determine the specific configuration of a…”
Efficient Parameter Importance Analysis via Ablation with Surrogates (2017, methodology): “The application of our surrogate-ablation requires: i) Instance features as numerical representations of instances; these are available for many domains (Xu et al. 2008; 2011; Gebser et al. 2011; Fawcett et al. 2014) or can be generated in a domain-independent fashion (Loreggia et al.”
ISAC - Instance-Specific Algorithm Configuration (2010, methodology): “Instance Features: We utilize the features proposed by [35] to classify each problem instance.”