Research map / Learning theory and algorithms / Combinatorial and search optimization
Better Understandings and Configurations in MaxSAT Stochastic Local Search Solvers via Anytime Performance Analysis
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Introduces ECDF-based anytime performance assessment of four MaxSAT stochastic local search solvers and shows that using an AUC-style anytime cost function in SMAC tuning yields better configurations than fixed-budget costs.
Problem
Existing MaxSAT solver comparisons rely on best-found solution quality at fixed cutoff times, which hides convergence behavior and anytime performance; tuning is likewise typically driven by fixed-budget fitness.
Approach
Apply empirical cumulative distribution functions (ECDF) and their area under the curve (AUC) over multiple cutoff times, aggregated across instances, as a ratio-scaled anytime metric for comparing MaxSAT SLS solvers and as a cost function for SMAC hyperparameter tuning.
Key results
- NuWLS achieves the highest aggregated ECDF on all four tracks (e.g., 0.584 on MSE23-w vs. 0.409 for SATLike3.0), with ECDFs separating solvers that tie on fixed-budget scores.
- Tuning SMAC with the AUC cost function gives the best anytime performance in six of eight solver-track scenarios and the best score in five of eight.
- When tuning NuWLS and SATLike, the AUC cost function gives average gains of about 4% and 15% over the second-best cost function.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use AUC rather than a fixed-budget cost function to tune solver configurations | SMAC configurations for MaxSAT SLS solvers · MSE23-w and MSE23-uw | ECDF: best anytime performance for six out of eight scenarios | Helped |
| Use AUC rather than a fixed-budget cost function to tune solver configurations | SMAC configurations for MaxSAT SLS solvers · MSE23-w and MSE23-uw | Score: best results for five out of eight scenarios | Helped |
| Tune NuWLS using AUC rather than the fixed-budget cost | NuWLS · MSE23-w and MSE23-uw | Score: 4% | Helped |
| Tune SATLike using AUC rather than the fixed-budget cost | SATLike · MSE23-w and MSE23-uw | Score: 15% | Helped |
| Use AUC rather than a fixed-budget cost function to tune | MaxSAT SLS configurations · Five out of 16 tested scenarios where AUC was not best | Score or ECDF: 0.6% | Hurt |
| Use AUC instead of Best-f or Norm-f as the tuning cost | SMAC for MaxSAT solvers · MSE23-w and MSE23-uw | configuration performance: around 10%; 11 out of 16 tested scenarios | Helped |
| Normalize AUC and Norm-f across 20 instances before evaluating a configuration (ablation) | SMAC cost function for MaxSAT solvers · MaxSAT solver configuration | configuration performance | No clear effect |
| Compare solvers using anytime ECDF rather than fixed-budget score | MaxSAT SLS solvers · Individual MaxSAT instances | performance discrimination | Helped |
| Use anytime analysis rather than fixed-budget comparison | MaxFPS and BandMax · Weighted MaxSAT | ECDF: 10s | Mixed |
| Use anytime analysis to examine per-instance convergence | NuWLS · Decision-tree instances | ECDF: around 10s | Hurt |
Surprising findings
- Normalizing AUC or Norm-f values averaged across multiple instances as the HPO cost does not help configure MaxSAT solvers.
- The relative ranking of BandMax and MaxFPS flips over time, and NuWLS can be trapped in local optima on some instance families after about 10s.
Limitations
- Only four SLS solvers and MaxSAT Evaluation tracks are assessed; hybrid complete solvers are not analyzed.
- HPO experiments use 20% of instances for training and a small per-configuration budget of 100s, validated at 300s.
- Fixed-target performance is not assessed because optima of MaxSAT instances are unknown.
Experimental setup
Datasets: MaxSAT Evaluation 2022 anytime track instances MaxSAT Evaluation 2023 anytime track instances
Benchmarks: MSE23-w MSE23-uw MSE22-w MSE22-uw
Metrics: number of winning instances score based on best-found solution cost ECDF AUC
Baselines: SATLike3.0 BandMax MaxFPS NuWLS Best-f cost function Norm-f cost function
Builds on: SATLike3.0 NuWLS MaxFPS BandMax SMAC
Closest papers by meaning
- Farsighted Probabilistic Sampling: A General Strategy for Boosting Local Search MaxSAT Solvers (AAAI 2023 · similarity 0.92)
- Reactive Dialectic Search Portfolios for MaxSAT (AAAI 2017 · similarity 0.88)
- Enhance Diversified Top-k MaxSAT Solving by Incorporating New Strategy for Generating Diversified Initial Assignments (Student Abstract) (AAAI 2024 · similarity 0.85)
- Improving the Lower Bound in Branch-and-Bound Algorithms for MaxSAT (AAAI 2025 · similarity 0.85)
- Theoretical and Empirical Analysis of Cost-Function Merging for Implicit Hitting Set WCSP Solving (AAAI 2024 · similarity 0.85)
- Automatic Core-Guided Reformulation via Constraint Explanation and Condition Learning (AAAI 2024 · similarity 0.84)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.