Redundancy rules for MaxSAT

TL;DR

This paper introduces a structured hierarchy of redundancy proof systems for MaxSAT, aiming to analyze proof complexity, with rules that are polynomially checkable, simpler, and more integrable with current solvers.

Contribution

It defines new MaxSAT proof systems based on redundancy hierarchies, compares their strengths, and discusses their integration with existing MaxSAT resolution proof systems.

Findings

Rules are polynomially checkable and simpler than previous systems.

The hierarchy includes MaxSAT variants of proof systems like SPR, PR, SR.

A short cost-SR proof for the weak pigeonhole principle is provided.

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.