Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



TR24-045 | 6th March 2024 10:31

Redundancy for MaxSAT


Authors: Ilario Bonacina, Maria Luisa Bonet, Sam Buss, Massimo Lauria
Publication: 6th March 2024 14:42
Downloads: 69


The concept of redundancy in SAT lead to more expressive and powerful proof search techniques, e.g. able to express various inprocessing techniques, and to interesting hierarchies of proof systems [Heule et.al’20, Buss-Thapen’19].
We propose a general way to integrate redundancy rules in MaxSAT, that is we define MaxSAT variants of proof systems such as SPR, PR, SR, and others. The main difference compared to the recent alternative approach in [Ihalainen et.al’22] is that our redundancy rules are polynomially checkable. We discuss the strength of the systems introduced and we give a short cost-SR proof that any assignment for the weak pigeonhole principle $\mathrm{PHP}^m_n$ falsifies at least $m - n$ clauses.

ISSN 1433-8092 | Imprint