Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Redundancy rules for MaxSAT

Ilario Bonacina, Maria Luisa Bonet, Sam Buss, Massimo Lauria

TL;DR

This work extends SAT redundancy notions to MaxSAT by introducing a hierarchy of polynomially checkable cost-preserving inferences based on blocking variables. It defines $\mathrm{cost\text{-}BC}$, $\mathrm{cost\text{-}LPR}$, $\mathrm{cost\text{-}SPR}$, $\mathrm{cost\text{-}PR}$, and $\mathrm{cost\text{-}SR}$, proving soundness for all and completeness for $\mathrm{cost\text{-}SPR}$, $\mathrm{cost\text{-}PR}$, and $\mathrm{cost\text{-}SR}$ while $\mathrm{cost\text{-}LPR}$ and $\mathrm{cost\text{-}BC}$ are incomplete. The paper demonstrates powerful, compact certificates for important formulas: polynomial-size proofs of the cost for the weak pigeonhole principle $\mathsf{bPHP}^{m}_{n}$ via $\mathrm{cost\text{-}SR}$ and short proofs for minimally unsatisfiable formulas via $\mathrm{cost\text{-}PR}$. It further connects these rules to veriPB simulations and to MaxSAT Resolution, showing there is a path toward integrating redundancy into practical MaxSAT tooling, while leaving open questions about simulations, relaxations, and lower bounds.

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.

Redundancy rules for MaxSAT

TL;DR

This work extends SAT redundancy notions to MaxSAT by introducing a hierarchy of polynomially checkable cost-preserving inferences based on blocking variables. It defines , , , , and , proving soundness for all and completeness for , , and while and are incomplete. The paper demonstrates powerful, compact certificates for important formulas: polynomial-size proofs of the cost for the weak pigeonhole principle via and short proofs for minimally unsatisfiable formulas via . It further connects these rules to veriPB simulations and to MaxSAT Resolution, showing there is a path toward integrating redundancy into practical MaxSAT tooling, while leaving open questions about simulations, relaxations, and lower bounds.

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 etal'20, Buss-Thapen'19]. Redundancy has also been integrated in MaxSAT [Ihalainen etal'22, Berg etal'23, Bonacina etal'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 etal'22]. Moreover, they are simpler and weaker than [Berg etal'23], and possibly amenable to lower bounds. This work also complements the approach of [Bonacina etal'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 falsifies at least 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.

Paper Structure

This paper contains 12 sections, 19 theorems, 36 equations.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Redundancy rules for MaxSAT
  4. Simulation by veriPB
  5. Soundness and completeness
  6. Soundness and completeness
  7. Incompleteness and Width Lower bounds
  8. Short proofs using redundancy rules
  9. Short proofs of minimally unsatisfiable formulas
  10. Short proofs of the minimum cost of $\mathsf{PHP}^{m}_{n}$
  11. MaxSAT Resolution $+$ Redundancy
  12. Conclusions and open problems

Key Result

Proposition 3.5

If $C\lor \ell$ is a $\mathrm{cost\text{-}BC}$ with respect to $\Gamma$ and the literal $\ell$, then $\mathrm{cost}(\Gamma) = \mathrm{cost}(\Gamma \cup \{C\lor \ell\})$.

Theorems & Definitions (45)

  • Definition 2.2
  • Definition 3.1: redundant clause, IBJ.22
  • Definition 3.2
  • Remark 3.3
  • Definition 3.4: $\mathrm{cost\text{-}BC}$
  • Proposition 3.5
  • proof
  • proof
  • Lemma 3.7
  • proof
  • ...and 35 more