Relaxed Survey Propagation for The Weighted Maximum Satisfiability Problem

The identification of performance-optimizing parameter settings is an important part of the development and application of algorithms. We describe an automatic framework for this algorithm configuration problem. More formally, we provide methods for optimizing a target algorithm's performance on a given class of problem instances by varying a set of ordinal and/or categorical parameters. We review a family of local-search-based algorithm configuration procedures and present novel techniques for accelerating them by adaptively limiting the time spent for evaluating individual configurations. We describe the results of a comprehensive experimental evaluation of our methods, based on the configuration of prominent complete and incomplete algorithms for SAT. We also present what is, to our knowledge, the first published work on automatically configuring the CPLEX mixed integer programming solver. All the algorithms we considered had default parameter settings that were manually identified with considerable effort. Nevertheless, using our automated algorithm configuration procedures, we achieved substantial and consistent performance improvements.

• Publication year

  2009

• Venue

  Journal of Artificial Intelligence Research

• Publication date

  2009-09-01

• Fields of study

  Mathematics, Computer Science

• Identifiers
  DOI 10.1613/jair.2808arXiv 1401.3483
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Data Structures

  2011cited by this paper
• A machine program for theorem-proving

  2011cited by this paper
• Tradeoffs in the empirical evaluation of competing algorithm designs

  2010cited by this paper
• Experimental Research in Evolutionary Computation - The New Experimentalism

  2010cited by this paper
• An experimental investigation of model-based parameter optimisation: SPO and beyond

  2009cited by this paper
• Buyer Power in International Markets

  2009cited by this paper
• SATenstein: Automatically Building Local Search SAT Solvers from Components

  2009cited by this paper
• An automatically configured modular algorithm for post enrollment course timetabling

  2009cited by this paper
• Automated configuration of algorithms for solving hard computational problems

  2009cited by this paper
• Message-passing and local heuristics as decimation strategies for satisfiability

  2009influential reference
• A strong conic quadratic reformulation for machine-job assignment with controllable processing times

  2009influential reference
• SATzilla: Portfolio-based Algorithm Selection for SAT

  2008cited by this paper
• Relaxed Survey Propagation: A Sum-Product Algorithm for Max-SAT

  2008influential reference
• Understanding the role of noise in stochastic local search: Analysis and experiments

  2008cited by this paper
• Reactive Search and Intelligent Optimization

  2008cited by this paper
• Structural Abstraction of Software Verification Conditions

  2007cited by this paper
• Boosting Verification by Automatic Tuning of Decision Procedures

  2007influential reference
• Cooled and Relaxed Survey Propagation for MRFs

  2007cited by this paper
• Automatic Algorithm Configuration Based on Local Search

  2007cited by this paper
• A replica exchange Monte Carlo algorithm for protein folding in the HP model

  2007cited by this paper
• Efficient parameter estimation for RNA secondary structure prediction

  2007cited by this paper
• Learning Restart Strategies

  2007cited by this paper
• et de Développements en Intelligence Artificielle

  2007cited by this paper
• Survey Propagation Revisited

  2007cited by this paper
• Preface to the Special Volume on the SAT 2005 Competitions and Evaluations

  2006cited by this paper
• Finding Optimal Algorithmic Parameters Using Derivative-Free Optimization

  2006cited by this paper
• Performance Prediction and Automated Tuning of Randomized and Parametric Algorithms

  2006cited by this paper
• Method-specific dynamic compilation using logistic regression

  2006cited by this paper
• RSat 2.0: SAT Solver Description

  2006cited by this paper
• Detecting Disjoint Inconsistent Subformulas for Computing Lower Bounds for Max-SAT

  2006cited by this paper
• Dynamic Algorithm Portfolios

  2006cited by this paper
• Using machine learning to focus iterative optimization

  2006cited by this paper
• Clustering of solutions in the random satisfiability problem

  2005cited by this paper
• Pairs of SAT Assignment in Random Boolean Formulae

  2005cited by this paper
• Efficient Stochastic Local Search for MPE Solving

  2005cited by this paper
• Benchmarking SAT Solvers for Bounded Model Checking

  2005influential reference
• Resolution in Max-SAT and its relation to local consistency in weighted CSPs

  2005cited by this paper
• Constructing free-energy approximations and generalized belief propagation algorithms

  2005cited by this paper
• Learning by message-passing in networks of discrete synapses

  2005cited by this paper
• APPLYING MACHINE LEARNING TO LOW‐KNOWLEDGE CONTROL OF OPTIMIZATION ALGORITHMS

  2005cited by this paper
• Evolving Evolutionary Algorithms Using Linear Genetic Programming

  2005cited by this paper
• Using CBR to Select Solution Strategies in Constraint Programming

  2005cited by this paper
• Three Truth Values for the SAT and MAX-SAT Problems

  2005cited by this paper
• Existential arc consistency: Getting closer to full arc consistency in weighted CSPs

  2005cited by this paper
• Rigorous location of phase transitions in hard optimization problems

  2005cited by this paper
• Minimizing energy below the glass thresholds.

  2004influential reference
• A new look at survey propagation and its generalizations

  2004influential reference
• UBCSAT: An Implementation and Experimentation Environment for SLS Algorithms for SAT & MAX-SAT

  2004influential reference
• A study of the lot-sizing polytope

  2004cited by this paper
• Fifty-Five Solvers in Vancouver: The SAT 2004 Competition

  2004cited by this paper
• The problem of tuning metaheuristics: as seen from the machine learning perspective

  2004cited by this paper
• Stochastic Local Search: Foundations & Applications

  2004cited by this paper
• Finding Optimal Algorithmic Parameters Using the Mesh Adaptive Direct Search Algorithm

  2004cited by this paper
• Generic Online Optimization of Multiple Configuration Parameters with Application to a Database Server

  2003cited by this paper
• The Design and Analysis of Computer Experiments

  2003cited by this paper
• Survey propagation as local equilibrium equations

  2003cited by this paper
• Introduction to stochastic search and optimization - estimation, simulation, and control

  2003cited by this paper
• The Essentials of the SAT 2003 Competition

  2003cited by this paper
• On the facets of the mixed–integer knapsack polyhedron

  2003influential reference
• Local Search on SAT-encoded Colouring Problems

  2003cited by this paper
• Survey propagation: An algorithm for satisfiability

  2002influential reference
• Learning the Empirical Hardness of Optimization Problems: The Case of Combinatorial Auctions

  2002cited by this paper
• The probabilistic analysis of a greedy satisfiability algorithm

  2002cited by this paper
• A Racing Algorithm for Configuring Metaheuristics

  2002influential reference
• Scaling and Probabilistic Smoothing: Efficient Dynamic Local Search for SAT

  2002cited by this paper
• Random K-satisfiability problem: from an analytic solution to an efficient algorithm.

  2002influential reference
• Dynamic restart policies

  2002cited by this paper
• A mixture-model for the behaviour of SLS algorithms for SAT

  2002cited by this paper
• The Cavity Method at Zero Temperature

  2002cited by this paper
• An adaptive noise mechanism for walkSAT

  2002cited by this paper
• Phase Transitions and Backbones of 3-SAT and Maximum 3-SAT

  2001cited by this paper
• Design of Iterated Local Search Algorithms

  2001cited by this paper
• Chaff: engineering an efficient SAT solver

  2001cited by this paper
• Auto-Walksat: A Self-Tuning Implementation of Walksat

  2001cited by this paper
• Factor graphs and the sum-product algorithm

  2001influential reference
• A Bayesian Approach to Tackling Hard Computational Problems (Preliminary Report)

  2001cited by this paper
• Iterated Local Search

  2001cited by this paper
• A backbone-search heuristic for efficient solving of hard 3-SAT formulae

  2001cited by this paper
• Using Experimental Design to Find Effective Parameter Settings for Heuristics

  2001cited by this paper
• Generalized Belief Propagation

  2000cited by this paper
• Towards a universal test suite for combinatorial auction algorithms

  2000cited by this paper
• Morphing: Combining Structure and Randomness

  1999cited by this paper
• Loopy Belief Propagation for Approximate Inference: An Empirical Study

  1999cited by this paper
• Evolution of Constraint Satisfaction strategies in examination timetabling

  1999cited by this paper
• A theoretician's guide to the experimental analysis of algorithms

  1999cited by this paper
• Stochastic local search for Bayesian network

  1999cited by this paper
• Approximating the unsatisfiability threshold of random formulas

  1998cited by this paper
• Efficient Global Optimization of Expensive Black-Box Functions

  1998cited by this paper
• Evidence for Invariants in Local Search

  1997cited by this paper
• Problem Structure in the Presence of Perturbations

  1997cited by this paper
• Heuristics based on unit propagation for satisfiability problems

  1997cited by this paper
• Adaptive Problem-solving for Large-scale Scheduling Problems: A Case Study

  1996cited by this paper
• Automatically configuring constraint satisfaction programs: A case study

  1996cited by this paper
• A Discrete Lagrangian-Based Global-Search Method for Solving Satisfiability Problems

  1996cited by this paper
• Noise Strategies for Improving Local Search

  1994cited by this paper
• Hoeffding Races: Accelerating Model Selection Search for Classification and Function Approximation

  1993cited by this paper
• Fundamentals of speech recognition

  1993cited by this paper
• An Analytic Learning System for Specializing Heuristics

  1993cited by this paper
• Minimizing Conflicts: A Heuristic Repair Method for Constraint Satisfaction and Scheduling Problems

  1992cited by this paper
• A New Method for Solving Hard Satisfiability Problems

  1992cited by this paper

• PID-based attitude control of quadrotor using robust pole assignment and LPV modeling

  2024cites this paper
• Optimizing local search-based partial MaxSAT solving via initial assignment prediction

  2024cites this paper
• Convergence analysis of a survey propagation algorithm

  2023cites this paper
• Nonlocal optimization of binary neural networks

  2022cites this paper
• Initial Solution Generation and Diversified Variable Picking in Local Search for (Weighted) Partial MaxSAT

  2022cites this paper
• Population management in metaheuristic algorithms: Could less be more?

  2021cites this paper
• Solving QAP with Auto-parameterization in Parallel Hybrid Metaheuristics

  2021cites this paper
• Leveraging cluster backbones for improving MAP inference in statistical relational models

  2020cites this paper
• An Improved ID3 classification algorithm for solving the backbone of proposition formulae

  2020cites this paper
• Efficient incident identification from multi-dimensional issue reports via meta-heuristic search

  2020cites this paper
• Hyper-parameter tuning for the (1 + (λ, λ)) GA

  2019cites this paper
• Estimating the Density of States of Boolean Satisfiability Problems on Classical and Quantum Computing Platforms

  2019cites this paper
• Improving the computational efficiency of stochastic programs using automated algorithm configuration: an application to decentralized energy systems

  2019cites this paper
• Building energy optimization: An extensive benchmark of global search algorithms

  2019cites this paper
• Collection of benchmark test problems for data reconciliation and gross error detection and identification

  2018cites this paper
• BRISE: Energy-Efficient Benchmark Reduction

  2018cites this paper
• Iterated Local Search: Framework and Applications

  2018cites this paper
• Towards building an automated bioinformatician: more accurate transcript assembly via parameter advising

  2018cites this paper
• A continuous-time MaxSAT solver with high analog performance

  2018cites this paper
• Empirical investigation of stochastic local search for maximum satisfiability

  2018cites this paper
• au Scoring Functions Based on Second Level Score for kSAT with Long Clauses

  2017cites this paper
• Hard Neighboring Variables Based Configuration Checking in Stochastic Local Search for Weighted Partial Maximum Satisfiability

  2017cites this paper
• Metalearning and Algorithm Selection: progress, state of the art and introduction to the 2018 Special Issue

  2017influential citation
• From Decimation to Local Search and Back: A New Approach to MaxSAT

  2017cites this paper
• CCEHC: An efficient local search algorithm for weighted partial maximum satisfiability

  2017cites this paper
• Sufficient conditions for convergence of the survey propagation algorithm

  2017cites this paper
• A Model-Based Scalability Optimization Methodology for Cloud Applications

  2017cites this paper
• Multilayer cognitive architecture for UAV control

  2016cites this paper
• Markov Chain methods for the Bipartite Boolean Quadratic Programming Problem

  2016cites this paper
• Population-based heuristic algorithms for continuous and mixed discrete-continuous optimization problems

  2015cites this paper
• Graphical models beyond standard settings: lifted decimation, labeling, and counting

  2015cites this paper
• Using Constraint Satisfaction Techniques and Variational Methods for Probabilistic Reasoning

  2015cites this paper
• An Empirical Study of Off-Line Configuration and On-Line Adaptation in Operator Selection

  2014cites this paper
• Symbolic Abstraction: Algorithms and Applications

  2014cites this paper
• An automatic algorithm selection approach for the multi-mode resource-constrained project scheduling problem

  2014cites this paper
• Scoring Functions Based on Second Level Score for k-SAT with Long Clauses

  2014cites this paper
• The taming of the shrew: increasing performance by automatic parameter tuning for java garbage collectors

  2014influential citation
• Using AI planning to automate the performance analysis of simulators

  2014cites this paper
• Clustering of search trajectory and its application to parameter tuning

  2013cites this paper
• Using automatic programming to generate state-of-the-art algorithms for random 3-SAT

  2013cites this paper
• Bandit-Based Search for Constraint Programming

  2013cites this paper
• Efficient planning through automatic configuration and machine learning

  2013cites this paper
• O planeamento de experiências no aperfeiçoamento de metaheuristicas

  2013cites this paper
• Automatic (offline) configuration of algorithms

  2013influential citation
• ParadisEO-MO: from fitness landscape analysis to efficient local search algorithms

  2013cites this paper
• Configuring simulation algorithms with ParamILS

  2012influential citation
• Computational results for an automatically tuned CMA-ES with increasing population size on the CEC’05 benchmark set

  2012influential citation
• Quantifying Homogeneity of Instance Sets for Algorithm Configuration

  2012cites this paper
• Planning with preferences using maximum satisfiability

  2012cites this paper
• Calibrating continuous multi-objective heuristics using mixture experiments

  2012cites this paper
• Qualitative modelling via constraint programming

  2012cites this paper
• Instance-based parameter tuning for evolutionary AI planning

  2011cites this paper
• DIMMA: A Design and Implementation Methodology for Metaheuristic Algorithms - A Perspective from Software Development

  2010cites this paper
• SPOT: An R Package For Automatic and Interactive Tuning of Optimization Algorithms by Sequential Parameter Optimization

  2010cites this paper
• An experimental investigation of model-based parameter optimisation: SPO and beyond

  2009cites this paper