SATzilla: Portfolio-based Algorithm Selection for SAT
arXiv:1111.2249 · doi:10.1613/jair.2490
Abstract
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 corpus (2)
Cited by in corpus (88)
- ParamILS: An Automatic Algorithm Configuration Framework
- SATzilla: Portfolio-based Algorithm Selection for SAT
- Learning a SAT Solver from Single-Bit Supervision
- Metaheuristics "In the Large"
- Benchmarking in Optimization: Best Practice and Open Issues
- First Three Years of the International Verification of Neural Networks Competition (VNN-COMP)
- Landscape-Aware Fixed-Budget Performance Regression and Algorithm Selection for Modular CMA-ES Variants
- Algorithm Runtime Prediction: Methods & Evaluation
- Fast counting with tensor networks
- Black-Box Optimization Revisited: Improving Algorithm Selection Wizards through Massive Benchmarking
- Deciding the Consistency of Non-Linear Real Arithmetic Constraints with a Conflict Driven Search Using Cylindrical Algebraic Coverings
- A Multi-Engine Approach to Answer Set Programming
- Relaxed Survey Propagation for The Weighted Maximum Satisfiability Problem
- Scheduling with Predictions and the Price of Misprediction
- LLAMA: Leveraging Learning to Automatically Manage Algorithms
- Machine Learning Methods in Solving the Boolean Satisfiability Problem
- The Maximum Common Subgraph Problem: A Portfolio Approach
- Optimal Decision Trees for the Algorithm Selection Problem: Integer Programming Based Approaches
- Benchmarking Feature-based Algorithm Selection Systems for Black-box Numerical Optimization
- Machine Learning for Electronic Design Automation: A Survey
- Comparing machine learning models to choose the variable ordering for cylindrical algebraic decomposition
- Machine Learning for Mathematical Software
- Extreme Algorithm Selection With Dyadic Feature Representation
- Efficiently Coupling the I-DLV Grounder with ASP Solvers
- Boosting Combinatorial Problem Modeling with Machine Learning
- MAPFAST: A Deep Algorithm Selector for Multi Agent Path Finding using Shortest Path Embeddings
- A Case Study in Complexity Estimation: Towards Parallel Branch-and-Bound over Graphical Models
- Using Sequential Runtime Distributions for the Parallel Speedup Prediction of SAT Local Search
- Machine learning for constraint solver design -- A case study for the alldifferent constraint
- Predicting SMT Solver Performance for Software Verification
- Algorithmically generating new algebraic features of polynomial systems for machine learning
- Algorithm Selection for Combinatorial Search Problems: A Survey
- Exploratory Landscape Analysis is Strongly Sensitive to the Sampling Strategy
- A Multicore Tool for Constraint Solving
- Learning-Theoretic Foundations of Algorithm Configuration for Combinatorial Partitioning Problems
- Sample Complexity of Tree Search Configuration: Cutting Planes and Beyond
- PDP: A General Neural Framework for Learning Constraint Satisfaction Solvers
- Improved cross-validation for classifiers that make algorithmic choices to minimise runtime without compromising output correctness
- Restart Strategy Selection using Machine Learning Techniques
- Experience-based Optimization: A Coevolutionary Approach
- Guiding High-Performance SAT Solvers with Unsat-Core Predictions
- Improving Nevergrad's Algorithm Selection Wizard NGOpt through Automated Algorithm Configuration
- From Shallow to Deep Interactions Between Knowledge Representation, Reasoning and Machine Learning (Kay R. Amel group)
- Optimizing Monotone Chance-Constrained Submodular Functions Using Evolutionary Multi-Objective Algorithms
- On Predictive Modeling for Optimizing Transaction Execution in Parallel OLTP Systems
- Few-shots Parallel Algorithm Portfolio Construction via Co-evolution
- Algorithm Portfolio for Individual-based Surrogate-Assisted Evolutionary Algorithms
- Phase Selection Heuristics for Satisfiability Solvers
- Learning Branching Heuristics for Propositional Model Counting
- Constraint Solving with Deep Learning for Symbolic Execution
- Lessons on Datasets and Paradigms in Machine Learning for Symbolic Computation: A Case Study on CAD
- Encoding Selection for Solving Hamiltonian Cycle Problems with ASP
- ASlib: A Benchmark Library for Algorithm Selection
- Automatic Construction of Parallel Portfolios via Explicit Instance Grouping
- The DEWCAD Project: Pushing Back the Doubly Exponential Wall of Cylindrical Algebraic Decomposition
- claspfolio 2: Advances in Algorithm Selection for Answer Set Programming
- sunny-as2: Enhancing SUNNY for Algorithm Selection
- ML + FV = ? A Survey on the Application of Machine Learning to Formal Verification
- Structured Factored Inference: A Framework for Automated Reasoning in Probabilistic Programming Languages
- Solving MaxSAT by Successive Calls to a SAT Solver
- Automated Aggregator -- Rewriting with the Counting Aggregate
- Reliability of Computational Experiments on Virtualised Hardware
- Elastic Solver: Balancing Solution Time and Energy Consumption
- Feature-Based Diversity Optimization for Problem Instance Classification
- Towards Feature-free TSP Solver Selection: A Deep Learning Approach
- MaLeS: A Framework for Automatic Tuning of Automated Theorem Provers
- Model Counting meets F0 Estimation
- Siamese Meta-Learning and Algorithm Selection with 'Algorithm-Performance Personas' [Proposal]
- Pilot, Rollout and Monte Carlo Tree Search Methods for Job Shop Scheduling
- Proceedings Second International Workshop on Formal Integrated Development Environment
- Semi-bandit Optimization in the Dispersed Setting
- Measuring Similarity of Graphs and their Nodes by Neighbor Matching
- QROSS: QUBO Relaxation Parameter Optimisation via Learning Solver Surrogates
- Modelling Constraint Solver Architecture Design as a Constraint Problem
- Simple Hyper-heuristics Control the Neighbourhood Size of Randomised Local Search Optimally for LeadingOnes
- Evolving Real-Time Heuristics Search Algorithms with Building Blocks
- On Constructing Algorithm Portfolios in Algorithm Selection for Computationally Expensive Black-box Optimization in the Fixed-budget Setting
- Zero Training Overhead Portfolios for Learning to Solve Combinatorial Problems
- Automatically selecting inference algorithms for discrete energy minimisation
- A PAC Approach to Application-Specific Algorithm Selection
- Concurrent Cube-and-Conquer
- Deep Optimization for Spectrum Repacking
- Transformation-based Feature Computation for Algorithm Portfolios
- Solver Scheduling via Answer Set Programming
- Ranking Algorithms by Performance
- The Multi-engine ASP Solver ME-ASP: Progress Report
- Using Volunteer Computing for Mounting SAT-based Cryptographic Attacks
- Using machine learning to make constraint solver implementation decisions