Research map / Learning theory and algorithms / Combinatorial and search optimization
Parameterization of (Partial) Maximum Satisfiability above Matching in a Variable-Clause Graph
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.
Improves the parameterized algorithm for MaxSAT above maximum matching in the variable-clause graph to O*(2^{1.5k}) via a faster (n-k)-Set Cover algorithm using Gallai-Edmonds decomposition, extends it to Partial MaxSAT, and derives record bounds for (n,3)- and (n,4)-MaxSAT.
Problem
MaximumSatisfiability parameterized above the size of a maximum matching in the variable-clause graph (previous best O*(4^k)); also Partial MaxSAT with hard clauses and exact bounds for bounded-occurrence MaxSAT.
Approach
Reduces MaxSAT above matching to (n-k)-Set Cover and solves it with a dynamic programming over covered/uncovered elements, using Gallai-Edmonds decomposition to bound the size of connected components of the residual graph, giving O*(2^{1.5k}); extends via reduction/branching rules to Partial MaxSAT where hard clauses have length at most 2.
Key results
- Algorithm for (ν(F)+k)-SAT runs in O*(2^{1.5k}) (about 2.83^k), improving the previous O*(4^k).
- (n,3)-MaxSAT solvable in O*(1.14977^m) and (n,4)-MaxSAT in O*(1.27895^m), improving 1.1554^m and 1.2872^m.
- On generated instances the implemented solver outperforms the listed MaxSAT Evaluation 2022 solvers.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use the Gallai–Edmonds-based (n − k)-SET COVER algorithm | MAXSAT above maximum matching · MAXSAT above maximum matching | running time: O∗(4^k) -> O∗(2^{3k/2}) | Helped |
| Apply the improved above-matching algorithm | (n, 3)-MAXSAT · (n, 3)-MAXSAT | running time: O∗(1.1554k′), O∗(1.1554m) -> O∗(1.14977k′), O∗(1.14977m) | Helped |
| Apply the improved above-matching algorithm | (n, 4)-MAXSAT · (n, 4)-MAXSAT | running time: O∗(1.2872m) -> O∗(1.27895m) | Helped |
| Apply the improved above-matching algorithm | (n, 4)-MAXSAT · (n, 4)-MAXSAT | running time: O∗(1.3248k′) -> O∗(1.27895k′) | Helped |
| Adapt the algorithm to handle hard clauses of length at most 2 | Partial (ν(F) + k)-SAT · Hard clauses length at most 2 | running time: O∗(2^{3k/2}) | Helped |
| Adapt the algorithm to handle h hard clauses | Partial (ν(F) + k)-SAT · h hard clauses | running time: O∗(2^{3k/2} + 2^k · 1.12226^h) | Helped |
| Use the proposed solver instead of the competing solvers | Proposed MaxSAT solver · Generated tests | computational time | Helped |
Surprising findings
- Adding hard clauses of length at most 2 does not worsen the O*(2^{1.5k}) bound, though a single hard clause can make the problem exponentially harder in general.
Limitations
- Algorithm is efficient mainly when k is small; brute force can beat it on general instances.
- Solver lacks heuristics used in practical MaxSAT solvers, so it is slower on MaxSAT Evaluation 2022 instances with large parameter values.
- Partial MaxSAT with hard clauses longer than 2 only gets the extra term O*(2^k * 1.12226^h).
Experimental setup
Benchmarks: generated MaxSAT instances (a=20, k=10, 100<=b<=50000)
Metrics: running time (ms) worst-case time bound exponent
Baselines: Basavaraju et al. 2016 O*(4^k) Crowston et al. 2014 Brilliantov et al. 2023 (n,3)/(n,4)-MaxSAT bounds Xiao 2022 open-wbo max-hs cgss eval-max-sat exact uwr-max-sat
Builds on: Crowston et al. 2014 (MaxSAT above matching reduction to (n-k)-Set Cover) Basavaraju et al. 2016 (O*(4^k) for (n-k)-Set Cover) Brilliantov, Alferov, Bliznets 2023 Hopcroft-Karp matching Gallai-Edmonds decomposition
Closest papers by meaning
- Improved Algorithms for Maximum Satisfiability and Its Special Cases (AAAI 2023 · similarity 0.92)
- New Length Dependent Algorithm for Maximum Satisfiability Problem (AAAI 2021 · similarity 0.90)
- Ordered Objectives in Maximum Satisfiability (AAAI 2026 · similarity 0.89)
- Improving the Lower Bound in Branch-and-Bound Algorithms for MaxSAT (AAAI 2025 · similarity 0.87)
- SAT-Based Tree Decomposition with Iterative Cascading Policy Selection (AAAI 2024 · similarity 0.85)
- Hardness of Random Reordered Encodings of Parity for Resolution and CDCL (AAAI 2024 · 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.