2026-07-20T05:31:25Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23741 2025-11-12T12:59:59Z ddc:004 open_access

Redundancy Rules for MaxSAT Bonacina, Ilario Bonet, Maria Luisa Buss, Sam Lauria, Massimo MaxSAT Redundancy Rules Pigeonhole Principle 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Ilario Bonacina and Maria Luisa Bonet and Sam Buss and Massimo Lauria 2025 Is Part Of LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.SAT.2025.7 urn:nbn:de:0030-drops-237411 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.7 eng https://creativecommons.org/licenses/by/4.0/legalcode