Redundancy rules for MaxSAT
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866909911329275904 |
|---|---|
| author | Bonacina, Ilario Bonet, Maria Luisa Buss, Sam Lauria, Massimo |
| author_facet | Bonacina, Ilario Bonet, Maria Luisa Buss, Sam Lauria, Massimo |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2511_14657 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Redundancy rules for MaxSAT Bonacina, Ilario Bonet, Maria Luisa Buss, Sam Lauria, Massimo Logic in Computer Science 03F20, 68R07 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. |
| title | Redundancy rules for MaxSAT |
| topic | Logic in Computer Science 03F20, 68R07 |
| url | https://arxiv.org/abs/2511.14657 |