Redundancy Rules for MaxSAT

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

doi:10.4230/LIPIcs.SAT.2025.7

Redundancy Rules for MaxSAT

Ilario Bonacina

UPC Universitat Politècnica de Catalunya, Barcelona, Spain Maria Luisa Bonet

UPC Universitat Politècnica de Catalunya, Barcelona, Spain Sam Buss

University of California, San Diego, CA, USA Massimo Lauria

Sapienza Università di Roma, Rome, Italy

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 $\mathrm{SPR}$ , $\mathrm{PR}$ , $\mathrm{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 $\mathrm{cost\text{-}SR}$ proof that any assignment for the weak pigeonhole principle $\mathsf{PHP}^{m}_{n}$ falsifies at least $m-n$ clauses.

Keywords and phrases:

MaxSAT, Redundancy Rules, Pigeonhole Principle

Funding:

Ilario Bonacina: The author was supported by grant PID2022-138506NB-C22 (PROOFS BEYOND) funded by AEI.

Maria Luisa Bonet: The author was supported by grant PID2022-138506NB-C21 (PROOFS BEYOND) funded by AEI.

Massimo Lauria: The author has been supported by the project PRIN 2022 “Logical Methods in Combinatorics” N. 2022BXH4R5 of the Italian Ministry of University and Research (MIUR).

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Proof complexity

Acknowledgements:

The authors would like to thank the Simons Institute for the Theory of Computing: part of this work has been done during the “Extended Reunion: Satisfiability” program (Spring 2023). Another part of this work has been done during the Oberwolfach workshop 2413 “Proof Complexity and Beyond” and during the 2023 Workshop on Proof Theory and its Applications organized by the Proof Society.

DOI:

10.4230/LIPIcs.SAT.2025.7

Event:

28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)

Editors:

Jeremias Berg and Jakob Nordström

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

This paper investigates new proof systems for MaxSAT that incorporate redundancy inferences tailored to work for MaxSAT. Redundancy inferences were introduced as extensions to SAT solvers to allow non-implicational inferences that preserve satisfiability and non-satisfiability. For resolution and SAT solvers, the first redundancy inferences were based on blocked clauses (BC) [25] and Resolution Asymmetric Tautology (RAT) [22, 15]. Other work on redundancy reasoning includes [14, 16, 20, 23, 17]; and, of particular relevance to the present paper, are the work of Heule, Kiesl, and Biere [19], and the work of Buss and Thapen [9]. Redundancy inferences formalize “without loss of generality” reasoning [30] and can substantially strengthen resolution and, in some cases, the effectiveness of SAT solvers for hard problems such as the pigeonhole principle (PHP) [20]. Indeed, in their full generality, redundancy inferences allow resolution to polynomially simulate extended resolution.

MaxSAT is a generalization of SAT; it is the problem of determining a truth assignment for a CNF formula that minimizes the number of falsified clauses. Although the MaxSAT problem is inherently more difficult than SAT, in some cases MaxSAT can be adapted to be more efficient in practice than CDCL solvers for hard problems such as PHP [7]. There are several approaches to MaxSAT solvers, including MaxSAT resolution [8, 26], core-guided MaxSAT [12, 1, 28, 27, 29], and maximum-hitting-set MaxSAT [2, 11, 31] ; the present paper discusses only MaxSAT resolution. The MaxSAT resolution proof system was first defined by Larrosa and Heras [26] and proved completed by Bonet, Levy and Manya [8].

We define cost preserving redundancy rules for MaxSAT mirroring the redundancy rules for SAT, called “ $\mathrm{cost\text{-}BC}$ ”, “ $\mathrm{cost\text{-}LPR}$ ”, “ $\mathrm{cost\text{-}SPR}$ ”, “ $\mathrm{cost\text{-}PR}$ ”, and “ $\mathrm{cost\text{-}SR}$ ” (see Definition 3.2). The strongest of these is “ $\mathrm{cost\text{-}SR}$ ” based on the substitution redundancy ( $\mathrm{SR}$ ) [9]. All five of these new inferences are sound for MaxSAT reasoning (Theorem 4.2). Furthermore, we prove that $\mathrm{cost\text{-}SPR}$ , $\mathrm{cost\text{-}PR}$ and $\mathrm{cost\text{-}SR}$ are complete for MaxSAT (Theorem 4.3). On the other hand, we prove that $\mathrm{cost\text{-}LPR}$ and $\mathrm{cost\text{-}BC}$ are incomplete for MaxSAT (Corollary 5.2). We illustrate the power of $\mathrm{cost\text{-}SR}$ by giving polynomial size proofs of the cost of the blocking-variable version of weak pigeonhole principle $\mathsf{bPHP}^{m}_{n}$ for arbitrary numbers $m>n$ of pigeons and holes (Theorem 6.3).

Ours is not the first paper bringing redundancy reasoning to the context of optimization. For instance, the work of Ihalainen, Berg and Järvisalo [21], building on [4], introduced versions of redundancy inferences that work with MaxSAT. In contrast to the system CPR of [21], all of our “cost-” inferences are polynomial-checkable for validity, and thus all give traditional Cook-Reckhow proof systems for MaxSAT.

Another system with redundancy rules for certifying unsatisfiability and optimization is veriPB [5]. Being rooted in cutting planes, veriPB is particularly apt at certifying optimality, and it can log the reasoning of MaxSAT solver strategies that are way out of reach of MaxSAT resolution [3]. The propositional fragment of $\mathrm{veriPB}$ is as strong as Extended Resolution and DRAT, and plausibly even stronger [24]. In contrast, our systems are plausibly weaker and simpler, but yet strong enough to prove efficiently interesting formulas. Still our systems might be amenable to proving lower bounds. Indeed, our explicit goal is to study the proof complexity of redundancy rules for MaxSAT in a similar vein of what [9] does for SAT, something that is beyond the scope of $\mathrm{veriPB}$ , focused on proof logging actual solvers. As a starting point, we show that “cost-BC” and “cost-LPR” are not complete (Corollary 5.2) and we show width lower bounds on “cost-SPR” and an analogue of a width lower bound for “cost-SR” (Corollary 5.3). Finally there is another work that tries to modify the redundancy rules to make them compatible with the MaxSAT model of soft and hard clauses [6]. That work has a similar spirit to this one, but departs in the redundancy test, which checks for inclusion rather than for reverse unit propagation. Such choice makes the inference weaker but preserves the number of unsatisfied clauses, hence the rule applies directly to soft clauses.

Before proceeding with the description and analysis of our systems, we should highlight two aspects of redundancy inference that are somehow orthogonal to the choice of the concrete inference rule: clause deletion and new variable introduction. The applicability of a redundancy rule depends on the clauses present in the database, and it seems that allowing deletion of past clauses makes the system stronger, and indeed collapses together the power of several types of inference rules (see [9]). Likewise the possibility of introducing new variables in redundant clauses makes all such systems as powerful as extended resolution [25]. Coherently with the stated goal of having systems that are simple and amenable to proof complexity analysis, in this paper we do not allow neither clause deletion nor new variables.

Structure of the paper

Section 2 contains all the necessary preliminaries, including notation on MaxSAT and the blocking variables encoding of MaxSAT instances (blocking variables are also used by [21]). Section 3 introduces the redundancy rules for MaxSAT, proves their basic properties, and defines calculi based on those rules. Section 4 shows their soundness, and their completeness. Section 5 shows the incompleteness of $\mathrm{cost\text{-}BC}$ / $\mathrm{cost\text{-}LPR}$ and some limitations of $\mathrm{cost\text{-}SPR}$ and even $\mathrm{cost\text{-}SR}$ . Section 6 gives examples of applications of the redundancy rules, including a polynomial size proof of the optimal cost of the weak Pigeonhole Principle and a general result about the polynomial size provability of minimally unsatisfiable formulas. Section 7 gives some concluding remarks.

2 Preliminaries

For a natural number $n$ , let $[n]$ be the set $\{1,\dots,n\}$ . Sets and multi-sets are denoted with capital Roman or Greek letters.

Propositional logic notation

A Boolean variable $x$ takes values in $\{0,1\}$ . A literal is either a variable $x$ or its negation $\overline{x}$ . A clause is a finite disjunction of literals, i.e., $C=\bigvee_{i}\ell_{i}$ . The empty clause is $\bot$ . A formula in Conjunctive Normal Form (CNF) is a conjunction of clauses $\Gamma=\bigwedge_{j}C_{j}$ . We identify a CNF with the multiset of its clauses, and denote as $|\Gamma|$ the number of its clauses (counted with multiplicity). We denote as ${\mathrm{Var}}(\Gamma)$ the set of variables in $\Gamma$ .

Substitutions and assignments

A substitution $\sigma$ for a set of variables $X$ is a function so that $\sigma(x)$ is either $0$ , $1$ or some literal defined on $X$ . For convenience, we extend a substitution $\sigma$ to constants and literals, setting $\sigma(0)=0$ , $\sigma(1)=1$ , and $\sigma(\overline{x})=\overline{\sigma(x)}$ for any variable $x\in X$ . The composition of two substitutions $\sigma,\tau$ is the substitution $\sigma\circ\tau$ , where $\sigma\circ\tau(x)=\sigma(\tau(x))$ for $x\in X$ . A substitution $\sigma$ is an assignment when $\sigma(x)\in\{0,1,x\}$ for any $x\in X$ . The domain of an assignment $\sigma$ is $\operatorname{dom}(\sigma)=\sigma^{-1}(\{0,1\})$ , and $\sigma$ is a total assignment over $X$ if $X$ is its domain, i.e., $\sigma$ maps all variables in $X$ to Boolean values. Given a clause $C=\bigvee_{i}\ell_{i}$ and a substitution $\sigma$ , the clause $C$ restricted by $\sigma$ , is $C\!\upharpoonright_{\sigma}=\bigvee_{i}\sigma(\ell_{i})\ ,$ simplified using the usual logic rules, i.e., $D\lor 0=D$ , $D\lor 1=1$ , and $D\lor\ell\lor\ell=D\lor\ell$ . Another notation for $C\!\upharpoonright_{\sigma}$ is $\sigma(C)$ . If $\sigma(C)=1$ or $\sigma(C)$ is tautological we say that $\sigma\vDash C$ , i.e., $\sigma$ satisfies $C$ .

The restriction of a CNF formula $\Gamma$ by $\sigma$ , denoted as $\Gamma\!\upharpoonright_{\sigma}$ , is the conjunction of all clauses $C\!\upharpoonright_{\sigma}$ where $C\in\Gamma$ and $\sigma(C)\neq 1$ . The CNF $\Gamma\!\upharpoonright_{\sigma}$ is also a multiset. We say that $\sigma$ satisfies $\Gamma$ ( $\sigma\vDash\Gamma$ ) if for every $C\in\Gamma$ , $\sigma\vDash C$ , i.e., $\Gamma\!\upharpoonright_{\sigma}=\emptyset$ . We say that $\Gamma\vDash C$ if for every substitution $\sigma$ , if $\sigma\vDash\Gamma$ then $\sigma\vDash C$ .

We identify a literal $\ell$ with the substitution that assigns $\ell$ to $1$ and leaves all other variables unassigned. Hence we use notations like $\Gamma\!\upharpoonright_{\ell}$ . Likewise, given a clauses $C$ we denote as $\overline{C}$ the assignment that maps all literals in $C$ to false, and we use the notation $\Gamma\!\upharpoonright_{\overline{C}}$ .

Unit propagation

A unit clause is a clause of just one literal. Unit propagation works as follows. Start with a CNF $\Gamma$ : if $\Gamma$ has no unit clauses, the process ends, otherwise pick some unit clause $\ell$ in $\Gamma$ arbitrarily, remove from $\Gamma$ all clauses containing $\ell$ and remove literal $\bar{\ell}$ from all clauses containing it. Keep repeating until $\Gamma$ has no more unit clauses. Regardless of the choice of the unit clause, the process always ends with the same formula.

We say that $\Gamma\vdash_{1}C$ when the application of unit propagation to the formula $\Gamma\!\upharpoonright_{\overline{C}}$ produces the empty clause. For two CNF formulas $\Gamma,\Delta$ we say that $\Gamma\vdash_{1}\Delta$ if for every $D\in\Delta$ , $\Gamma\vdash_{1}D$ . Clearly, if $\Gamma\supseteq\Delta$ then $\Gamma\vdash_{1}\Delta$ , and if $\Gamma\vdash_{1}\Delta$ , then $\Gamma\vDash\Delta$ . It is important to stress that the $\vdash_{1}$ relation is efficiently checkable.

Observation 2.1 ([9, Fact 1.3]).

Let $\sigma$ be a substitution and $\Gamma,\Delta$ be CNF formulas, if $\Gamma\vdash_{1}\Delta$ , then $\Gamma\!\upharpoonright_{\sigma}\vdash_{1}\Delta\!\upharpoonright_{\sigma}$ .

Resolution

Resolution is a well-studied propositional deduction system with two inference rules: (i) from a clause $A$ we can deduce any $B$ s.t. $A\subseteq B$ ; (ii) from clauses $A\lor x$ and $B\lor\overline{x}$ we can deduce $A\lor B$ . A resolution proof from a set of clauses $\Gamma$ is a sequence of clauses $D_{1},D_{2},\ldots,D_{t}$ where each $D_{i}$ is either already in $\Gamma$ or is deduced from earlier clauses in the sequence using one of the two inference rules. Resolution is complete, thus deciding whether a clause $C$ can be deduced from $\Gamma$ is the same as deciding whether $\Gamma\vDash C$ .

MaxSAT

Given a CNF formula $F$ , MaxSAT asks to find the maximum number of clauses in $F$ which can be simultaneously satisfied. In applications, it is useful to consider a generalization for which we divide the clauses into hard or soft (partial MaxSAT). Hard clauses must be satisfied, while soft clauses can be falsified with a cost. Consider $F=H\land S$ where $H$ is the multiset of hard clauses and $S$ is the multiset of soft ones. In this model, MaxSAT asks to find the maximum number of clauses in $S$ that can be simultaneously satisfied by an assignment that satisfies all clauses in $H$ . Observe that the optimization problem is not well defined if $H$ is not satisfiable.¹¹1An even more general version is weighted MaxSAT, where we would consider weighted set of clauses $(F,w)$ , i.e., each clauses $C\in F$ has an associated weight $w(C)$ where $w:F\to\mathbb{N}\cup\{\infty\}$ . In this model the goal is to minimize the weight of the falsified clauses. The role of the weight $\infty$ is to model hard clauses. In this paper we do not focus on this model. It is not relevant whether $H$ is a set or a multiset. In $S$ , on the other hand, the multiplicity of soft clauses must be accounted for.

Proof systems for MaxSAT aim to show lower bounds on the cost of (partial) MaxSAT instances, one such system is MaxSAT resolution.

MaxSAT with blocking variables

Without loss of generality we can assume that all soft clauses in a MaxSAT instance are unit clauses; indeed, using a new variable $b$ , a soft clause $C$ can be replaced with a hard clause $C\lor b$ and a soft clause $\overline{b}$ , without affecting the cost. The variable $b$ is usually called a blocking variable. This appears in [13], but it might have been used even earlier.

Definition 2.2.

Let $F=H\land S$ with soft clauses $S=C_{1}\land\dots\land C_{m}$ . The blocking variables formulation of $F$ is $F^{\prime}=H^{\prime}\land S^{\prime}$ where

$\blacksquare$

$H^{\prime}=H\land(C_{1}\lor b_{1})\land\dots\land(C_{m}\lor b_{m})$ ,
$\blacksquare$

$S^{\prime}=\overline{b_{1}}\land\dots\land\overline{b_{m}}$ ,

and $b_{1},\dots,b_{m}$ are new variables (blocking variables) not appearing in $F$ . We say that $\Gamma$ is a MaxSAT instance encoded with blocking variables, when it is given as a set of hard clauses of the form as in $H^{\prime}$ above. The soft clauses, then, are implicit.

Observation 2.3.

Let $F=H\land S$ be a MaxSAT instance and $F^{\prime}=H^{\prime}\land S^{\prime}$ be the blocking variables formulation of $F$ . Any assignment that satisfies $H$ and falsifies $k$ clauses in $S$ can be extended to an assignment that satisfies $H^{\prime}$ and sets $k$ blocking variables to true. Vice versa, any assignment that satisfies $H^{\prime}$ and sets $k$ blocking variables to true satisfies $H$ too and falsifies at most $k$ clauses in $S$ .

Because of ˜2.3, for the rest of this work we consider $\Gamma$ to be a MaxSAT instance encoded with blocking variables usually named $\{b_{1},\dots,b_{m}\}$ . The goal is to satisfy $\Gamma$ while setting to true the least number of blocking variables. More formally, given a total assignment $\alpha$ for $\Gamma$ , we define

\mathrm{cost}(\alpha)=\sum^{m}_{i=1}\alpha(b_{i})\quad\hbox{and}\quad\mathrm{% cost}(\Gamma)=\min_{\alpha\,:\,\alpha\,\vDash\,\Gamma}\mathrm{cost}(\alpha)

and the goal is to find the value of $\mathrm{cost}(\Gamma)$ . Notice that, the notation $\mathrm{cost}(\alpha)$ is defined even for assignments not satisfying $\Gamma$ .

3 Redundancy rules for MaxSAT

In the context of SAT, a clause $C$ is redundant w.r.t. a CNF instance $\Gamma$ if $\Gamma$ and $\Gamma\cup\{C\}$ are equisatisfiable, that is either they both are satisfiable or both unsatisfiable [25]. The natural adaptation of this notion to MaxSAT is a clause $C$ that does not affect the cost of $\Gamma$ .

Definition 3.1 (redundant clause, [21]).

A clause $C$ is redundant w.r.t. a MaxSAT instance $\Gamma$ when

\mathrm{cost}(\Gamma)=\mathrm{cost}(\Gamma\cup\{C\})\;.

(1)

Clauses that logically follow from $\Gamma$ are obviously redundant, but there may be other useful clauses that do not follow logically, and yet do not increase the cost if added.

The condition in eq. (1) is not polynomially checkable (unless, say $\hbox{P}=\hbox{NP}$ ). Therefore, we consider efficiently certifiable notions of redundancy, i.e., ways to add redundant clauses (in the sense of eq. (1)) while certifying efficiently their redundancy. This is done showing how to extend in a systematic way the notions of efficiently certifiable redundancy already studied in the context of SAT (BC, RAT, LPR, SPR, PR, SR) [19, 9] to the context of MaxSAT. This is an alternative to the approach of [21]. This definition could also be seen as a very special case of veriPB [5] (see Section 3.1 for more details on the connections with veriPB).

Definition 3.2.

A clause $C$ is cost substitution redundant ( $\mathrm{cost\text{-}SR}$ ) w.r.t. to $\Gamma$ if there exists a substitution $\sigma$ such that

1.

$\Gamma\!\upharpoonright_{\overline{C}}\ \vdash_{1}(\Gamma\cup\{C\})|_{\sigma}$ (redundancy)
2.

for all total assignments $\tau\supseteq\overline{C}$ , $\mathrm{cost}(\tau\circ\sigma)\leq\mathrm{cost}(\tau)$ (cost).

If the substitution $\sigma$ has some additional structure, we have the following redundancy rules listed in decreasing order of generality:

Cost propagation redundant ( $\mathrm{cost\text{-}PR}$ ): if $\sigma$ is a partial assigment.
Cost subset propagation redundant ( $\mathrm{cost\text{-}SPR}$ ): if $\sigma$ is a partial assigment with the same domain as $\overline{C}$ . In other words, $\sigma$ flips some variables in $\overline{C}$ .
Cost literal propagation redundant ( $\mathrm{cost\text{-}LPR}$ ): if $\sigma$ is a partial assignment with the same domain as $\overline{C}$ , but differs from $\overline{C}$ on exactly one variable.
Cost blocked clause ( $\mathrm{cost\text{-}BC}$ ): if $\sigma$ is a partial assignment with the same domain as $\overline{C}$ , which differs from $\overline{C}$ on exactly one variable $v$ , and moreover, for every clause $D\in\Gamma$ containing the variable $v$ , $\sigma\vDash D$ .²²2The definition of blocked clause is written to match the previous definitions. In this case, the redundancy condition is always satisfied.

Item 1 in Definition 3.2 claims that adding $C$ does not make $\Gamma$ unsatisfiable, unless it was already the case. Together with Item 2, it ensures that any assignment that falsifies the new clause $C$ can be patched with a substitution $\sigma$ so that $C$ is satisfied without increasing the minimum cost (see Lemma 3.4).

Indeed, Item 1 in Definition 3.2 and its variants correspond to the redundancy rules of proof systems $\mathrm{SR}$ , $\mathrm{PR}$ , $\mathrm{SPR}$ , and $\mathrm{LPR}$ from [9], adapted here to consider cost. Since $\mathrm{LPR}$ is the same as $\mathrm{RAT}$ (see [9, Theorem 1.10]), the notion of cost literal propagation redundancy could as well be called cost- $\mathrm{RAT}$ redundancy.

$\blacktriangleright$ Remark 3.3.

It is important to compare Definition 3.2 with [21, Definition 2]. Redundancy conditions are very similar and the main differences are in the cost conditions. Let us compare their CPR rule with our $\mathrm{cost\text{-}PR}$ . In $\mathrm{cost\text{-}PR}$ , the cost condition requires the witness $\sigma$ to be at least as good as all possible extensions of $\overline{C}$ , while in CPR the requirement is enforced only on those extensions of $\overline{C}$ that satisfy $\Gamma$ . The latter more permissive condition allows to derive more clauses, but it is unlikely to be polynomially checkable, while the condition in $\mathrm{cost\text{-}PR}$ is polynomially checkable (see Lemma 3.5). In [21], the authors also define two polynomially checkable rules where the cost condition is not present, but implicitly enforced via restrictions on the type of assignments used. Those rules are special cases of $\mathrm{cost\text{-}LPR}$ and $\mathrm{cost\text{-}SPR}$ respectively.

Lemma 3.4.

If $C$ is $\mathrm{cost\text{-}SR}$ w.r.t. to $\Gamma$ , then $C$ is redundant w.r.t. $\Gamma$ .

Proof.

It is enough to show that $\mathrm{cost}(\Gamma)\geq\mathrm{cost}(\Gamma\cup\{C\})$ . Let $\mathrm{cost}(\Gamma)=k$ . To show that adding $C$ to $\Gamma$ does not increase the cost, consider an optimal total assignment $\alpha$ that satisfies $\Gamma$ and sets to true exactly $k$ blocking variables. If $\alpha\vDash C$ we already have that $\alpha\vDash\Gamma\cup\{C\}$ and $\mathrm{cost}(\alpha)=k$ . Otherwise, $\alpha$ extends $\overline{C}$ and, by assumption, there is a substitution $\sigma$ such that $\mathrm{cost}(\alpha\circ\sigma)\leq k$ . To show that $\mathrm{cost}(\Gamma\cup\{C\})\leq k$ , it remains to show that indeed $\alpha\circ\sigma\vDash\Gamma\cup\{C\}$ . By assumption,

\Gamma\!\upharpoonright_{\overline{C}}\ \vdash_{1}(\Gamma\cup\{C\})|_{\sigma}\;,

and, since $\alpha\vDash\Gamma$ and extends $\overline{C}$ , then $\alpha\vDash(\Gamma\cup\{C\})|_{\sigma}$ too. Equivalently, $\alpha\circ\sigma\vDash\Gamma\cup\{C\}$ . $\hfill\blacktriangleleft$

Both Item 1 and Item 2 of Definition 3.2 are stronger than what is actually needed for Lemma 3.4 to hold. Indeed, for Item 1, it would be enough that $\Gamma\!\upharpoonright_{\overline{C}}\ \vDash(\Gamma\cup\{C\})|_{\sigma}$ , and, for Item 2, it would be sufficient to check it for any $\tau\supseteq\overline{C}$ such that $\tau\vDash\Gamma$ . Unfortunately, these latter versions of Item 1 and Item 2 are in general not polynomially checkable. Instead, our conditions are checkable in polynomial time.

Lemma 3.5.

Let $\Gamma$ be a MaxSAT instance, $C$ a clause and $\sigma$ a substitution. There is a polynomial time algorithm to decide whether $C$ is $\mathrm{cost\text{-}SR}$ w.r.t. $\Gamma$ , given the substitution $\sigma$ .

Proof (sketch).

The redundancy condition in Definition 3.2 is polynomially checkable, since it is a unit propagation. To check the cost condition we need to check whether

\max_{\tau\supseteq\overline{C}}(\mathrm{cost}(\tau\circ\sigma)-\mathrm{cost}(% \tau))

(2)

is at most $0$ . This amounts to maximizing the function

\Big{(}\sum_{i=1}^{n}\sigma(b_{i})-b_{i}\Big{)}\Big{\rvert}_{\overline{C}}

(3)

over all assignments on variables in ${\mathrm{Var}}{(\Gamma)}\setminus{\mathrm{Var}}{(\overline{C})}$ . Observe that eq. (3) is a function of the form $c\leavevmode\nobreak\ +\leavevmode\nobreak\ \sum_{v\in{\mathrm{Var}}{(\Gamma)}% \setminus{\mathrm{Var}}{(\overline{C})}}c_{v}\cdot v$ , for suitable constants $c$ and $c_{v}$ s. Therefore its maximum can be easily determined in polynomial time and corresponds to assigning each $v$ to $1$ when $c_{v}>0$ and to $0$ otherwise. $\hfill\blacktriangleleft$

Lemma 3.5 allows the definition of proof systems that extend resolution using cost redundancy rules in the sense of Cook-Reckhow [10].

Definition 3.6 ( $\mathrm{cost\text{-}SR}$ calculus).

The $\mathrm{cost\text{-}SR}$ calculus is a proof system for MaxSAT. A derivation of a clause $C$ from a MaxSAT instance $\Gamma$ (encoded with blocking variables) is a sequence of clauses $D_{1},D_{2},\ldots,D_{t}$ where, $C\in\Gamma\cup\{D_{i}\}_{i\in[t]}$ , each $D_{i}$ is either already in $\Gamma$ or is deduced from earlier clauses in the sequence using a resolution rule, or $D_{i}$ is $\mathrm{cost\text{-}SR}$ w.r.t. to $\Gamma\cup\{D_{1},\ldots,D_{i-1}\}$ with ${\mathrm{Var}}(D_{i})\subseteq{\mathrm{Var}}(\Gamma)$ .³³3We only consider the case where no new variables are added via $\mathrm{cost\text{-}SR}$ rules. To be coherent with [9], $\mathrm{cost\text{-}SR}$ should be $\mathrm{cost\text{-}SR}^{-}$ , following the notational convention of adding an exponent with “ $-$ ” to denote $\mathrm{SR}$ , $\mathrm{PR}$ and $\mathrm{SPR}$ when the systems are not allowed to introduce new variables. We ignore that convention to ease an already rich notation. The length of such derivation is $t$ , i.e., the number of derived clauses. To check the validity of derivations in polynomial time, any application of the $\mathrm{cost\text{-}SR}$ rule comes accompanied by the corresponding substitution that witnesses its soundness.

If the goal is to certify that $\mathrm{cost}(\Gamma)\geq s$ , we can accomplish this deriving $s$ distinct unit clauses of the form $\{b_{i_{1}},\dots,b_{i_{s}}\}$ (see Theorem 4.2). If the goal is to certify that $\mathrm{cost}(\Gamma)=s$ , we can accomplish this deriving $s$ distinct unit clauses of the form $\{b_{i_{1}},\dots,b_{i_{s}}\}$ together with the unit clauses $\{\overline{b}_{j}:j\notin\{i_{1},\dots,i_{s}\}\}$ (see Theorem 4.2).

In a similar fashion we define $\mathrm{cost\text{-}PR}$ , $\mathrm{cost\text{-}SPR}$ , $\mathrm{cost\text{-}LPR}$ , and $\mathrm{cost\text{-}BC}$ calculi. A remarkable aspect of these calculi is that a proof must somehow identify the blocking variables to be set to true. When there are multiple optimal solutions, it is quite possible that none of the $b_{i}$ follows logically from $\Gamma$ . Nevertheless, the redundancy rules, often used to model “without loss of generality” reasoning, can reduce the solution space.

3.1 Simulation by veriPB

We show that $\mathrm{cost\text{-}SR}$ and its subsystems are p-simulated by $\mathrm{veriPB}$ . This is actually not surprising since $\mathrm{veriPB}$ proof steps are based on cutting planes, which in turn easily simulates resolution. Furthermore $\mathrm{veriPB}$ includes the SAT redundancy rules equipped with some criteria of cost preservation. $\mathrm{veriPB}$ can argue within the proof whether some substitution is cost preserving. If $\mathrm{veriPB}$ can do that for the substitutions that respect the second condition in Definition 3.2, then it p-simulates $\mathrm{cost\text{-}SR}$ .

Since $\mathrm{veriPB}$ is a complex system, we describe the minimal fragment needed to simulate $\mathrm{cost\text{-}SR}$ . Consider a CNF formula $F$ and some objective linear function $f$ to be minimized. A $\mathrm{veriPB}$ derivation starts with $F$ encoded as linear inequalities. At each step a linear inequality $C$ is derived from the set $\Gamma$ of previously derived inequalities in one of the following ways:

1.

$C$ is derived from $\Gamma$ using some cutting planes rule;
2.

there exists a substitution $\sigma$ so that $\Gamma\cup{\overline{C}}\ \vdash(\Gamma\cup\{C\})\!\upharpoonright_{\sigma}% \cup\{f\!\upharpoonright_{\sigma}\leq f\}$ ,where the symbol $\vdash$ means that there is a cutting planes proof that witnesses the implication.

In Item 2 the cutting plane proof is included in the $\mathrm{veriPB}$ proof to make it polynomially verifiable, unless it just consists in unit propagation steps or certain uses of Boolean axioms. In the latter cases the verifier can efficiently recover such derivation steps on its own.

The resolution inference rule of $\mathrm{cost\text{-}SR}$ can be simulated using 1. The redundacy inference rule of $\mathrm{cost\text{-}SR}$ is simulated by 2. The redundancy condition is syntactically the same, while the cost condition is argued via a cutting planes proof. The latter is the only non-trivial part. This argument gives a proof sketch of the following proposition.

Proposition 3.7.

Let $F$ be a MaxSAT instance over $n$ variables with blocking variables $b_{1},b_{2},\ldots,b_{k}$ . If there is a $t$ step $\mathrm{cost\text{-}SR}$ derivation of a set of clauses $\Gamma$ from it, then there is a $\mathrm{veriPB}$ proof from $F$ and objective $f=\sum^{k}_{i=1}b_{i}$ of some $\Gamma^{\prime}\supseteq\Gamma$ in $\mathrm{poly}(nt)$ steps.

4 Soundness and completeness

The calculi $\mathrm{cost\text{-}SR}$ / $\mathrm{cost\text{-}PR}$ / $\mathrm{cost\text{-}SPR}$ are sound and complete. Before proving the soundness we show an auxiliary lemma, that shows that when the calculus certifies the lower bound for the optimal values, it can also certify the optimality.

Lemma 4.1.

Let $\Gamma$ be a MaxSAT instance encoded with blocking variables $b_{1},\dots,b_{m}$ , of $\mathrm{cost}(\Gamma)=k$ , and suppose $\Gamma$ contains the unit clauses $b_{i_{1}},\dots,b_{i_{k}}$ . Then $\mathrm{cost\text{-}PR}$ can prove $\overline{b}_{j}$ for each $j\notin\{i_{1},\dots,i_{k}\}$ in $\mathcal{O}(km)$ steps.

Proof.

Let $\sigma$ be a total assignment satisfying $\Gamma$ with $\mathrm{cost}(\sigma)=k$ , that is $\sigma$ maps all the $b_{i_{\ell}}$ s to $1$ and the other blocking variables to $0$ . We derive all the clauses

C_{j}=\overline{b}_{i_{1}}\lor\dots\lor\overline{b}_{i_{k}}\lor\overline{b}_{j}

with $j\notin\{i_{1},\dots,i_{k}\}$ using the $\mathrm{cost\text{-}PR}$ rule. For all clauses $C_{j}$ , the substitution witnessing the validity of the $\mathrm{cost\text{-}PR}$ rule is always $\sigma$ . The redundancy condition from Definition 3.2 is trivially true since $\Gamma$ union an arbitrary set of $C_{j}$ s is mapped to $1$ under $\sigma$ . The cost condition is true because for every $\tau\supseteq\overline{C_{j}}$ , $\mathrm{cost}(\tau)\geq k+1$ and $\mathrm{cost}(\tau\circ\sigma)=\mathrm{cost}(\sigma)=k$ .

To conclude, by resolution, derive $\overline{b}_{j}$ from $C_{j}$ and the unit clauses $b_{i_{1}},\dots,b_{i_{k}}$ . $\hfill\blacktriangleleft$

Theorem 4.2 (soundness of $\mathrm{cost\text{-}SR}$ ).

Let $\Gamma$ be a MaxSAT instance encoded with blocking variables. If there is a $\mathrm{cost\text{-}SR}$ proof of $k$ distinct blocking variables, then $\mathrm{cost}(\Gamma)\geq k$ . If there is a $\mathrm{cost\text{-}SR}$ proof of $k$ distinct blocking variables $\{b_{i_{1}},\dots,b_{i_{k}}\}$ and all the unit clauses $\overline{b}_{j}$ for $j\notin\{i_{1},\dots,i_{k}\}$ , then $\mathrm{cost}(\Gamma)=k$ .

Proof.

Let $b_{1},\ldots,b_{m}$ be the blocking variables of $\Gamma$ . Let $\Gamma^{\prime}$ the set of clauses in $\Gamma$ plus all the clauses derived in the proof of $\mathrm{cost}(\Gamma)\geq k$ . That is $\Gamma^{\prime}$ also contains contains $k$ distinct unit clauses $b_{i_{1}},\dots,b_{i_{k}}$ , hence $\mathrm{cost}(\Gamma^{\prime})\geq k$ . By Lemma 3.4, the cost is preserved along proof steps, therefore $\mathrm{cost}(\Gamma)=\mathrm{cost}(\Gamma^{\prime})\geq k$ . In the case where we have all the $\overline{b}_{j}$ s then $\mathrm{cost}(\Gamma^{\prime})=k$ and therefore $\mathrm{cost}(\Gamma)=k$ . $\hfill\blacktriangleleft$

As an immediate consequence of Theorem 4.2, also all the $\mathrm{cost\text{-}PR}$ , $\mathrm{cost\text{-}SPR}$ , $\mathrm{cost\text{-}LPR}$ calculi are sound. Moreover, we can always prove the optimal lower bound in $\mathrm{cost\text{-}SPR}$ calculus.

Theorem 4.3 (completeness of $\mathrm{cost\text{-}SPR}$ ).

Let $\Gamma$ be a MaxSAT instance encoded with blocking variables, of $\mathrm{cost}(\Gamma)=k$ . There is a $\mathrm{cost\text{-}SPR}$ derivation of the unit clauses $b_{i_{1}},\dots,b_{i_{k}}$ for some distinct $k$ blocking literals and all the $\overline{b}_{j}$ for $j\notin\{i_{1},\dots,i_{k}\}$ .

Proof.

Let $b_{1},\ldots,b_{m}$ be the blocking variables of $\Gamma$ . Take $\alpha_{\mathrm{opt}}$ to be an optimal assignment, that is $\alpha_{\mathrm{opt}}\vDash\Gamma$ , $\mathrm{cost}(\alpha_{\mathrm{opt}})=k$ , and for every total assignment $\beta$ that satisfies $\Gamma$ , $\mathrm{cost}(\beta)\geq k$ . Without loss of generality we can assume $\alpha_{\mathrm{opt}}$ sets variables $b_{1},\dots,b_{k}$ to $1$ and the remaining $b_{j}$ s to $0$ .

Given any assignment $\gamma$ , let $\bar{\gamma}$ be the largest clause falsified by $\gamma$ . Let $\Sigma$ be the set of all clauses $\bar{\gamma}$ where $\gamma$ is a total assignment that satisfies $\Gamma$ is different from $\alpha_{\mathrm{opt}}$ . We want to derive $\Sigma$ from $\Gamma$ , essentially forbidding any satisfying assignment except for $\alpha_{\mathrm{opt}}$ .

We can add all clauses in $\Sigma$ one by one by the $\mathrm{cost\text{-}SPR}$ rule. Indeed, for any clause $\bar{\gamma}\in\Sigma$ and any $\Sigma^{\prime}\subseteq\Sigma$ , the clause $\bar{\gamma}$ is $\mathrm{cost\text{-}SPR}$ w.r.t. $\Gamma\cup\Sigma^{\prime}$ , with $\alpha_{\mathrm{opt}}$ as the witnessing assignment. The redundancy condition

(\Gamma\cup\Sigma^{\prime})\!\upharpoonright_{\gamma}\vdash_{1}(\Gamma\cup% \Sigma^{\prime}\cup\bar{\gamma})\!\upharpoonright_{\alpha_{\mathrm{opt}}}

holds because $\alpha_{\mathrm{opt}}\vDash\Gamma\cup\Sigma^{\prime}\cup\bar{\gamma}$ so the RHS is just true. The cost condition holds by optimality of $\alpha_{\mathrm{opt}}$ . In the end, the only assignment that satisfies $\Gamma\cup\Sigma$ is $\alpha_{\mathrm{opt}}$ . By the completeness resolution we can prove all its literals, in particular literals $b_{i}$ for $1\leq i\leq k$ and literals $\overline{b}_{i}$ for $i>k$ . $\hfill\blacktriangleleft$

5 Incompleteness and Width Lower bounds

Theorem 4.3 shows the completeness of $\mathrm{cost\text{-}SPR}$ , hence for $\mathrm{cost\text{-}PR}$ and $\mathrm{cost\text{-}SR}$ . It is not a coincidence that the proof does not apply to $\mathrm{cost\text{-}LPR}$ , indeed the latter is not complete. We will see that for some redundant clause derived according to Definition 3.2, the number of values that partial assignment $\sigma$ flips with respect to any $\tau\supseteq\overline{C}$ may have to be large. In a $\mathrm{cost\text{-}LPR}$ proof this number is always at most one. For a redundant clause $C$ derived in some subsystem of $\mathrm{cost\text{-}SR}$ via a witness substitution $\sigma$ we define

\operatorname{flip}(C,\sigma)=\max_{\tau\supseteq\overline{C}}\;\operatorname{% HammingDistance}(\tau,\tau\circ\sigma)\;,

where $\operatorname{HammingDistance}$ is the number of different bits between two total assignments. The following result shows sufficient conditions for $\operatorname{flip}(C,\sigma)$ to be large.

Theorem 5.1.

Let $\Gamma$ be a MaxSAT instance encoded with blocking variables, of $\mathrm{cost}(\Gamma)=k$ , and let $A$ be the set of optimal total assignments for $\Gamma$ , i.e., $\alpha\in A$ when $\alpha\vDash\Gamma$ and $\mathrm{cost}(\alpha)=k$ . If $A$ is such that

1.

all pairs of assignments in $A$ have Hamming distance at least $d$ , and
2.

for every blocking variable $b$ there are $\alpha,\beta\in A$ s.t. $\alpha(b)=0$ and $\beta(b)=1$ ,

then to derive any blocking literal $b$ , $\mathrm{cost\text{-}SR}$ must derive a redundant clause with $\operatorname{flip}(C,\sigma)\geq d$ , where $\sigma$ is the witnessing substitution for $C$ .

Proof.

Consider a $\mathrm{cost\text{-}SR}$ derivation from $\Gamma$ as a sequence $\Gamma_{0},\Gamma_{1},\dots,\Gamma_{s}$ where each $\Gamma_{i+1}:=\Gamma_{i}\cup\{C\}$ with $C$ either derived by resolution from clauses in $\Gamma_{i}$ , or $C$ is $\mathrm{cost\text{-}SR}$ w.r.t. $\Gamma_{i}$ . For $0\leq j\leq s$ , let $\mu(j)$ be the number of the optimal assignments for $\Gamma_{j}$ .

At the beginning $\mu(0)=|A|$ by construction. If at some point $\Gamma_{j}$ contains some clause $b_{i}$ , then the value $\mu(j)$ must be strictly smaller than $|A|$ because $A$ contains at least some assignment with $\{b_{i}\mapsto 0\}$ (by assumption 2).

Let $j$ be the first step where $\mu(j)$ drops below $|A|$ . The clause $C$ introduced at that moment must be $\mathrm{cost\text{-}SR}$ w.r.t. $\Gamma_{j-1}$ , because the resolution steps do not change the set of optimal assignments. Let then $\sigma$ be the witnessing substitution used to derive $C$ , we have

\Gamma_{j-1}\!\upharpoonright_{\overline{C}}\ \ \vdash_{1}(\Gamma_{j-1}\cup\{C% \})\!\upharpoonright_{\sigma}\ .

(4)

Since $\mu(j)$ dropped below $|A|$ , clause $C$ must be incompatible with some $\tau\in A$ , that is $\tau\supseteq\overline{C}$ . Therefore, by cost preservation,

\mathrm{cost}(\tau\circ\sigma)\leq\mathrm{cost}(\tau)=k\;.

(5)

By ˜2.1, eq. (4) implies that

\Gamma_{j-1}\!\upharpoonright_{\tau}\ \ \vdash_{1}(\Gamma_{j-1}\cup\{C\})\!% \upharpoonright_{\tau\circ\sigma}\;.

Since $j$ was the first moment when $\mu(j)<|A|$ we have that $\tau\vDash\Gamma_{j-1}$ and therefore $\tau\circ\sigma\vDash\Gamma_{j-1}\cup\{C\}$ . In particular, $\tau\circ\sigma\vDash\Gamma$ . By eq. (5) then it must be $\tau\circ\sigma\in A$ . But then, by assumption 1, $\tau$ and $\tau\circ\sigma$ have Hamming distance at least $d$ , which implies $\operatorname{flip}(C,\sigma)\geq d$ . $\hfill\blacktriangleleft$

We see an example application of this result to $\mathrm{cost\text{-}LPR}$ , where the number of values allowed to be flipped by the rule is at most $1$ .

The formula $F=\{x\lor y\lor b_{1},\overline{x}\lor b_{2},\overline{y}\lor b_{3}\}$ has cost $1$ and its optimal assignments to variables $x,y,b_{1},b_{2},b_{3}$ are $\{00100,10010,01001\}$ . These assignments fulfil the premises of Theorem 5.1, with Hamming distance $>1$ . Therefore $\mathrm{cost\text{-}LPR}$ cannot prove the cost of $F$ to be $1$ , and hence $\mathrm{cost\text{-}LPR}$ is incomplete.

Corollary 5.2.

Proof systems $\mathrm{cost\text{-}LPR}$ , $\mathrm{cost\text{-}BC}$ are incomplete.

Corollary 5.3.

There is a formula family $F_{n}$ with $O(n)$ variables, $O(n)$ clauses and $\mathrm{cost}(F_{n})=\Omega(n)$ where, in order to prove $\mathrm{cost}(F_{n})\geq 1$ , any $\mathrm{cost\text{-}SR}$ proof derives a redundant clause with $\operatorname{flip}(C,\sigma)=\Omega(n)$ , where $\sigma$ is the witnessing substitution for $C$ .

Proof.

We define $F_{n}$ on variables $x_{0},x_{1},\ldots,x_{n}$ , and variables $y_{0},y_{1},\ldots,y_{n}$ . The formula contains hard clauses to encode the constraint $x_{0}\neq y_{0}$ , and constraints $x_{0}=x_{i}$ , $y_{0}=y_{i}$ for $i\in[n]$ . Furthermore $F_{n}$ has the soft clauses, encoded as hard clauses with blocking variables, $\neg x_{i}\lor b_{i}$ and $\neg y_{i}\lor b_{i+n}$ for $i\in[n]$ .

To satisfy the formula an assignment must either set all $x$ ’s to true and $y$ ’s to false, or vice versa. Both such assignments set to true $n$ of the blocking variables, and no blocking variable is fixed to a constant value. Therefore the claim follows from Theorem 5.1. $\hfill\blacktriangleleft$

Corollary 5.4.

Any $\mathrm{cost\text{-}SPR}$ proof for a formula respecting the hypothesis of Theorem 5.1 requires some redundant clauses of width at least $d$ .

Proof.

Any redundant clause $C$ derived in $\mathrm{cost\text{-}SPR}$ must have $|C|\geq\operatorname{flip}(C,\sigma)$ , and by Theorem 5.1, $\operatorname{flip}(C,\sigma)\geq d$ . $\hfill\blacktriangleleft$ For instance, the formula $F_{n}$ from Corollary 5.3 requires $\mathrm{cost\text{-}SPR}$ refutations of width $\Omega(n)$ .

6 Short proofs using redundancy rules

We show applications demonstarting the power of the redundancy rules on notable families of CNF formulas. In Section 6.1 we consider minimally unsatisfiable formulas, while in Section 6.2 we consider the weak Pigeonhole Principle.

$\blacktriangleright$ Remark 6.1.

Due to Theorem 4.2 and Theorem 4.3, we refer to a $\mathrm{cost\text{-}SPR}$ (resp. $\mathrm{cost\text{-}PR}$ , $\mathrm{cost\text{-}SR}$ ) derivation from $\Gamma$ of $b_{i_{1}},\dots,b_{i_{k}}$ for some distinct $k$ blocking literals and all the $\overline{b}_{j}$ for $j\notin\{i_{1},\dots,i_{k}\}$ , as a proof of $\mathrm{cost}(\Gamma)=k$ in $\mathrm{cost\text{-}SPR}$ (resp. $\mathrm{cost\text{-}PR}$ , $\mathrm{cost\text{-}SR}$ ).

6.1 Short proofs of minimally unsatisfiable formulas

Recall the definition of $\mathrm{PR}$ from [18] (see also [9, Definition 1.16]). A $\mathrm{PR}$ calculus refutation of a CNF formula $\Gamma$ is a sequence of clauses $D_{1},\dots,D_{t}$ where $D_{t}=\bot$ , and each $D_{i+1}$ is either a clause in $\Gamma$ , or derived by resolution, or is $\mathrm{PR}$ w.r.t. $\Gamma_{i}=\Gamma\cup\{D_{1},\dots,D_{i}\}$ , that is $D_{i+1}$ satisfies

\Gamma_{i}\!\upharpoonright_{\overline{D_{i+1}}}\ \vdash_{1}(\Gamma_{i}\cup\{D% _{i+1}\})|_{\sigma}\ ,

that is, Item 1 of Definition 3.2 for a $\sigma$ which is a partial assignment. A $\mathrm{PR}$ refutation is a $\mathrm{PR}$ derivation of $\bot$ . The size of a refutation is the number of clauses in it.

An unsatisfiable set $\Gamma$ of clauses is minimally unsatisfiable if no proper subset of $\Gamma$ is unsatisfiable.

Theorem 6.2.

If a minimally unsatisfiable CNF formula $\{C_{1},\dots,C_{m}\}$ has a $\mathrm{PR}$ refutation of size $s$ , then there is a $\mathrm{cost\text{-}PR}$ proof of $\mathrm{cost}(\{C_{1}\lor b_{1},\dots,C_{m}\lor b_{m}\})=1$ of at most $\mathcal{O}(s+m)$ many clauses.

Proof.

Let $F=\{C_{1},\dots,C_{m}\}$ and $\Gamma=\{C_{1}\lor\penalty 10000b_{1},\penalty 1000\dots,\penalty 1000C_{m}% \lor\penalty 10000b_{m}\}$ be the corresponding MaxSAT instance. Let $\pi=(D_{1},\dots,D_{s})$ be a $\mathrm{PR}$ refutation of $F$ , so $D_{s}=\bot$ . First we show that

\pi_{B}=(D_{1}\lor B,\dots,D_{s}\lor B)\;,

with $B=\bigvee_{i\in[m]}b_{i}$ , is a valid $\mathrm{cost\text{-}PR}$ derivation of $B$ from $\Gamma$ . In particular, assuming we already derived the first $i$ steps of $\pi_{B}$ , we show how to derive $D_{i+1}\lor B$ .

When $D_{i+i}\in F$ , the clause $D_{i+i}\lor B$ is the weakening of some clause in $\Gamma$ . If $D_{i+1}$ was derived using a resolution rule on some premises in $\pi$ , then $D_{i+i}\lor B$ can be derived in the same way from the corresponding premises in $\pi_{B}$ . The remaining case is when $D_{i+1}$ is $\mathrm{PR}$ w.r.t. $F_{i}=F\cup\{D_{1},\ldots,D_{i}\}$ . Let $\alpha$ be the assignment that witnesses it. This assignment only maps variables from the original formula $F$ , so we extend it to $\alpha^{\prime}=\alpha\cup\{b_{1}\mapsto 0,\ldots,b_{m}\mapsto 0\}$ , and then use $\alpha^{\prime}$ to witness that indeed $D_{i+1}\lor B$ is $\mathrm{cost\text{-}PR}$ w.r.t. $\Gamma_{i}=\Gamma\cup\{D_{1}\lor B,\ldots D_{i}\lor B\}$ . For the cost condition in Definition 3.2, just observe that any extension of $\alpha^{\prime}$ has cost $0$ . For the redundancy condition, observe that, by construction, $\Gamma_{i}\!\upharpoonright_{\overline{D_{i+1}}\wedge\overline{B}}=F_{i}\!% \upharpoonright_{\overline{D_{i+1}}}$ , $(F_{i}\cup\{D_{i+1}\})\!\upharpoonright_{\alpha}=(\Gamma_{i}\cup\{D_{i+1}\lor B% \})\!\upharpoonright_{\alpha^{\prime}}$ , and $F_{i}\!\upharpoonright_{\overline{D_{i+1}}}\vdash_{1}(F_{i}\cup\{D_{i+1}\})\!% \upharpoonright_{\alpha}$ .

The last clause of $\pi_{B}$ is $B$ . Let $\alpha_{opt}$ be an optimal assignment of $\Gamma$ . Since $F$ is minimally unsatisfiable, $\mathrm{cost}(\alpha_{opt})=1$ . W.l.o.g. assume $\alpha_{opt}$ sets $b_{m}=1$ and all $b_{i}=0$ for $i<m$ .

Now, for each $i<m$ , the clause $E_{i}=\overline{b}_{i}\lor b_{m}$ is $\mathrm{cost\text{-}PR}$ w.r.t. $\pi_{B}\cup\{E_{j}:j<i\}$ , using $\alpha_{opt}$ itself as the witnessing assignment: redundancy holds since $\alpha_{opt}$ satisfies every clause in $\pi_{B}$ and all clauses $E_{j}$ . The cost condition follow since $\mathrm{cost}(\tau)\geq 1$ for any $\tau\supseteq\overline{E_{i}}$ and $\mathrm{cost}(\tau\circ\alpha_{opt})=\mathrm{cost}(\alpha_{opt})=1$ .

In the end we use $O(m)$ steps to derive $b_{m}$ from $B$ and $E_{1},\dots,E_{m-1}$ , and to derive in $\mathrm{cost\text{-}PR}$ calculus all the units $\overline{b}_{1},\dots,\overline{b}_{m-1}$ via Lemma 4.1. $\hfill\blacktriangleleft$

Theorem 6.2 shows that the propositional refutations for the minimally unsatisfiable formulas in [9] translate immediately to certificates in the MaxSAT. In particular, as a corollary of Theorem 6.2, we have that $\mathrm{cost\text{-}PR}$ proves in polynomial size that

$\blacksquare$

the Pigeonhole Principle with $n+1$ pigeons and $n$ holes [9, Theorem 4.3] and [19, Section 5],
$\blacksquare$

the Bit-Pigeonhole Principle [9, Theorem 4.4],
$\blacksquare$

the Parity Principle [9, Theorem 4.6],
$\blacksquare$

the Tseitin Principle on a connected graph [9, Theorem 4.10],

have all cost 1, since they are all minimally unsatisfiable. In MaxSAT resolution that would require exponentially long derivations.

6.2 Short proofs of the minimum cost of $\mathsf{PHP}^{m}_{n}$

Let $m>n\geq 1$ . The pigeonhole principle from $m$ pigeons to $n$ holes, with blocking variables, has the following formulation, that we call $\mathsf{bPHP}^{m}_{n}$ : the totality clauses $\bigvee_{j\in[n]}p_{i,j}\lor b_{i}$ for $i\in[m]$ , and the injectivity clauses $\overline{p}_{i,j}\lor\overline{p}_{k,j}\lor b_{i,k,j}$ for $1\leq i<k\leq m$ and $j\in[n]$ . We use $b_{k,i,j}$ as an alias of the variable $b_{i,k,j}$ , given that $i<k$ .

Theorem 6.3.

$\mathrm{cost\text{-}SR}$ proves $\mathrm{cost}(\mathsf{bPHP}^{m}_{n})=m-n$ in polynomial size.

This is the main result of the section. Before proving it we show two useful lemmas. The first lemma is used to “clean up” the set of clauses during a derivation. For each new step in a $\mathrm{cost\text{-}SR}$ calculus derivation the redundancy condition must be checked against an ever increasing set of clauses. It turns out that some already derived clauses can be completely ignored for the rest of the derivation under some technical conditions. This makes up for the lack of a deletion rule, that we do not have, and in the context of SAT seems to give more power to the systems [9].

Lemma 6.4.

Let $\Gamma$ and $\Sigma$ be two sets of clauses. Any $\mathrm{cost\text{-}SR}$ derivation $D_{1}\ldots,D_{t}$ from $\Gamma$ is also a valid derivation from $\Gamma\cup\Sigma$ if either of the two cases applies

1.

Variables in $\Sigma$ do not occur in $\Gamma\cup\{D_{1},\ldots,D_{t}\}$ .
2.

For every clause $C\in\Sigma$ there is a clause $C^{\prime}\in\Gamma$ so that $C^{\prime}\subseteq C$ .

Proof.

The cost condition does not depend on the set of clauses, therefore we only need to check the validity of the redundancy condition. In the first case, the redundancy condition applies because the clauses of $\Sigma$ are unaffected by the substitutions involved.

For the second case, consider the derivation of a clause $D_{i}$ witnessed by $\sigma_{i}$ . The clauses in $\Sigma\!\upharpoonright_{\overline{D_{i}}}$ and $\Sigma\!\upharpoonright_{\sigma_{i}}$ are subsumed by clauses in $\Gamma\!\upharpoonright_{\overline{D_{i}}}$ and $\Gamma\!\upharpoonright_{\sigma_{i}}$ , respectively. Hence

(\Gamma\cup\{D_{1},\ldots,D_{i-1}\})\!\upharpoonright_{\overline{D_{i}}}\vdash% _{1}(\Gamma\cup\Sigma\cup\{D_{1},\ldots,D_{i}\})\!\upharpoonright_{\sigma_{i}}

which implies the validity of the redundancy condition. $\hfill\blacktriangleleft$

The second lemma is used as a general condition to enforce clauses to be $\mathrm{cost\text{-}SR}$ .

Lemma 6.5.

Let $C$ be a clause and $\Gamma$ a set of clauses. If there exists a permutation $\pi$ such that

1.

$\pi$ maps the set of blocking variables to itself,
2.

the substitution $\overline{C}\circ\pi$ satisfies $C$ , and $\Gamma\!\upharpoonright_{\overline{C}}\supseteq\Gamma\!\upharpoonright_{% \overline{C}\,\circ\,\pi}$ ,

then $C$ is $\mathrm{cost\text{-}SR}$ w.r.t. $\Gamma$ . Notice that the second condition in item (2) is automatically satisfied if $\pi$ is a symmetry of $\Gamma$ , i.e. $\Gamma=\Gamma\!\upharpoonright_{\pi}$ .

Proof.

The cost condition follows from Item 1. The redundancy condition is immediate by Item 2 using as $\sigma$ the substitution $\overline{C}\circ\pi$ . $\hfill\blacktriangleleft$

Proof of Theorem 6.3.

The proof is by induction. The goal is to reduce the formula to $m-1$ pigeons and $n-1$ holes. First we do some preprocessing: from $\mathsf{bPHP}^{m}_{n}$ we derive a slightly more structured formula $\mathsf{F}^{m}_{n}$ . Then we show how to derive $\mathsf{F}^{m-1}_{n-1}$ in a polynomial number of steps. The results follows because after $n$ such derivations we obtain the formula $\mathsf{F}^{m-n}_{0}$ that contains the clauses $b_{1},\dots,b_{m-n}$ . Moreover, we also derive $\overline{b_{m-n+1}},\dots,\overline{b_{m}}$ along the way.

We derive $\mathsf{F}^{m-1}_{n-1}$ from $\mathsf{F}^{m}_{n}$ using the rules of $\mathrm{cost\text{-}SR}$ calculus. We divide the argument into several steps, but first we show how to derive $\mathsf{F}^{m}_{n}$ from $\mathsf{bPHP}^{m}_{n}$ .

Preprocessing 1.

“Make $b_{i}$ full-fledged extension variables”. ⁴⁴4This is true in general: if a MaxSAT instance contains a clause $C\lor b$ then it is possible to make the blocking variable $b$ a full-fledged extension variable ( $b\leftrightarrow\overline{C}$ ) by $\mathrm{cost\text{-}LPR}$ . Turn all the variables $b_{i}$ into full-fledged extension variables that satisfy $b_{i}\leftrightarrow\neg(p_{i,1}\lor\cdots\lor p_{i,n})$ , by adding the clauses

\mathsf{Ext}=\{\overline{p_{i,j}}\lor\overline{b_{i}}:i\in[m],j\in[n]\}

one by one in $\mathrm{cost\text{-}LPR}$ .

We need to derive clause $D_{j}=\overline{p_{1,j}}\lor\overline{b_{1}}$ for every $j\in[n]$ . Assume that we already got $D_{1},\ldots,D_{j-1}$ , we derive $D_{j}$ as a $\mathrm{cost\text{-}LPR}$ clause w.r.t. $\mathsf{bPHP}^{m}_{n}\cup\{D_{1},\ldots,D_{j-1}\}$ . The witnessing assignment is $\sigma_{j}:=\{p_{1,j}=1,b_{1}=0\}$ . Since $\overline{D_{j}}=\{p_{1,j}=\penalty 100001,b_{1}=1\}$ , the cost condition is satisfied. The redundancy condition follows from

\mathsf{bPHP}^{m}_{n}\!\upharpoonright_{\overline{D_{j}}}\supseteq(\mathsf{% bPHP}^{m}_{n}\cup\{D_{1},\ldots,D_{j}\})\!\upharpoonright_{\sigma_{j}}\;.

Indeed, on clauses of $\mathsf{bPHP}^{m}_{n}$ that do not contain the variable $b_{j}$ , the assignments $\overline{D_{j}}$ and $\sigma_{j}$ behave identically, while all the clauses containing $b_{j}$ are satisfied by $\sigma_{j}$ . Repeat the previous argument to get all the clauses $\overline{p_{i,j}}\lor\overline{b_{i}}$ . The current database of clauses is $\mathsf{bPHP}^{m}_{n}\cup\mathsf{Ext}$ .

Preprocessing 2.

“Enforce injectivity”. Optimal assignments for $\mathsf{bPHP}^{m}_{n}$ can have unassigned pigeons or have collisions between pigeons. It is more convenient to avoid collisions and just focus on assignments that are partial matching. A moment’s thought suffices to realize that such restriction does not change the optimal cost but simplifies the solution space. We enforce collisions to never occur by deriving all the unit clauses $\overline{b_{i,k,j}}$ by $\mathrm{cost\text{-}PR}$ .

These clauses can be derived in any particular order: to show that $\overline{b_{i,k,j}}$ is $\mathrm{cost\text{-}SR}$ w.r.t. $\Gamma_{0}$ and the previously derived $\overline{b_{i^{\prime},k^{\prime},j^{\prime}}}$ we pick one of the two pigeons involved (say $k$ ) and use $\sigma=\{b_{i,k,j}=0,b_{k}=1,p_{k,1}=\dots=p_{k,n}=0\}$ as the witnessing assignment. The cost is not increased, and to check the redundancy condition observe that $\sigma$ satisfies all the clauses that touches, so on the right side of the redundancy condition has a subset of $\mathsf{bPHP}^{m}_{n}\cup\mathsf{Ext}$ with no occurrences $b_{i,k,j}$ , while the left side has the same set of clauses, but restricted with $b_{i,k,j}=0$ .

Now that we have all clauses $\overline{b_{i,k,j}}$ we resolve them with the corresponding clauses $\overline{p_{i,j}}\lor\overline{p_{k,j}}\lor b_{i,k,j}$ to get the set of clauses

\mathsf{Inj}=\{\overline{p_{i,j}}\lor\overline{p_{k,j}}:1\leq i<k\leq m\text{ % and }j\in[n]\}\ ,

for all holes $j$ and pair of pigeons $i$ and $k$ .

We do not need variables $b_{i,k,j}$ anymore. By one application of Lemma 6.4, from now on we can ignore all clauses $\overline{p_{i,j}}\lor\overline{p_{k,j}}\lor b_{i,k,j}$ . By another application, we can also ignore the clauses $\overline{b_{i,k,j}}$ . We will do induction on the current database of clauses.

For clarity we list all its clauses again.

Formula $\mathsf{F}^{m}_{n}\quad$ $\bigvee_{j\in[n]}p_{i,j}\lor b_{i}$ for $i\in[m]$ (totality 1), $\overline{p_{i,j}}\lor\overline{b_{i}}$ for $i\in[m]$ and $j\in[n]$ (totality 2), $\overline{p_{i,j}}\lor\overline{p_{k,j}}$ for $1\leq i<k\leq m$ and $j\in[n]$ (injectivity).

The core idea of the induction is that if a pigeon flies to a hole, we can assume without loss of generality that it is pigeon $m$ that flies into hole $n$ .

Step 0.

“If some pigeon $i$ flies, we can assume it is pigeon $m$ who flies”. We want to derive, in this order, the set of clauses

\Delta_{1}=\{\overline{b_{m}}\lor b_{1},\overline{b_{m}}\lor b_{2},\ldots,% \overline{b_{m}}\lor b_{(m-1)}\}

from $\mathsf{F}^{m}_{n}$ , to claim that if some pigeon is mapped, then pigeon $m$ is mapped too. For each $C_{i}=\overline{b_{m}}\lor b_{i}$ we apply Lemma 6.5 using as the witnessing permutation $\pi_{i}$ , the permutation that swaps pigeons $m$ and $i$ .

Namely, $\pi_{i}(p_{m,j})=p_{i,j}$ , $\pi_{i}(p_{i,j})=p_{m,j}$ , $\pi_{i}(b_{m})=b_{i}$ , $\pi_{i}(b_{i})=b_{m}$ , and $\pi_{i}$ is the identity on all other variables, therefore $\pi_{i}$ satisfies the first requirement for the lemma. Likewise $\overline{C_{i}}\circ\pi_{i}\vDash C_{i}$ , and we need to check that

(\mathsf{F}^{m}_{n}\cup\{C_{1},\ldots,C_{(i-1)}\})\!\upharpoonright_{\overline% {C_{i}}}\supseteq(\mathsf{F}^{m}_{n}\cup\{C_{1},\ldots,C_{(i-1)}\})\!% \upharpoonright_{\overline{C_{i}}\,\circ\,\pi_{i}}\;.

By symmetry $\mathsf{F}^{m}_{n}\!\upharpoonright_{\overline{C_{i}}}=\mathsf{F}^{m}_{n}\!% \upharpoonright_{\overline{C_{i}}\,\circ\,\pi_{i}}$ , and for $1\leq i^{\prime}<i$ , $C_{i^{\prime}}\!\upharpoonright_{\overline{C_{i}}\,\circ\,\pi_{i}}=1$ , hence the inclusion is true. The current database of clauses is $\Gamma_{1}=\mathsf{F}^{m}_{n}\cup\Delta_{1}$ .

Step 1.

“If pigeon $m$ flies to some hole, we can assume it flies to hole $n$ ”. Using $\mathrm{cost\text{-}SR}$ inferences, we derive from $\Gamma_{1}$ , in this order, the clauses

\Delta_{2}=\{\overline{p_{m,1}}\lor p_{m,n},\overline{p_{m,2}}\lor p_{m,n},% \ldots,\overline{p_{m,(n-1)}}\lor p_{m,n}\}

expressing that if pigeon $m$ flies to some hole, this hole is the last one.

For each $C_{j}=\overline{p_{m,j}}\lor p_{m,n}$ we apply Lemma 6.5 with the witnessing permutation $\pi_{j}$ swapping holes $n$ and $j$ .

Namely $\pi_{j}(p_{i,n})=p_{i,j}$ and $\pi_{j}(p_{i,j})=p_{i,n}$ , and $\pi_{j}$ is the identity on all other variables. By construction $\pi_{j}$ satisfies the first requirement for the lemma, and likewise $\overline{C_{j}}\circ\pi_{j}\vDash C_{j}$ , and, again, we need to check

(\Gamma_{1}\cup\{C_{1},\ldots,C_{(j-1)}\})\!\upharpoonright_{\overline{C_{j}}}% \supseteq(\Gamma_{1}\cup\{C_{1},\ldots,C_{(j-1)}\})\!\upharpoonright_{% \overline{C_{j}}\,\circ\,\pi_{j}}\;.

By symmetry $\Gamma_{1}\!\upharpoonright_{\overline{C_{j}}}=\Gamma_{1}\!\upharpoonright_{% \overline{C_{j}}\,\circ\,\pi_{j}}$ , and for $1\leq j^{\prime}<j$ , $C_{j^{\prime}}\!\upharpoonright_{\overline{C_{j}}\,\circ\,\pi_{j}}=1$ , hence the inclusion is true. The current database of clauses is $\Gamma_{2}=\Gamma_{1}\cup\Delta_{2}=\mathsf{F}^{m}_{n}\cup\Delta_{1}\cup\Delta% _{2}$ .

Step 2.

“Obtain $\overline{p_{k,n}}$ for every $1\leq k<m$ via resolution”. Resolve the clause $(p_{m,1}\lor p_{m,2}\lor\dots\lor p_{m,n}\lor b_{m})$ (totality 1) with $\overline{p_{m,n}}\lor\overline{p_{k,n}}$ , the resulting clause with all clauses $\overline{p_{m,j}}\lor p_{m,n}$ from step 2, to get $b_{m}\lor p_{m,n}\lor\overline{p_{k,n}}$ . Then resolve $b_{m}\lor p_{m,n}\lor\overline{p_{k,n}}$ again with the injectivity clause $\overline{p_{m,n}}\lor\overline{p_{k,n}}$ , then the result with clause $\overline{b_{m}}\lor b_{k}$ (from step 1), and again this latter result with clause $\overline{b_{k}}\lor\overline{p_{k,n}}$ (totality 2). The final result is $\overline{p_{k,n}}$ .

The clauses $\overline{p_{k,n}}$ subsume the clauses in $\mathsf{Inj}$ of the form $\overline{p_{m,n}}\lor\overline{p_{k,n}}$ and all the intermediate clauses from the previous resolution steps. Therefore we use Lemma 6.4 to be able to ignore the subsumed clauses.

The current database of clauses is $\Gamma_{3}$ is equal to

\mathsf{F}^{m}_{n}\cup\Delta_{1}\cup\Delta_{2}\cup\{\overline{p_{k,n}}:1\leq k% <m\}\setminus\{\overline{p_{m,n}}\lor\overline{p_{k,n}}:1\leq k<m\}.

Step 3.

“Assign pigeon $m$ to hole $n$ : derive unit clauses $p_{m,n}$ and $\overline{b_{m}}$ ”. The goal is to enforce pigeon $m$ to be mapped to hole $n$ , by deriving the clause $p_{m,n}$ using the $\mathrm{cost\text{-}PR}$ rule. Then we get $\overline{b_{m}}$ immediately by resolving $p_{m,n}$ with $\overline{p_{m,n}}\lor\overline{b_{m}}$ (totality 2).

The unit clause $p_{m,n}$ is $\mathrm{cost\text{-}PR}$ w.r.t. $\Gamma_{3}$ , using partial assignment $\sigma=\{p_{m,n}=1,b_{m}=0\}$ as witness.

Clearly $\sigma$ satisfies the cost condition. To see that the redundancy condition holds as well, we need to show that $\Gamma_{3}|_{\overline{C}}\vdash_{1}D|_{\sigma}$ for all $D$ in $\Gamma_{3}$ that contain $\overline{p_{m,n}}$ , but the only such clause that remains in $\Gamma_{3}$ is $\overline{p_{m,n}}\lor\overline{b_{m}}$ , which is satisfied by $\sigma$ . The current database of clauses is $\Gamma_{4}=\Gamma_{3}\cup\{p_{m,n},\overline{b_{m}}\}$ .

Step 4.

“Derive $\overline{p_{m,1}},\dots,\overline{p_{m,(n-1)}}$ by $\mathrm{cost\text{-}SR}$ ”. We can derive them in any order using as witnessing substitution of the $\mathrm{cost\text{-}SR}$ rule the assignment $\sigma$ setting $p_{m,n}=1$ , $p_{m,1}=\dots=p_{m,(n-1)}=0$ , and $b_{m}=0$ .

The cost condition is immediate, and the redundancy condition follows from the fact that $\Gamma_{4}\!\upharpoonright_{\sigma}\subseteq\Gamma_{4}$ .

Step 5.

“Reduction to $m-1$ pigeons and $n-1$ holes”. First we derive by unit propagation all the the totality clauses of $\mathsf{F}^{m-1}_{n-1}$ . That is, we remove the hole $n$ from the totality axioms of the pigeons $1,\dots,m-1$ in the current database. Now, the current database is $\mathsf{F}^{m-1}_{n-1}$ , the unit clauses $\overline{b_{m}}$ , $p_{m,n}$ , $\overline{p_{k,n}}$ for $k\neq m$ and $\overline{p_{m,j}}$ for $j\neq n$ , and clauses that are subsumed by one of these unit clauses. Therefore by Lemma 6.4 we can ignore all the unit clauses and all the clauses subsumed by them. That is we can carry on the derivation using only $\mathsf{F}^{m-1}_{n-1}$ .

Thus steps (1)–(6) are repeated $n-1$ times, up to derive $\mathsf{F}^{m-n}_{0}$ .

The unit clauses derived in the whole process include

$\blacksquare$

$b_{1},\dots,b_{(m-n)}$ (totality clauses in $\mathsf{F}^{m-n}_{0}$ ).
$\blacksquare$

$\overline{b_{n+1}},\dots,\overline{b_{m}}$ (derived at each step of the induction),
$\blacksquare$

$\overline{b_{i,k,j}}$ for all $i<k$ and $j$ (derived at the preprocessing).

Therefore $\mathrm{cost}(\mathsf{bPHP}^{m}_{n})=m-n$ . $\hfill\blacktriangleleft$

7 Conclusions and open problems

We proposed a way to extend redundancy rules, originally introduced for SAT, into polynomially verifiable rules for MaxSAT. We defined sound and complete calculi based on those rules and we showed the strength of some of the calculi giving short derivations of notable principles and we showed the incompleteness of the weaker ones and width lower bounds for the stronger ones. We conclude this article with a list of open problems:

1.

The cost constraint for the redundancy rules is very strict, for example compared to the rule CPR in [21]. Indeed, $\mathrm{cost\text{-}PR}$ enforces the check on the cost even on assignments falsifying the hard clauses of the formula. Is it possible to relax $\mathrm{cost\text{-}PR}$ without giving up on efficient verification as in [21]?
2.

Does $\mathrm{cost\text{-}SR}$ simulate MaxSAT Resolution? That is, if we have a MaxSAT instance $\Gamma$ with blocking variables and MaxSAT Resolution proves in size $s$ that $\mathrm{cost}(\Gamma)=k$ , is there a proof of $\mathrm{cost}(\Gamma)=k$ in $\mathrm{cost\text{-}SR}$ of size $\mathsf{poly}(s)$ ?
3.

We proved a width lower bound for $\mathrm{cost\text{-}SPR}$ and an analogue of a width lower bound for $\mathrm{cost\text{-}SR}$ on formulas with optimal assignments far from each other in the Hamming distance. We reiterate the open problem of proving size lower bounds for $\mathrm{cost\text{-}SPR}$ and stronger systems.

References

[1] Carlos Ansótegui, Maria Luisa Bonet, and Jordi Levy. SAT-based MaxSAT algorithms. Artif. Intell., 196:77–105, 2013. doi:10.1016/J.ARTINT.2013.01.002.
[2] Fahiem Bacchus, Matti Järvisalo, and Ruben Martins. Maximum satisfiabiliy. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 929–991. IOS Press, 2021. doi:10.3233/FAIA201008.
[3] Jeremias Berg, Bart Bogaerts, Jakob Nordström, Andy Oertel, and Dieter Vandesande. Certified core-guided MaxSAT solving. In Proceedings of the 29th International Conference on Automated Deduction (CADE), volume 14132, pages 1–22, 2023. doi:10.1007/978-3-031-38499-8_1.
[4] Jeremias Berg and Matti Järvisalo. Unifying reasoning and core-guided search for maximum satisfiability. In Proceedings of the 16th European Conference on Logics in Artificial Intelligence (JELIA), volume 11468, pages 287–303, 2019. doi:10.1007/978-3-030-19570-0_19.
[5] Bart Bogaerts, Stephan Gocht, Ciaran McCreesh, and Jakob Nordström. Certified dominance and symmetry breaking for combinatorial optimisation. Journal of Artificial Intelligence Research, 77:1539–1589, 2023. doi:10.1613/JAIR.1.14296.
[6] Ilario Bonacina, Maria Luisa Bonet, and Massimo Lauria. MaxSAT Resolution with Inclusion Redundancy. In Proceedings of the 27th International Conference on Theory and Applications of Satisfiability Testing (SAT), volume 305, pages 7:1–7:15, 2024. doi:10.4230/LIPIcs.SAT.2024.7.
[7] Maria Luisa Bonet, Sam Buss, Alexey Ignatiev, João Marques-Silva, and António Morgado. MaxSAT resolution with the dual rail encoding. In Proceedings of the 32nd AAAI Conference on Artificial Intelligence, (AAAI), the 30th innovative Applications of Artificial Intelligence (IAAI), and the 8th AAAI Symposium on Educational Advances in Artificial Intelligence (EAAI), pages 6565–6572, 2018. doi:10.1609/AAAI.V32I1.12204.
[8] Maria Luisa Bonet, Jordi Levy, and Felip Manyà. Resolution for Max-SAT. Artificial Intelligence, 171(8-9):606–618, 2007. doi:10.1016/J.ARTINT.2007.03.001.
[9] Sam Buss and Neil Thapen. DRAT and propagation redundancy proofs without new variables. Logical Methods in Computer Science, 17(2), 2021. URL: https://lmcs.episciences.org/7400.
[10] Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. Journal of Symbolic Logic, 44(1):36–50, 1979. doi:10.2307/2273702.
[11] Jessica Davies and Fahiem Bacchus. Solving MAXSAT by solving a sequence of simpler SAT instances. In Proceedings of the 17th International Conference on Principles and Practice of Constraint Programming (CP), pages 225–239, 2011. doi:10.1007/978-3-642-23786-7_19.
[12] Zhaohui Fu and Sharad Malik. On solving the partial MAX-SAT problem. In Proceedings of the 9th International Conference on Theory and Applications of Satisfiability Testing (SAT), pages 252–265, 2006. doi:10.1007/11814948_25.
[13] Michel X. Goemans and David P. Williamson. New $\frac{3}{4}$ -approximation algorithms for the maximum satisfiability problem. SIAM Journal on Discrete Mathematics, 7(4):656–666, 1994. doi:10.1137/S0895480192243516.
[14] Marijn Heule, Warren A. Hunt Jr., and Nathan Wetzler. Trimming while checking clausal proofs. In Proceedings of the conference on Formal Methods in Computer-Aided Design (FMCAD), pages 181–188, 2013. URL: https://ieeexplore.ieee.org/document/6679408/.
[15] Marijn Heule, Warren A. Hunt Jr., and Nathan Wetzler. Verifying refutations with extended resolution. In Proceedings of the 24th International Conference on Automated Deduction (CADE), volume 7898, pages 345–359, 2013. doi:10.1007/978-3-642-38574-2_24.
[16] Marijn Heule, Warren A. Hunt Jr., and Nathan Wetzler. Expressing symmetry breaking in DRAT proofs. In Proceedings of the 25th International Conference on Automated Deduction (CADE), volume 9195, pages 591–606, 2015. doi:10.1007/978-3-319-21401-6_40.
[17] Marijn J. H. Heule and Armin Biere. What a difference a variable makes. In Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS), volume 10806, pages 75–92, 2018. doi:10.1007/978-3-319-89963-3_5.
[18] Marijn J. H. Heule, Benjamin Kiesl, and Armin Biere. Short proofs without new variables. In Proceedings of the 26th International Conference on Automated Deduction (CADE), volume 10395, pages 130–147, 2017. doi:10.1007/978-3-319-63046-5_9.
[19] Marijn J. H. Heule, Benjamin Kiesl, and Armin Biere. Strong extension-free proof systems. Journal of Automated Reasoning, 64(3):533–554, 2019. Extended version of [18]. doi:10.1007/s10817-019-09516-0.
[20] Marijn J. H. Heule, Benjamin Kiesl, Martina Seidl, and Armin Biere. Pruning through satisfaction. In Proceedings of the Hardware and Software: Verification and Testing - 13th International Haifa Verification Conference (HVC), volume 10629, pages 179–194, 2017. doi:10.1007/978-3-319-70389-3_12.
[21] Hannes Ihalainen, Jeremias Berg, and Matti Järvisalo. Clause redundancy and preprocessing in maximum satisfiability. In Proceedings of the 11th International Joint Conference on Automated Reasoning (IJCAR), volume 13385, pages 75–94, 2022. doi:10.1007/978-3-031-10769-6_6.
[22] Matti Järvisalo, Marijn Heule, and Armin Biere. Inprocessing rules. In Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR), volume 7364, pages 355–370, 2012. doi:10.1007/978-3-642-31365-3_28.
[23] Benjamin Kiesl, Adrián Rebola-Pardo, and Marijn J. H. Heule. Extended resolution simulates DRAT. In Proceedings of the 9th International Joint Conference on Automated Reasoning (IJCAR), Held as Part of the Federated Logic Conference, FloC 2018, volume 10900, pages 516–531, 2018. doi:10.1007/978-3-319-94205-6_34.
[24] Leszek Aleksander Kołodziejczyk and Neil Thapen. The Strength of the Dominance Rule. In Proceedings of the 27th International Conference on Theory and Applications of Satisfiability Testing (SAT), volume 305, pages 20:1–20:22, 2024. doi:10.4230/LIPIcs.SAT.2024.20.
[25] Oliver Kullmann. On a generalization of extended resolution. Discrete Applied Mathematics, 96-97:149–176, 1999. doi:10.1016/S0166-218X(99)00037-2.
[26] Javier Larrosa and Federico Heras. Resolution in max-sat and its relation to local consistency in weighted csps. In Proceedings of the 19h International Joint Conference on Artificial Intelligence (IJCAI), pages 193–198, 2005. URL: http://ijcai.org/Proceedings/05/Papers/0360.pdf.
[27] António Morgado, Carmine Dodaro, and João Marques-Silva. Core-guided MaxSAT with soft cardinality constraints. In Proceedings of the 20th International Conference on Principles and Practice of Constraint Programming (CP), pages 564–573, 2014. doi:10.1007/978-3-319-10428-7_41.
[28] António Morgado, Federico Heras, Mark H. Liffiton, Jordi Planes, and João Marques-Silva. Iterative and core-guided MaxSAT solving: A survey and assessment. Constraints An Int. J., 18(4):478–534, 2013. doi:10.1007/S10601-013-9146-2.
[29] Nina Narodytska and Fahiem Bacchus. Maximum satisfiability using core-guided MaxSAT resolution. In Proceedings of the 28th Conference on Artificial Intelligence (AAAI), pages 2717–2723, 2014. doi:10.1609/AAAI.V28I1.9124.
[30] Adrián Rebola-Pardo and Martin Suda. A theory of satisfiability-preserving proofs in SAT solving. In Proceedings of the 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), volume 57, pages 583–603, 2018. doi:10.29007/TC7Q.
[31] Paul Saikko, Jeremias Berg, and Matti Järvisalo. LMHS: a SAT-IP hybrid MaxSAT solver. In Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing (SAT), pages 539–546, 2016. doi:10.1007/978-3-319-40970-2_34.

[bib.bib1] [1] Carlos Ansótegui, Maria Luisa Bonet, and Jordi Levy. SAT-based MaxSAT algorithms. Artif. Intell., 196:77–105, 2013. doi:10.1016/J.ARTINT.2013.01.002.

[bib.bib2] [2] Fahiem Bacchus, Matti Järvisalo, and Ruben Martins. Maximum satisfiabiliy. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 929–991. IOS Press, 2021. doi:10.3233/FAIA201008.

[bib.bib3] [3] Jeremias Berg, Bart Bogaerts, Jakob Nordström, Andy Oertel, and Dieter Vandesande. Certified core-guided MaxSAT solving. In Proceedings of the 29th International Conference on Automated Deduction (CADE), volume 14132, pages 1–22, 2023. doi:10.1007/978-3-031-38499-8_1.

[bib.bib4] [4] Jeremias Berg and Matti Järvisalo. Unifying reasoning and core-guided search for maximum satisfiability. In Proceedings of the 16th European Conference on Logics in Artificial Intelligence (JELIA), volume 11468, pages 287–303, 2019. doi:10.1007/978-3-030-19570-0_19.

[bib.bib5] [5] Bart Bogaerts, Stephan Gocht, Ciaran McCreesh, and Jakob Nordström. Certified dominance and symmetry breaking for combinatorial optimisation. Journal of Artificial Intelligence Research, 77:1539–1589, 2023. doi:10.1613/JAIR.1.14296.

[bib.bib6] [6] Ilario Bonacina, Maria Luisa Bonet, and Massimo Lauria. MaxSAT Resolution with Inclusion Redundancy. In Proceedings of the 27th International Conference on Theory and Applications of Satisfiability Testing (SAT), volume 305, pages 7:1–7:15, 2024. doi:10.4230/LIPIcs.SAT.2024.7.

[bib.bib7] [7] Maria Luisa Bonet, Sam Buss, Alexey Ignatiev, João Marques-Silva, and António Morgado. MaxSAT resolution with the dual rail encoding. In Proceedings of the 32nd AAAI Conference on Artificial Intelligence, (AAAI), the 30th innovative Applications of Artificial Intelligence (IAAI), and the 8th AAAI Symposium on Educational Advances in Artificial Intelligence (EAAI), pages 6565–6572, 2018. doi:10.1609/AAAI.V32I1.12204.

[bib.bib8] [8] Maria Luisa Bonet, Jordi Levy, and Felip Manyà. Resolution for Max-SAT. Artificial Intelligence, 171(8-9):606–618, 2007. doi:10.1016/J.ARTINT.2007.03.001.

[bib.bib9] [9] Sam Buss and Neil Thapen. DRAT and propagation redundancy proofs without new variables. Logical Methods in Computer Science, 17(2), 2021. URL: https://lmcs.episciences.org/7400.

[bib.bib10] [10] Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. Journal of Symbolic Logic, 44(1):36–50, 1979. doi:10.2307/2273702.

[bib.bib11] [11] Jessica Davies and Fahiem Bacchus. Solving MAXSAT by solving a sequence of simpler SAT instances. In Proceedings of the 17th International Conference on Principles and Practice of Constraint Programming (CP), pages 225–239, 2011. doi:10.1007/978-3-642-23786-7_19.

[bib.bib12] [12] Zhaohui Fu and Sharad Malik. On solving the partial MAX-SAT problem. In Proceedings of the 9th International Conference on Theory and Applications of Satisfiability Testing (SAT), pages 252–265, 2006. doi:10.1007/11814948_25.

[bib.bib13] [13] Michel X. Goemans and David P. Williamson. New $\frac{3}{4}$ -approximation algorithms for the maximum satisfiability problem. SIAM Journal on Discrete Mathematics, 7(4):656–666, 1994. doi:10.1137/S0895480192243516.

[bib.bib14] [14] Marijn Heule, Warren A. Hunt Jr., and Nathan Wetzler. Trimming while checking clausal proofs. In Proceedings of the conference on Formal Methods in Computer-Aided Design (FMCAD), pages 181–188, 2013. URL: https://ieeexplore.ieee.org/document/6679408/.

[bib.bib15] [15] Marijn Heule, Warren A. Hunt Jr., and Nathan Wetzler. Verifying refutations with extended resolution. In Proceedings of the 24th International Conference on Automated Deduction (CADE), volume 7898, pages 345–359, 2013. doi:10.1007/978-3-642-38574-2_24.

[bib.bib16] [16] Marijn Heule, Warren A. Hunt Jr., and Nathan Wetzler. Expressing symmetry breaking in DRAT proofs. In Proceedings of the 25th International Conference on Automated Deduction (CADE), volume 9195, pages 591–606, 2015. doi:10.1007/978-3-319-21401-6_40.

[bib.bib17] [17] Marijn J. H. Heule and Armin Biere. What a difference a variable makes. In Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS), volume 10806, pages 75–92, 2018. doi:10.1007/978-3-319-89963-3_5.

[bib.bib18] [18] Marijn J. H. Heule, Benjamin Kiesl, and Armin Biere. Short proofs without new variables. In Proceedings of the 26th International Conference on Automated Deduction (CADE), volume 10395, pages 130–147, 2017. doi:10.1007/978-3-319-63046-5_9.

[bib.bib19] [19] Marijn J. H. Heule, Benjamin Kiesl, and Armin Biere. Strong extension-free proof systems. Journal of Automated Reasoning, 64(3):533–554, 2019. Extended version of [18]. doi:10.1007/s10817-019-09516-0.

[bib.bib20] [20] Marijn J. H. Heule, Benjamin Kiesl, Martina Seidl, and Armin Biere. Pruning through satisfaction. In Proceedings of the Hardware and Software: Verification and Testing - 13th International Haifa Verification Conference (HVC), volume 10629, pages 179–194, 2017. doi:10.1007/978-3-319-70389-3_12.

[bib.bib21] [21] Hannes Ihalainen, Jeremias Berg, and Matti Järvisalo. Clause redundancy and preprocessing in maximum satisfiability. In Proceedings of the 11th International Joint Conference on Automated Reasoning (IJCAR), volume 13385, pages 75–94, 2022. doi:10.1007/978-3-031-10769-6_6.

[bib.bib22] [22] Matti Järvisalo, Marijn Heule, and Armin Biere. Inprocessing rules. In Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR), volume 7364, pages 355–370, 2012. doi:10.1007/978-3-642-31365-3_28.

[bib.bib23] [23] Benjamin Kiesl, Adrián Rebola-Pardo, and Marijn J. H. Heule. Extended resolution simulates DRAT. In Proceedings of the 9th International Joint Conference on Automated Reasoning (IJCAR), Held as Part of the Federated Logic Conference, FloC 2018, volume 10900, pages 516–531, 2018. doi:10.1007/978-3-319-94205-6_34.

[bib.bib24] [24] Leszek Aleksander Kołodziejczyk and Neil Thapen. The Strength of the Dominance Rule. In Proceedings of the 27th International Conference on Theory and Applications of Satisfiability Testing (SAT), volume 305, pages 20:1–20:22, 2024. doi:10.4230/LIPIcs.SAT.2024.20.

[bib.bib25] [25] Oliver Kullmann. On a generalization of extended resolution. Discrete Applied Mathematics, 96-97:149–176, 1999. doi:10.1016/S0166-218X(99)00037-2.

[bib.bib26] [26] Javier Larrosa and Federico Heras. Resolution in max-sat and its relation to local consistency in weighted csps. In Proceedings of the 19h International Joint Conference on Artificial Intelligence (IJCAI), pages 193–198, 2005. URL: http://ijcai.org/Proceedings/05/Papers/0360.pdf.

[bib.bib27] [27] António Morgado, Carmine Dodaro, and João Marques-Silva. Core-guided MaxSAT with soft cardinality constraints. In Proceedings of the 20th International Conference on Principles and Practice of Constraint Programming (CP), pages 564–573, 2014. doi:10.1007/978-3-319-10428-7_41.

[bib.bib28] [28] António Morgado, Federico Heras, Mark H. Liffiton, Jordi Planes, and João Marques-Silva. Iterative and core-guided MaxSAT solving: A survey and assessment. Constraints An Int. J., 18(4):478–534, 2013. doi:10.1007/S10601-013-9146-2.

[bib.bib29] [29] Nina Narodytska and Fahiem Bacchus. Maximum satisfiability using core-guided MaxSAT resolution. In Proceedings of the 28th Conference on Artificial Intelligence (AAAI), pages 2717–2723, 2014. doi:10.1609/AAAI.V28I1.9124.

[bib.bib30] [30] Adrián Rebola-Pardo and Martin Suda. A theory of satisfiability-preserving proofs in SAT solving. In Proceedings of the 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), volume 57, pages 583–603, 2018. doi:10.29007/TC7Q.

[bib.bib31] [31] Paul Saikko, Jeremias Berg, and Matti Järvisalo. LMHS: a SAT-IP hybrid MaxSAT solver. In Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing (SAT), pages 539–546, 2016. doi:10.1007/978-3-319-40970-2_34.

Redundancy Rules for MaxSAT

Abstract

Keywords and phrases:

Funding:

Copyright and License:

2012 ACM Subject Classification:

Acknowledgements:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

Structure of the paper

2 Preliminaries

Propositional logic notation

Substitutions and assignments

Unit propagation

Observation 2.1 ([9, Fact 1.3]).

Resolution

MaxSAT

MaxSAT with blocking variables

Definition 2.2.

Observation 2.3.

3 Redundancy rules for MaxSAT

Definition 3.1 (redundant clause, [21]).

Definition 3.2.

▶ Remark 3.3.

Lemma 3.4.

Proof.

Lemma 3.5.

Proof (sketch).

Definition 3.6 (cost⁢-⁢SR calculus).

3.1 Simulation by veriPB

Proposition 3.7.

4 Soundness and completeness

Lemma 4.1.

Proof.

Theorem 4.2 (soundness of cost⁢-⁢SR).

Proof.

Theorem 4.3 (completeness of cost⁢-⁢SPR).

Proof.

5 Incompleteness and Width Lower bounds

Theorem 5.1.

Proof.

Corollary 5.2.

Corollary 5.3.

Proof.

Corollary 5.4.

Proof.

6 Short proofs using redundancy rules

▶ Remark 6.1.

6.1 Short proofs of minimally unsatisfiable formulas

Theorem 6.2.

Proof.

6.2 Short proofs of the minimum cost of 𝗣𝗛𝗣𝒏𝒎

Theorem 6.3.

Lemma 6.4.

Proof.

Lemma 6.5.

Proof.

Proof of Theorem 6.3.

Preprocessing 1.

Preprocessing 2.

Step 0.

Step 1.

Step 2.

Step 3.

Step 4.

Step 5.

7 Conclusions and open problems

References

$\blacktriangleright$ Remark 3.3.

Definition 3.6 ( $\mathrm{cost\text{-}SR}$ calculus).

Theorem 4.2 (soundness of $\mathrm{cost\text{-}SR}$ ).

Theorem 4.3 (completeness of $\mathrm{cost\text{-}SPR}$ ).

$\blacktriangleright$ Remark 6.1.

6.2 Short proofs of the minimum cost of $\mathsf{PHP}^{m}_{n}$