Research map / Learning theory and algorithms / Combinatorial and search optimization
Improving the Lower Bound in Branch-and-Bound Algorithms for MaxSAT
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.
Proposes an unlocking mechanism that lets soft clauses in already-detected cores be reused for finding further disjoint cores in BnB MaxSAT lookahead, keeping the lower bound sound, and integrates it into MaxCDCL and WMaxCDCL.
Problem
Branch-and-bound MaxSAT solvers compute lower bounds by detecting disjoint cores via unit propagation, but soft clauses in already detected cores are locked and cannot be reused, limiting the number of cores found and the tightness of the lower bound.
Approach
Unlock soft literals (or locked weight in the weighted case) of a core once enough of its literals are falsified during unit propagation, allowing reuse for new cores; new cores merge the unlocked cores, and the weight/locked-weight bookkeeping keeps the LB sound for both unweighted and weighted MaxSAT.
Key results
- MaxCDCL+Unlock solves 1427 unweighted instances vs 1397 for MaxCDCL across MSE19-23 subsets (Table 1 sums), and WMaxCDCL+Unlock solves 1446 vs 1416 weighted.
- WMaxCDCL+Unlock won the first two places in the exact unweighted category of MaxSAT Evaluation 2024 among 15 participant solvers.
- Unlocking increases solved instances in the M23 portfolio from 1523 to 1536 (unweighted) and W23 portfolio from 1572 to 1578 (weighted).
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Add the unlocking mechanism to MaxCDCL | MaxCDCL · Unweighted total | instances solved: 1397 -> 1427 | Helped |
| Add the unlocking mechanism to WMaxCDCL | WMaxCDCL · Weighted total | instances solved: 1416 -> 1446 | Helped |
| Add the unlocking mechanism to MaxCDCL | MaxCDCL · Unweighted 19∩20 | instances solved: 102 -> 102 | No clear effect |
| Add the unlocking mechanism to MaxCDCL | MaxCDCL · Unweighted 19 | instances solved: 322 -> 331 | Helped |
| Add the unlocking mechanism to WMaxCDCL | WMaxCDCL · Weighted 20 | instances solved: 315 -> 326 | Helped |
Surprising findings
- Naive extension of the unlocking mechanism to weighted MaxSAT can yield a smaller lower bound than without unlocking (Example 2), motivating the more complex weight bookkeeping.
Limitations
- Benefit concentrated on instances with high percentage of soft conflicts; the second-stage success rate is low (9%) for instances with few soft conflicts.
- Weighted extension is considerably more complex and a soft literal can belong to multiple cores, so the simple unweighted guarantee does not hold.
- Gains are modest (e.g., 1-13 extra instances per benchmark group) relative to the strong baselines.
Experimental setup
Datasets: MaxSAT Evaluation 2019-2023 exact track instances
Benchmarks: MaxSAT Evaluation 2019-2023 unweighted and weighted exact track instances MaxSAT Evaluation 2024
Metrics: number of instances solved within 3600s timeout number of extra instances solved cactus plot
Baselines: MaxCDCL WMaxCDCL MaxCDCL-S6-HS9 WMaxCDCL-S6-HS12 EvalMaxSAT-SCIP CASHWMAXSAT-CorePlus
Builds on: MaxCDCL WMaxCDCL MaxSatz unit-propagation core detection
Closest papers by meaning
- Improved Algorithms for Maximum Satisfiability and Its Special Cases (AAAI 2023 · similarity 0.92)
- Ordered Objectives in Maximum Satisfiability (AAAI 2026 · similarity 0.91)
- Parameterization of (Partial) Maximum Satisfiability above Matching in a Variable-Clause Graph (AAAI 2024 · similarity 0.87)
- Enhance Diversified Top-k MaxSAT Solving by Incorporating New Strategy for Generating Diversified Initial Assignments (Student Abstract) (AAAI 2024 · similarity 0.86)
- Automatic Core-Guided Reformulation via Constraint Explanation and Condition Learning (AAAI 2024 · similarity 0.86)
- Better Understandings and Configurations in MaxSAT Stochastic Local Search Solvers via Anytime Performance Analysis (AAAI 2025 · similarity 0.85)
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.