Simple redundancy rules for MaxSAT

Ilario Bonacina
ilario.bonacina@upc.edu

Universitat Politècnica de Catalunya

January 16, 2026

This talk is based on a couple of joint works with

  • Maria Luisa Bonet
  • Massimo Lauria
  • Sam Buss.

The context

Redundancy rules
adding clause C to a database of clauses \Gamma


  • \Gamma \land C satisfiable iff \Gamma satisfiable

  • models preprocessing / inprocessing in SAT

  • studied from proof complexity perspective

  • what about MaxSAT?

This talk

Simple proof systems for MaxSAT redundancy
  • extension/modification of proof systems RAT/LPR, SPR, PR, SR …
  • polynomially verifiable
  • proof power only depends on the redundancy rule
  • MAIN GOAL: amenable to proof complexity analysis
  • BONUS: maybe easy to integrate with tools as dpr-trim

SAT redundancy as wlog reasoning

\Gamma database of clauses
C a clause

We want to certify that \Gamma and \Gamma\land C are equisatisfiable.

A proof of this fact is a substitution \sigma that uniformly fixes all problematic assignments:

for every \alpha satisfying \Gamma, either

  • \alpha satisfies \Gamma\land C, or
  • if \alpha satisfies \Gamma\land \overline C, then \alpha\circ \sigma satisfies \Gamma\land C, i.e. \displaystyle \Gamma\land \overline C\ {\color{red}{\models}}\ (\Gamma\land C)|_{\overline C \circ \sigma}

How to check \color{red}{\models}?

Use some proxy: \vdash_1 instead of \color{red}{\models}

Rule name \sigma
Substitution Redundancy (SR) \sigma : \{ variables \} \to \{ literals \} \cup \{ 0,1 \}
Propagation Red. (PR) \sigma is a partial assignment
Set Propagation Red. (SPR) \sigma only sets variables in C
Literal Propagation Red. (LPR, RAT) \sigma only sets one variable in C

SR = “Strongest Rule”

LPR = “Least Powerful Rule”

SR proof system = Resolution + SR rule

  • \sim for the other rules

  • super-poly lower bunds for LPR (and SBC)



This talk
  • no new variables (otherwise all systems are \equiv EF)
  • no deletions

Figure from (Buss and Thapen 2021)

Redundancy in MaxSAT

\underbrace{H_1\land H_2 \land H_3 \land \dots}_{\text{hard clauses}} \quad\land\quad \underbrace{\color{blue}{S_1} \land \color{blue}{S_2} \land \color{blue}{S_3} \land \color{blue}{\dots}}_{\color{blue}{\text{soft clauses}}}

cost(\Gamma) = min # of soft clauses we need to falsify

C is redundant wrt \Gamma iff cost(\Gamma \land C) = cost(\Gamma),
i.e. some optimal solution of \Gamma satisfies C

Certifiable with SR/PR/SPR/LPR & simple modifications

i-SR/i-PR/i-SPR/i-LPR

i = inclusion

i-SR rule = same as SR but instead of \vdash_1 use \supseteq (as multisets), i.e
need to check \displaystyle \Gamma|_{\overline C}\supseteq_m (\Gamma\land C)|_{\overline C\circ \sigma}

MaxSAT Resolution + i-SR rule

  • \Gamma\cup\{C\lor x,C\lor \lnot x\}\leadsto \Gamma\cup\{C\}
  • \Gamma\cup\{C\}\leadsto \Gamma\cup\{C\lor x,C\lor \lnot x\}
  • \Gamma \leadsto \Gamma\cup\{C\} if C is i-SR w.r.t. \Gamma
  • \Gamma\cup\{C\} \leadsto \Gamma if C is i-SR w.r.t. \Gamma

F\leadsto ... \leadsto \{\underbrace{\bot,\dots,\bot}_k, ...\}

MaxSAT-Resolution + i-SR is already quite strong

  • efficiently proves the optimal cost of some hard tautologies (\mathsf{PHP}^{m}_{n}, \mathsf{Parity}_n, F[\oplus^m])
  • the proof of the optimal cost of \mathsf{PHP}^{m}_{n} is \sim (Heule, Kiesl, and Biere 2019) but adapted to the context of the substitution rules of MaxSAT-Resolution
  • Captures simple Branch-and-Bound procedures
  • Open: size lower bounds for MaxSAT-Resolution + i-SPR

cost-SR/cost-PR/cost-SPR/cost-LPR

\underbrace{H_1\land H_2 \land H_3 \land \dots \land (S_1\lor {\color{blue}{b_1}}) \land (S_2\lor {\color{blue}{b_2}})\land \dots}_{\text{hard clauses}}

cost(\alpha)= \sum_i \alpha({\color{blue}{b_i}})

cost-SR rule = same as SR but also check a cost condition:
whenever \alpha falsifies C, cost(\alpha\circ \sigma)\leq cost(\alpha), i.e. \left.(\sum_i b_i - \sigma(b_i))\right|_{\overline C}\geq 0

Resolution + cost-SR rule

A derivation of \color{blue}{b_{i_1}}, \color{blue}{b_{i_2}}, \dots, \color{blue}{b_{i_k}} certifies that cost(\alpha)\geq k for every \alpha.

  • for the cost-condition to be sound it would be enough:
    whenever \alpha falsifies C and \alpha satisfies \Gamma, cost(\alpha\circ \sigma)\leq cost(\alpha), but with the red part this is not polytime checkable
  • symmetry breaking is it useful in SAT-solving, but here it is a necessity.
    E.g. b_1\lor b_2, b_3\lor b_4, b_5\lor b_6, …
    Mitigation: disjoint sets of b_is, minimum HS …
  • cost condition can be checked in parallel, and separately from redundancy

Some results on Resolution + cost-SR/cost-PR/…

  • Resolution + cost-SR has short proofs of the optimal cost of \mathsf{PHP}^m_n
  • if cost(F)=1 and F has a short refutation in PR, then Resolution + cost-PR has a short proof of optimal cost of F
  • Resolution + cost-SPR is complete
    (proof sketch) use an optimal assignment as witness \sigma, to forbid every other assignment \alpha, add by redundancy the clause \lnot \alpha
  • Resolution + cost-LPR is incomplete!

Thm. There is a formula family F_n with \mathcal O(n) variables, \mathcal O(n) clauses and cost(F_n)=\Omega(n), where even to prove cost(F_n)\geq 1 any Resolution + cost-SR proof derives a clause C with witnessing substition \sigma s.t. \max_{\alpha : \alpha\supseteq \overline C} HammingDistance(\alpha, \alpha\circ\sigma)=\Omega(n)\ .

\implies Resolution + cost-LPR is incomplete, since \sigma can flip at most one variable.

\implies any Resolution + cost-SPR proof of F_n requires linear width, since \sigma can only flip variables inside C

Comparison with VeriPB

  • base language is cutting planes

  • focus on certification, hence very expressive by design:
    redundancy, dominance, extension variables, …

  • cost-redundancy and inclusion-redundancy of C are expressible in veriPB itself, hence can be certified by a veriPB proof

  • veriPB easily simulates Resolution + cost-SR and MaxSAT Resolution + i-SR

Comparison with (Ihalainen, Berg, and Järvisalo 2022)

  • systems for redundancy in MaxSAT \sim cost-SR/cost-PR/cost-SPR/cost-LPR

  • cost condition is cost(F\land C, \sigma)\leq cost(F,\sigma)\leq cost(F, \overline C):
    not polynomially cheackable, requires a SAT-call (i.e. additional proof)

  • poly-checkable subsystems CSPR, CLPR

cost vs inclusion redundancy

  • Proof systems for understanding redundancy in MaxSAT

  • Potentially simpler to analyze, i.e. good for theory

  • different types of restriction on SR rules
    one with \supseteq instead of \vdash_1 the other enforcing a cost-condition

  • i-SR rule applies directly to soft clauses

  • i-SR preserves # of falsified soft clauses

  • i-SR can be integrated with MaxSAT resolution.

Open: Does Resolution + cost-SR p-simulate MaxSat Resolution?

Open Problems

  • Does Resolution + cost-SR p-simulates MaxSAT Resolution?
  • size lower bounds for Resolution + cost-SPR
  • size lower bounds for MaxSAT Resolution + i-SPR

Thank you!

References

Bogaerts, Bart, Stephan Gocht, Ciaran McCreesh, and Jakob Nordström. 2023. “Certified Dominance and Symmetry Breaking for Combinatorial Optimisation.” Journal of Artificial Intelligence Research 77. https://doi.org/10.1613/jair.1.14296.
Bonacina, Ilario, Maria Luisa Bonet, Sam Buss, and Massimo Lauria. 2025. “Redundancy Rules for MaxSAT.” https://doi.org/10.4230/LIPIcs.SAT.2025.7.
Bonacina, Ilario, Maria Luisa Bonet, and Massimo Lauria. 2024. “MaxSAT Resolution with Inclusion Redundancy.” https://doi.org/10.4230/LIPIcs.SAT.2024.7.
Buss, Sam, and Neil Thapen. 2021. “DRAT and Propagation Redundancy Proofs Without New Variables.” Logical Methods in Computer Science Volume 17, Issue 2. https://doi.org/10.23638/LMCS-17(2:12)2021.
Heule, Marijn J. H., Benjamin Kiesl, and Armin Biere. 2019. “Strong Extension-Free Proof Systems.” Journal of Automated Reasoning 64 (3). https://doi.org/10.1007/s10817-019-09516-0.
Ihalainen, Hannes, Jeremias Berg, and Matti Järvisalo. 2022. “Clause Redundancy and Preprocessing in Maximum Satisfiability.” In Automated Reasoning, edited by Jasmin Blanchette, Laura Kovács, and Dirk Pattinson, 75–94. Cham: Springer International Publishing. https://doi.org/10.1007/978-3-031-10769-6_6.
Kołodziejczyk, Leszek Aleksander, and Neil Thapen. 2024. “The Strength of the Dominance Rule.” In SAT 2024. https://doi.org/10.4230/LIPIcs.SAT.2024.20.
Kullmann, O. 1999. “On a Generalization of Extended Resolution.” Discrete Applied Mathematics. https://doi.org/https://doi.org/10.1016/S0166-218X(99)00037-2.