RECORD
Redundancy rules for MaxSAT
Logic in Computer Science · Submitted 18 Nov 2025
abstract compiled · 2026-09-23 · no language-model review
The authors' main claim We conclude by discussing the integration of our rules with the MaxSAT resolution proof system, which is a commonly studied proof system for MaxSAT.
The compiled record
The paper's own sentences, arranged. Each label is drawn from a closed vocabulary; the number beside it is the probability the classifier gave that label. Numbers in the tables are the authors', checked by code. No sentence in this record was written by a model.
Open the compiled record
The abstract, sentence by sentence
The concept of redundancy in SAT leads to more expressive and powerful proof search techniques, e.g., able to express various inprocessing techniques, and originates interesting hierarchies of proof systems [Heule et$.$al'20, Buss-Thapen'19]. Redundancy has also been integrated in MaxSAT [Ihalainen et$.$al'22, Berg et$.$al'23, Bonacina et$.$al'24]. In this paper, we define a structured hierarchy of redundancy proof systems for MaxSAT, with the goal of studying its proof complexity. We obtain MaxSAT variants of proof systems such as SPR, PR, SR, and others, previously defined for SAT. All our rules are polynomially checkable, unlike [Ihalainen et$.$al'22]. Moreover, they are simpler and weaker than [Berg et$.$al'23], and possibly amenable to lower bounds. This work also complements the approach of [Bonacina et$.$al'24]. Their proof systems use different rule sets for soft and hard clauses, while here we propose a system using only hard clauses and blocking variables. This is easier to integrate with current solvers and proof checkers. We discuss the strength of the systems introduced, we show some limitations of them, and we give a short cost-SR proof that any assignment for the weak pigeonhole principle $PHP^{m}_{n}$ falsifies at least $m-n$ clauses. We conclude by discussing the integration of our rules with the MaxSAT resolution proof system, which is a commonly studied proof system for MaxSAT.
background contribution method result interpretation main claim
| # | sentence | role | the authors' own work | states the main conclusion | strength |
|---|---|---|---|---|---|
| s0 | The concept of redundancy in SAT leads to more expressive and powerful proof search techniques, e.g., able to express various inprocessing techniques, and originates interesting hierarchies of proof systems [Heule et$.$al'20, Buss-Thapen'19]. | background 1.00 | 0.04 | 0.02 | asserted 1.00 |
| s1 | Redundancy has also been integrated in MaxSAT [Ihalainen et$.$al'22, Berg et$.$al'23, Bonacina et$.$al'24]. | background 1.00 | 0.04 | 0.02 | asserted 1.00 |
| s2 | In this paper, we define a structured hierarchy of redundancy proof systems for MaxSAT, with the goal of studying its proof complexity. | contribution 1.00 | 0.91 | 0.12 | asserted 0.98 |
| s3 | We obtain MaxSAT variants of proof systems such as SPR, PR, SR, and others, previously defined for SAT. | contribution 0.93 | 0.92 | 0.11 | asserted 1.00 |
| s4 | All our rules are polynomially checkable, unlike [Ihalainen et$.$al'22]. | result 0.77 | 0.86 | 0.09 | asserted 1.00 |
| s5 | Moreover, they are simpler and weaker than [Berg et$.$al'23], and possibly amenable to lower bounds. | interpretation 0.38 | 0.59 | 0.09 | hedged possibility 0.58 |
| s6 | This work also complements the approach of [Bonacina et$.$al'24]. | background 0.46 | 0.25 | 0.04 | asserted 1.00 |
| s7 | Their proof systems use different rule sets for soft and hard clauses, while here we propose a system using only hard clauses and blocking variables. | contribution 0.65 | 0.72 | 0.05 | asserted 1.00 |
| s8 | This is easier to integrate with current solvers and proof checkers. | interpretation 0.88 | 0.45 | 0.06 | asserted 1.00 |
| s9 | We discuss the strength of the systems introduced, we show some limitations of them, and we give a short cost-SR proof that any assignment for the weak pigeonhole principle $PHP^{m}_{n}$ falsifies at least $m-n$ clauses. | contribution 0.58 | 0.95 | 0.16 | asserted 1.00 |
| s10 | We conclude by discussing the integration of our rules with the MaxSAT resolution proof system, which is a commonly studied proof system for MaxSAT. | future work 0.64 | 0.68 | 0.35 | asserted 0.75 |
What was examined, and what was not
- arXiv listing abstract v2
- full text
- figures and tables
- references and citing sentences
- relations to other papers
- P abstract
- S sections
- T body sentences
- C citations
- R cross-paper relations
The paper
Original abstract
The concept of redundancy in SAT leads to more expressive and powerful proof search techniques, e.g., able to express various inprocessing techniques, and originates interesting hierarchies of proof systems [Heule et$.$al'20, Buss-Thapen'19]. Redundancy has also been integrated in MaxSAT [Ihalainen et$.$al'22, Berg et$.$al'23, Bonacina et$.$al'24]. In this paper, we define a structured hierarchy of redundancy proof systems for MaxSAT, with the goal of studying its proof complexity. We obtain MaxSAT variants of proof systems such as SPR, PR, SR, and others, previously defined for SAT. All our rules are polynomially checkable, unlike [Ihalainen et$.$al'22]. Moreover, they are simpler and weaker than [Berg et$.$al'23], and possibly amenable to lower bounds. This work also complements the approach of [Bonacina et$.$al'24]. Their proof systems use different rule sets for soft and hard clauses, while here we propose a system using only hard clauses and blocking variables. This is easier to integrate with current solvers and proof checkers. We discuss the strength of the systems introduced, we show some limitations of them, and we give a short cost-SR proof that any assignment for the weak pigeonhole principle $PHP^{m}_{n}$ falsifies at least $m-n$ clauses. We conclude by discussing the integration of our rules with the MaxSAT resolution proof system, which is a commonly studied proof system for MaxSAT.
Human review
Discussion
Know something about this paper? Leave a comment, or highlight any passage above to comment on it.