PaperlayerView exact revision on arXiv

Source-linked AI summary

SATzilla: Portfolio-based Algorithm Selection for SAT

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

arXiv:1111.2249v1cs.AI

TL;DR

SAT solving lacks a single dominant solver because different algorithms excel on different instances, creating a per-instance selection problem. SATzilla constructs automated portfolios using empirical hardness models and extends them with scalable automation, local-search integration, score prediction, and hierarchical models. Its portfolios outperformed their component solvers in experiments, while SATzilla07 achieved strong results in the 2007 SAT Competition.

  • Problem

    Different SAT solvers perform best on different instances, so selecting one solver based only on average performance can neglect strong instance-specific alternatives.

  • Method

    SATzilla builds per-instance algorithm portfolios using empirical hardness models, with automated construction, local-search candidate solvers, score prediction, and hierarchical models for different SAT instance types.

  • Results

    SATzilla07 portfolio solvers always outperformed their components, and the 2007 version placed first in three competition categories, second in one, and third in another.

  • Takeaways & Limitations

    SATzilla’s performance benefits from combining solvers with complementary instance-specific strengths, including solvers that are competitive only for certain kinds of instances.

  • Takeaways & Limitations

    SATzilla’s performance depends on the power of its component solvers, and further gains may require identifying additional solvers that are overlooked because they perform poorly on average.

Abstract

from arXiv · show

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.

1. Introduction

SAT solving has produced many sophisticated but differently performing algorithms, making per-instance algorithm selection preferable to choosing a single average winner. SATzilla addresses this problem with empirical hardness models that predict solver performance and support automated algorithm portfolios.

  • 1.1 The Algorithm Selection Problem: SAT solvers often perform very differently across instances, so practitioners must choose which algorithm or algorithms to run for a performance objective such as expected runtime.
  • 1.1 The Algorithm Selection Problem: The winner-take-all approach selects the solver with the best average or median runtime, neglecting solvers that excel on particular instances.
  • 1.1 The Algorithm Selection Problem: Empirical hardness models predict an algorithm’s runtime from instance features and past performance, enabling per-instance selection among multiple solvers.
  • 1. Introduction: SATzilla is a portfolio-based SAT solver using empirical hardness models for per-instance selection, and its 2007 version placed first in three competition categories and second and third in two others.
  • 1.2 Algorithm Portfolios: An algorithm portfolio combines multiple black-box algorithms to exploit differences in their best-case performance and improve average-case performance.
  • 1.2 Algorithm Portfolios: An (a, b)-of-n portfolio contains n algorithms and selects between a and b algorithms when none terminates early; portfolios may run solvers in parallel, sequentially, or partly sequentially.

2. Design I: Building Algorithm Portfolios with Empirical Hardness Models

The portfolio methodology builds an offline, per-instance solver selector from representative data, instance features, and empirical hardness models, then applies predictions online. It addresses costly runtime data and unknown satisfiability through preprocessing, fallback solvers, feature selection, censored-data modeling, and hierarchical models.

  • Offline portfolio construction: Portfolio construction selects representative instances, complementary candidate solvers, informative low-cost features, and training runtimes before fitting predictive models.Candidate solvers should have relatively uncorrelated runtimes and perform well on at least some instances.
  • Offline portfolio construction: Pre-solvers handle easy instances before feature computation, while a validation-selected backup solver handles feature-computation failures or timeouts.Without enough such cases, the single best component solver is used as backup.
  • Offline portfolio construction: Empirical hardness models predict each portfolio algorithm’s runtime from instance features, after which automatic subset selection retains the solver combination with best validation performance.Because predictions are imperfect, removing a solver can improve portfolio performance.
  • Online portfolio use: Online selection runs pre-solvers, computes features, predicts every candidate’s runtime, and runs the predicted best solver, trying the next-best solver if execution fails.If feature computation fails, the backup solver is selected instead.
  • Empirical hardness models: Models use feature selection, quadratic basis expansion, and ridge regression to predict logarithmic runtime, with regression choice requiring accurate and computationally efficient predictions.The log transformation is important because runtimes vary substantially across hard combinatorial instances.
  • Empirical hardness models: Censored-run modeling is necessary because SAT runtimes can be extremely costly to collect; earlier experiments found dropping censored runs or assigning cutoff values significantly worse than the presented method.The comparison attributes the inferior alternatives’ performance to bias in the empirical hardness models.
  • Hierarchical hardness models: Hierarchical hardness models combine conditional predictions using learned satisfiability-related weighting functions rather than directly selecting a model from the classifier output.The framework can use six conditional models trained on satisfiable and unsatisfiable instances from different data sets.

3. Construction I: Building SATzilla07 for the 2007 SAT Competition

SATzilla07 was constructed in category-specific and heterogeneous forms for the 2007 SAT Competition using the paper’s portfolio design methodology. The authors trained versions on RANDOM, HANDMADE, and ALL data, and later reported an INDUSTRIAL version built after the submission deadline.

  • SATzilla07 variants: The competition featured RANDOM, HANDMADE (CRAFTED), and INDUSTRIAL categories, and SATzilla07 targeted these distributions with category-specific or heterogeneous training data.Two submitted versions targeted RANDOM and HANDMADE; the ALL version used all three categories.
  • SATzilla07 variants: The authors submitted three SATzilla07 versions and omitted an INDUSTRIAL submission because of time constraints and the three-submission team limit.An INDUSTRIAL version was built after the deadline and its results were reported later.
  • Construction methodology: All SATzilla07 solvers followed the portfolio design methodology described earlier.The construction section organizes its subsections around the methodology’s steps.
  • Training data: The training data combined instances from SAT Competitions 2002–2005 and the 2006 SAT Race, yielding 4,811 instances overall.The 2006 SAT Race contributed only INDUSTRIAL instances.
  • Training data: Data were randomly split 40:30:30 into training, validation, and test sets, with the test set reserved for final reported results.Parameter tuning and intermediate model testing used the validation set.
  • Training data: The study denoted category-specific data sets as D_r, D_h, and D_i, while D represented the combined ALL data set.These labels treated the data set as an input parameter to SATzilla.

3.2 Selecting Solvers

SATzilla07 selected seven high-performance candidate solvers from prior competition results, emphasizing solvers that performed best on subsets of instances. Preprocessing was evaluated but excluded because it did not materially improve performance.

  • Seven high-performance solvers were selected as SATzilla07 candidates after identifying algorithms that performed best on subsets of competition instances.The selection considered both satisfiable and unsatisfiable instances and the cost of misclassifications.
  • Performance differences with Hypre preprocessing were smaller than 1% for solved instances, runtime, and SAT competition score, so preprocessing was dropped.The differences were also not consistently favorable to preprocessing.

3.3 Choosing Features

SATzilla07 uses instance features chosen to predict solver-specific hardness while remaining inexpensive to compute. Its feature set derives from 84 SAT features organized into structural, probing, and search-based categories, with expensive features removed.

  • Useful features must correlate with solver-specific instance hardness while being cheap enough that their computation does not dominate runtime.Feature computation time counts as part of SATzilla07’s runtime.
  • SATzilla07 starts from 84 SAT-instance features grouped into nine categories, including problem size, graph structure, balance, Horn proximity, LP-based, DPLL probing, and local-search probing.The categories also include variable-clause, variable, and clause graph features.
  • Problem-size and graph features summarize clause and variable counts, their ratio, and degree statistics for variable-clause, variable, and clause graphs.The graph statistics include means, variation coefficients, minima, maxima, and entropy where specified.
  • Balance and Horn-proximity features measure literal-sign distributions, clause types, Horn-clause fractions, and variable occurrences in Horn clauses.These features use summary statistics such as means, variation coefficients, extrema, and entropy.
  • DPLL and local-search probing features capture unit propagation, estimated search-space size, progress toward local minima, and variability in unsatisfied clauses.The probing set includes SAPS and GSAT-derived measurements.

3.4 Computing Features and Runtimes

Experiments used a 55-machine cluster and followed SAT Competition-style censored runtime measurement with a 1 200 CPU-second cutoff.

  • Experiments ran on 55 dual-CPU machines with 2GB RAM under Suse Linux 10.1, and solver runs exceeding the cutoff were aborted and censored.Timeouts were recorded as runs completing at the cutoff time for runtime calculations.
  • The experiments used a cutoff time of 1 200 CPU seconds to keep computational cost manageable.

3.5 Identifying Pre-solvers

SATzilla07 used brief unconditional pre-solvers to solve easy instances before feature computation. March dl04 was used for RANDOM, HANDMADE, and ALL, while Rsat 1.03 was used for INDUSTRIAL.

  • March dl04 and SAPS were selected as pre-solvers for RANDOM, HANDMADE, and ALL based on training runtime data.Pre-solvers run briefly and unconditionally before features are computed.
  • 47.8%, 47.7%, and 43.4% of RANDOM, HANDMADE, and ALL instances were solved by March dl04 within 5 CPU seconds.
  • SAPS solved 28.8%, 5.3%, and 14.5% of the remaining RANDOM, HANDMADE, and ALL instances within 2 CPU seconds.Its runtime was almost completely uncorrelated with March dl04, with Pearson correlation coefficient r = 0.118 for 487 instances solved by both.
  • Rsat 1.03 solved 32.0% of INDUSTRIAL instances within 2 CPU seconds and was used there instead of SAPS.SAPS solved less than 3% of the remaining INDUSTRIAL instances within that interval.

3.6 Identifying the Backup Solver

SATzilla07 evaluated its solvers using average runtime with timeouts counted at the 1,200-CPU-second cutoff. March dl04 was the best single solver for ALL, RANDOM, and HANDMADE.

  • 1,200 CPU seconds is the cutoff used when computing average runtime, with timeouts counted as completed runs at that limit.
  • March dl04 was the best single solver for ALL, RANDOM, and HANDMADE.

3.7 Learning Empirical Hardness Models

SATzilla07 learned empirical hardness models to predict solver runtimes and used exhaustive subset search to select component solvers for each data set.

  • SATzilla07 learned empirical hardness models for predicting each solver’s runtime, handling censored data and using hierarchical models.
  • Automatic exhaustive subset search determined which solvers to include in SATzilla07.
  • Table 3 reports the solvers selected for each of the four data sets.

4. Evaluation I: Performance Analysis of SATzilla07

SATzilla07 was evaluated in the 2007 SAT Competition and against component solvers across RANDOM, HANDMADE, INDUSTRIAL, and ALL data sets. It generally outperformed the strongest single solver, while feature computation was a notable cost for INDUSTRIAL instances.

  • SATzilla07 versions were evaluated in the 2007 SAT Competition and in detailed comparisons against their component solvers.
  • Three SATzilla07 versions were submitted to the 2007 SAT Competition, with category-specific training on RANDOM, HANDMADE, or ALL instances.
  • SATzilla07(S,Dh) won the HANDMADE SAT+UNSAT and UNSAT subcategories and placed second in SAT.
  • The general SATzilla07(S,D) solver solved more instances across the union of all three categories than any other solver.
  • 19% of INDUSTRIAL instances timed out during feature computation at the 60-CPU-second limit, requiring the backup solver.
  • Average feature computation times were 3.01, 4.22, and 14.4 CPU seconds for RANDOM, HANDMADE, and INDUSTRIAL, respectively.
  • On RANDOM, SATzilla07 was more than three times faster on average than March dl04 and solved 20% more instances within the cutoff.
  • On HANDMADE, SATzilla07’s average runtime was about 45% lower than its best component solver, and it solved 13% more instances than the best non-portfolio solver.

5. Design II: SATzilla Beyond 2007

SATzilla07 was extended with automated pre-solver and subset selection, score prediction, local-search integration, and hierarchical models for heterogeneous instances.

  • Automatically Selecting Pre-solvers: Manual pre-solver selection did not scale and ignored how pre-solvers change the training data and learned hardness models.Pre-solving can improve easy-instance scores, add runtime costs, and filter training data toward harder instances.
  • Automatically Selecting Pre-solvers: The automated procedure evaluates candidate pre-solvers, cutoff times, and execution orders, considering up to two pre-solvers.Candidates are selected from complete and local-search algorithms using validation scores, with cutoff times of 0, 2, 5, or 10 CPU seconds.
  • Randomized Solver Subset Selection: Randomized iterative improvement replaces exhaustive subset search when many component solvers make evaluating all 2^N subsets impractical.The procedure explores neighboring subsets formed by adding or dropping one solver and accepts validation-improving choices.
  • Predicting Performance Score: The score-learning approach is exact for solution and speed purse contributions but approximates the non-independent series purse.Series-purse scores depend on performance across other instances, motivating the independent approximation.
  • Predicting Performance Score: SATzilla can predict competition performance scores instead of runtimes, avoiding censored-data techniques because scores remain defined for timeouts and crashes.The 2007 competition’s series-purse component is approximated by an independent per-instance score so it can be modeled with supervised learning.

6. Construction II: Building the Improved SATzilla Versions

The improved SATzilla versions were constructed from expanded data and solver sets, automated pre-solvers, score models, and randomized component-subset selection.

  • Training and Evaluation Data: The expanded benchmark contains 5,680 instances across RANDOM, HANDMADE, and INDUSTRIAL categories, including 869 instances from the 2007 SAT Competition.The categories contain 2,811 RANDOM, 1,676 HANDMADE, and 1,193 INDUSTRIAL instances.
  • Training and Evaluation Data: The experiments compare data sets that differ in whether pre-2007 and 2007 instances are used for training, validation, and testing.D uses only pre-2007 data, D′ adds new instances to testing, and D+ combines old and new instances throughout.
  • Candidate Solvers: The candidate solver pool adds eight complete and four local-search solvers to the seven solvers used in SATzilla07.Candidate solver sets are treated as an input parameter of SATzilla.
  • SATzilla Versions: SATzilla07+ and SATzilla07* incorporate the new techniques, while intermediate versions isolate the effects of additional solvers, training data, and design changes.The versions are evaluated using identical test data for direct comparison.
  • Automated Construction: The improved systems automatically select pre-solvers and backup solvers, construct score-prediction models, and choose solver subsets using validation results.SATzilla07+ uses two underlying hierarchical models, whereas SATzilla07* uses more general hierarchical hardness models.

7. Evaluation II: Performance Analysis of the Improved SATzilla Versions

Across SAT categories, the improved SATzilla versions generally outperformed individual solvers, with the strongest gains from the new mechanisms and the general model on heterogeneous data.

  • RANDOM Category: 11% more instances solved, average runtime reduced by more than half, and score increased by over 50% after introducing SATzilla07+ mechanisms on RANDOM instances.Adding complete solvers and training data alone produced little improvement; the score-optimizing variants also exceeded non-portfolio solvers in score.
  • RANDOM Category: Local-search solvers achieved higher overall scores than complete solvers on RANDOM instances despite solving fewer instances and none of the unsatisfiable instances.Their advantage was attributed to excellent performance on satisfiable instances under the competition scoring function.
  • INDUSTRIAL Category: SATzilla07+ outperformed the best INDUSTRIAL component solver by 17% in average runtime, 7.2% in solved instances, and 11.5% in score.The best component solver solved 85.9% of instances within the 1,200-CPU-second cutoff.
  • ALL Category: SATzilla07* solved about 30% more instances than the best non-portfolio solver, March dl04, on ALL.Its runtime cumulative distribution function dominated the other SATzilla versions.

8. Conclusions

SATzilla extends per-instance SAT algorithm selection into an automated portfolio that combines complementary solvers and improves performance across broad benchmark sets.

  • Conclusions: SATzilla portfolios consistently outperformed their component solvers across four large sets of SAT competition instances.The 2007 SAT Competition independently demonstrated the practical effectiveness of the approach.
  • Conclusions: The extended approach optimizes complex scoring functions, integrates local-search components, and automates pre-solver selection.Extensive computational experiments showed substantial performance improvements over SATzilla07.
  • Conclusions: SATzilla can be applied out of the box from component solvers and representative training and validation instances, with solver choices determined automatically.The remaining computational bottleneck is running possible component solvers on representative instances.
  • Conclusions: Local-search components substantially boosted performance on RANDOM, improved INDUSTRIAL results, and weakened performance on HANDMADE instances.The authors identify better understanding of features and instance categorizations as a route to further improvement.
  • Conclusions: SATzilla’s performance depends on the strength of its component solvers and can benefit from solvers that are competitive only for particular instance types.Identifying additional specialized solvers could further improve portfolio performance.
Loading 1111.2249v1…