On Tackling the Limits of Resolution in SAT Solving

TL;DR

This paper introduces a new transformation that enables solving hard SAT problems more efficiently using MaxSAT solvers, surpassing traditional CDCL SAT solver limitations.

Contribution

It proposes a novel problem transformation reducing CNF SAT decision to MaxSAT over Horn formulas, with polynomial bounds and practical efficiency demonstrated.

Findings

Polynomial bounds on MaxSAT resolution steps for pigeonhole formulas.

Modern MaxSAT solvers efficiently solve CNF formulas hard for CDCL.

Experimental validation shows improved performance on hard SAT instances.

Abstract

The practical success of Boolean Satisfiability (SAT) solvers stems from the CDCL (Conflict-Driven Clause Learning) approach to SAT solving. However, from a propositional proof complexity perspective, CDCL is no more powerful than the resolution proof system, for which many hard examples exist. This paper proposes a new problem transformation, which enables reducing the decision problem for formulas in conjunctive normal form (CNF) to the problem of solving maximum satisfiability over Horn formulas. Given the new transformation, the paper proves a polynomial bound on the number of MaxSAT resolution steps for pigeonhole formulas. This result is in clear contrast with earlier results on the length of proofs of MaxSAT resolution for pigeonhole formulas. The paper also establishes the same polynomial bound in the case of modern core-guided MaxSAT solvers. Experimental results, obtained on CNF formulas known to be hard for CDCL SAT solvers, show that these can be efficiently solved with modern MaxSAT solvers.

Tables

Table 1. Table 1 : Example MaxSAT-resolution steps.

Clause 1	Clause 2	Derived Clauses
$(x\vee A,u)$	$(\neg x\vee B,w)$	$(A\vee B,m)$, $(x\vee A,u\ominus m)$, $(\neg x\vee B,w\ominus m)$,
$(x\vee A\vee \neg B,m)$, $(\neg x\vee \neg A\vee B,m)$
$(x\vee A,1)$	$(\neg x,\top )$	$(A,1)$, $(\neg x,\top )$, $(\neg x\vee \neg A,1)$

Table 2. Table 3 : Analysis of ℳ j subscript ℳ 𝑗 {\mathcal{M}}_{j} , iteration k 𝑘 k .

Clauses	Unit Propagation
$\left(p_{k+1j}\right)$	$p_{k+1j}=1$
$\left(\neg p_{1j}\vee \neg p_{k+1j}\right),\dots ,\left(\neg p_{kj}\vee \neg p_{k+1j}\right)$	$p_{1j}=\dots =p_{kj}=0$
$\left(r_{1j}\vee p_{1j}\right),\dots ,\left(r_{kj}\vee p_{kj}\right)$	$r_{1j}=\dots =r_{kj}=1$
${\sum }_{l=1}^k{r}_{lj}\le k-1$	$\left({\sum }_{l=1}^k{r}_{lj}\le k-1\right){⊢}_1\perp$

Table 3. Table 5 : Families of solvers considered in the evaluation (their best performing representatives are written in italics ). SAT+ stands for SAT strengthened with other techniques, IHS MaxSAT is for implicit hitting set based MaxSAT, CG MaxSAT is for core-guided MaxSAT, MRes is for MaxSAT resolution, MIP is for mixed integer programming, OPB is for pseudo-Boolean optimization, BDD is for binary decision diagrams.

SAT		SAT+		IHS MaxSAT		CG MaxSAT			MRes	MIP	OPB		BDD
minisat	glucose	lgl	crypto	maxhs	lmhs	mscg	wbo	wpm3	eva	lp	cc	sat4j	zres
[33]	[8]	[14, 15]	[67, 66]	[29, 30, 31]	[63]	[55]	[51]	[3]	[56]	[41]	[35]	[12]	[22]

Equations

$$\underset{i=1}{\overset{m+1}{\bigwedge }}\text{AtLeast}1(x_{i1},\dots ,x_{im})\wedge \underset{j=1}{\overset{m}{\bigwedge }}\text{AtMost}1(x_{1j},\dots ,x_{m+1,j})$$

$$(x_1\vee \neg x_2\vee x_3)\wedge (x_2\vee x_3)\wedge (\neg x_1\vee \neg x_3)$$

$$(\neg n_1\vee \neg p_1)\wedge (\neg n_2\vee \neg p_2)\wedge (\neg n_3\vee \neg p_3)$$

$$(\neg n_1\vee \neg p_2\vee \neg n_3)\wedge (\neg n_2\vee \neg n_3)\wedge (\neg p_1\vee \neg p_3)$$

$$\begin{array}{rl}\{& (n_{11}),\dots ,(n_{1m}),\dots ,(n_{m+11}),\dots ,(n_{m+1m}),\\ & (p_{11}),\dots ,(p_{1m}),\dots ,(p_{m+11}),\dots ,(p_{m+1m})\}\end{array}$$

$$\text{HEnc}\left({\text{PHP}}_m^{m+1}\right)\triangleq ⟨\mathcal{H},\mathcal{S}⟩=⟨{\wedge }_{i=1}^{m+1}{\mathcal{L}}_i\wedge {\wedge }_{j=1}^m{\mathcal{M}}_j\wedge \mathcal{P},\mathcal{S}⟩$$

Full text

1 Introduction

Boolean Satisfiability (SAT) solvers have made remarkable progress over the last two decades. Unable to solve formulas with more than a few hundred variables in the early 90s, SAT solvers are now capable of routinely solving formulas with a few million variables [17, 13]. The success of SAT solvers is supported by the CDCL (Conflict-Driven Clause Learning) [17, Chapter 04] paradigm, and the ability of SAT solvers to learn clauses from induced conflicts [17]. Nevertheless, being no more powerful than the general resolution proof system [59], CDCL SAT solvers are also known not to scale for specific formulas, which are hard for resolution [39, 68, 23]. Recent work has considered different forms of extending CDCL with techniques adapted from more powerful proof systems as well as others [22, 67, 40, 7, 12, 16], with success in some settings. Nevertheless, for pigeonhole formulas [27], and with the exception of the lingeling SAT solver [14] on specific encodings, modern CDCL SAT solvers are unable to prove unsatisfiability even for a fairly small numbers of pigeons.

This paper proposes an alternative path to tackle the difficulties of the resolution proof system, by developing an approach that aims to complement existing SAT solvers, and which also builds upon efficient CDCL SAT solvers. The motivation is to transform the original problem, from one clausal form to another, the latter enconding a restricted maximum satisfiability problem, but in such a way that CDCL SAT solvers can still be exploited.

Given any CNF formula ${\mathcal{F}}$, the paper shows how to encode the problem as Horn Maximum Satisfiability (HornMaxSAT), more concretely by requiring a given cost on the HornMaxSAT formulation. This enables solving the modified problem with either a MaxSAT solver or with a dedicated HornMaxSAT solver. The basic encoding is also shown to be subject to a number of optimizations, that can effectively reduce the number of variables. The paper then shows that for propositional encodings of the pigeonhole principle [27], transformed to HornMaxSAT, there exists a polynomially time bounded sequence of MaxSAT resolution steps which enables deriving a number of falsified clauses that suffices for proving unsatisfiable the original PHP formula. Similarly, the paper also proves that for modern core-guided MaxSAT solvers there exist sequences of unsatisfiable cores that enable reaching the same conclusion in polynomial time. This in turn suggests that MaxSAT algorithms [54] can be effective in practice when applied to such instances.

Experimental results, obtained on different encodings of the pigeonhole principle, but also on other instances that are well-known to be hard for resolution [68], confirm the theoretical result. Furthermore, a recently-proposed family of MaxSAT solvers [29, 63], based on iterative computation of minimum hitting sets, is also shown to be effective in practice and on a wider range of classes of instances.

The paper is organized as follows. section 2 introduces the definitions and notation used throughout the paper. section 3 develops a simple encoding from SAT into HornMaxSAT. section 4 derives a polynomial bound on the number and size of MaxSAT-resolution steps to establish the unsatisfiability of propositional formulas encoding the pigeonhole principle transformed into HornMaxSAT. The section also shows that there are executions of core-guided MaxSAT solvers that take polynomial time to establish a lower bound of the cost of the MaxSAT solution which establishes the unsatisfiability of the original CNF formula. Experimental results on formulas encoding the pigeonhole principle, but also on other formulas known to be hard for CDCL SAT solvers [68] are analyzed in subsection 5.2. The paper concludes in section 6.

2 Preliminaries

The paper assumes definitions and notation standard in propositional satisfiability (SAT) and maximum satisfiability (MaxSAT) [17]. Propositional variables are taken from a set $X=\{x_{1},x_{2},\ldots\}$. A Conjunctive Normal Form (CNF) formula is defined as a conjunction of disjunctions of literals, where a literal is a variable or its complement. CNF formulas can also be viewed as sets of sets of literals, and are represented with calligraphic letters, ${\mathcal{A}}$, ${\mathcal{F}}$, ${\mathcal{H}}$, etc. A truth assignment is a map from variables to $\{0,1\}$. Given a truth assignment, a clause is satisfied if at least one of its literals is assigned value 1; otherwise it is falsified. A formula is satisfied if all of its clauses are satisfied; otherwise it is falsified. If there exists no assignment that satisfies a CNF formula ${\mathcal{F}}$, then ${\mathcal{F}}$ is referred to as unsatisfiable. (Boolean) Satisfiability (SAT) is the decision problem for propositional formulas, i.e. to decide whether a given propositional formula is satisfiable. Since the paper only considers propositional formulas in CNF, throughout the paper SAT refers to the decision problem for propositional formulas in CNF.

To simplify modeling with propositional logic, one often represents more expressive constraints. Concrete examples are cardinality constraints and pseudo-Boolean constraints [17]. A cardinality constraint of the form $\sum x_{i}\leq k$ is referred to as an $\textsf{AtMost}{}k$ constraint, whereas a cardinality constraint of the form $\sum x_{i}\geq k$ is referred to as an $\textsf{AtLeast}{}k$ constraint. The study of propositional encodings of cardinality and pseudo-Boolean constraints is an area of active research [69, 9, 65, 34, 17, 4, 25, 10, 5, 1, 58].

A clause is Horn if it contains at most one positive literal. A Horn clause is a goal clause if it has no positive literals; otherwise it is a definite clause. The decision problem for Horn formulas is well-known to be in P, with linear time algorithms since the 80s [32, 52]. A number of function problems defined on Horn formulas can be solved in polynomial time [48]. These include computing the lean kernel, finding a minimal unsatisfiable subformula and finding a maximal satisfiable subformula.

2.1 Propositional Encodings of the Pigeonhole Principle

The propositional encoding of the pigeonhole hole principle is well-known [27].

Definition 1** (Pigeonhole Principle, PHP [27]).**

The pigeonhole principle states that if $m+1$ pigeons are distributed by $m$ holes, then at least one hole contains more than one pigeon. A more formal formulation is that there exists no injective function mapping from $\{1,2,...,m+1\}$ to $\{1,2,...,m\}$, for $m\geq 1$.

Propositional formulations of PHP encode the negation of the principle, and ask for an assignment such that the $m+1$ pigeons are placed into $m$ holes. The propositional encoding of the $\text{PHP}^{m+1}_{m}$ problem can be derived as follows. Let the variables be $x_{ij}$, with $1\leq i\leq m+1,1\leq j\leq m$, with $x_{ij}=1$ iff the $i^{\text{th}}$ pigeon is placed in the $j^{\text{th}}$ hole. The constraints are that each pigeon must be placed in at least one hole, and each hole must not have more than one pigeon.

[TABLE]

An $\textsf{AtLeast}1$ constraint can be encoded with a single clause. For the $\textsf{AtMost}1$ constraint there are different encodings, including [17, 65, 34]. For example, the pairwise encoding [17] of $\textsf{AtMost}1(x_{1j},\ldots,x_{m+1,j})$ uses no auxiliary variables and the clauses $\land_{r=2}^{m+1}\land_{s=1}^{r-1}(\neg x_{rj}\lor\neg x_{sj})$. It is well-known that resolution has an exponential lower bound for PHP [39, 11, 61].

2.2 MaxSAT, MaxSAT Resolution & MaxSAT Algorithms

MaxSAT.

For unsatisfiable formulas, the maximum satisfiability (MaxSAT) problem is to find an assignment that maximizes the number of satisfied clauses (given that not all clauses can be satisfied). There are different variants of the MaxSAT problem [17, Chapter 19]. Partial MaxSAT allows for hard clauses (which must be satisfied) and soft clauses (which represent a preference to satisfy those clauses). There are also weighted variants, in which soft clauses are given a weight, and for which hard clauses (if any) have a weight of $\top$ (meaning clauses that must be satisfied). The notation $(c,w)$ will be used to represent a clause $c$ with $w$ denoting the cost of falsifying $c$. The paper considers partial MaxSAT instances, with hard clauses, for which $w=\top$, and soft clauses, for which $w=1$. The notation $\langle{\mathcal{H}},{\mathcal{S}}\rangle$ is used to denote partial MaxSAT problems with sets of hard (${\mathcal{H}}$) and soft (${\mathcal{S}}$) clauses. Throughout the paper, a MaxSAT solution represents either a maximum cardinality set of satisfied soft clauses or an assignment that satisfies all hard clauses and also maximizes (or minimizes, resp.) the number of satisfied (or falsified, resp.) soft clauses.

MaxSAT Resolution [18, 46].

In contrast with SAT, the MaxSAT resolution operation requires the introduction of additional clauses other than the resolvent, and resolved clauses cannot be resolved again. Let $(x\lor A,u)$ and $(\neg x\lor B,w)$ be two clauses, and let $m\triangleq\min(u,w)$, $u\ominus w\triangleq(u\;\text{==}\,\top)\,\text{?}\,\top:u-w$, with $u\geq w$. The (non-clausal) MaxSAT resolution step [46] is shown in Table 1. (We could have used the clausal formulation [18], but it is more verbose and unnecessary for the purposes of the paper. It suffices to mention that clausal MaxSAT resolution adds at most $2n$ clauses at each resolution step, where the number of variables is $n$ and the number of literals in each clause does not exceed $n$.)

It is well-known that MaxSAT-resolution is unlikely to improve propositional resolution [18]. For the original $\text{PHP}^{m+1}_{m}$ formulas, there are known exponential lower bounds on the size of deriving one empty clause by MaxSAT-resolution (given that the remaining clauses are satisfiable) [18, Corollary 18].

MaxSAT Algorithms.

Many algorithms for MaxSAT have been proposed over the years [17, Chapter 19]. The most widely investigated can be broadly organized into branch and bound [17, Chapter 19], iterative-search [36, 12, 45], core-guided [36, 49, 54, 2, 56, 53, 50], and minimum hitting sets [29, 63]. In most proposed algorithms, core-guided and minimum hitting sets MaxSAT algorithms iteratively determine formulas to be unsatisfiable, until satisfiability is reached for a formula that relaxes clauses of minimum cost. This paper analyzes the operation of core-guided MaxSAT algorithms, concretely the MSU3 algorithm [49] 111Different implementations of the MSU3 have been proposed over the years [49, 54, 2, 50], which often integrate different improvements. A well-known implementation of MSU3 is OpenWBO [50], one of the best MaxSAT solvers in the MaxSAT Evaluations since 2014.. Moreover, and to our best knowledge, the relationship between core-guided MaxSAT algorithms and MaxSAT resolution was first investigated in [56].

2.3 Related Work

The complexity of resolution on pigeonhole formulas has been studied by different authors, e.g. see [27, 39, 11, 61, 57] and references therein, among others. It is well-known that for other proof systems, including cutting planes and extended resolution, PHP has polynomial proofs [26, 20, 28, 21, 6, 64]. Different authors have looked into extending CDCL (and so resolution) with the goal of solving formulas for which resolution has known exponential lower bounds [37, 38, 67, 40, 7, 12, 13, 43, 44, 16]. Some SAT solvers apply pattern matching techniques [14], but these are only effective for specific propositional encodings. Furthermore, there has been limited success in applying cutting planes and extended resolution in practical SAT solvers.

3 Reducing SAT to HornMaxSAT

The propositional satisfiability problem for CNF formulas can be reduced to HornMaxSAT, more concretely to the problem of deciding whether for some target Horn formula there exists an assignment that satisfies a given number of soft clauses.

Let ${\mathcal{F}}$ be a CNF formula, with $N$ variables $\{x_{1}\ldots,x_{N}\}$ and $M$ clauses $\{c_{1},\ldots,c_{M}\}$. Given ${\mathcal{F}}$, the reduction creates a Horn MaxSAT problem with hard clauses ${\mathcal{H}}$ and soft clauses ${\mathcal{S}}$, $\langle{\mathcal{H}},{\mathcal{S}}\rangle=\textsf{HEnc}({\mathcal{F}})$. For each variable $x_{i}\in X$, create new variables $p_{i}$ and $n_{i}$, where $p_{i}=1$ iff $x_{i}=1$, and $n_{i}=1$ iff $x_{i}=0$. Thus, we need a hard clause $(\neg p_{i}\lor\neg n_{i})$, to ensure that we do not simultaneously assign $x_{i}=1$ and $x_{i}=0$. (Observe that the added clause is Horn.) This set of hard Horn clauses is referred to as ${\mathcal{P}}$. For each clause $c_{j}$, we require $c_{j}$ to be satisfied, by requiring that one of its literals not to be falsified. For each literal $x_{i}$ use $\neg n_{i}$, and for each literal $\neg x_{i}$ use $\neg p_{i}$. Thus, $c_{j}$ is encoded with a new (hard) clause $c^{\prime}_{j}$ with the same number of literals as $c_{j}$, but with only negative literals on the $p_{i}$ and $n_{i}$ variables, and so the resulting clause is also Horn. The set of soft clauses ${\mathcal{S}}$ is given by $(p_{i})$ and $(n_{i})$ for each of the original variables $x_{i}$. If the resulting Horn formula has a HornMaxSAT solution with at least $N$ variables assigned value 1, then the original formula is satisfiable; otherwise the original formula is unsatisfiable. (Observe that, by construction, the HornMaxSAT solution cannot assign value 1 to more than $N$ variables. Thus, unsatisfiability implies being unable to satisfy more than $N-1$ soft clauses.) Clearly, the encoding outlined in this section can be the subject of different improvements, e.g. not all clauses need to be goal clauses. (An approach to tighten the encoding is detailed later in this section.)

Example 1*.*

Let the CNF formula be:

[TABLE]

The new variables are $\{n_{1},p_{1},n_{2},p_{2},n_{3},p_{3}\}$. Preventing simultaneous assignment to 0 and 1 is guaranteed with the hard clauses:

[TABLE]

The original clauses are reencoded as hard clauses as follows:

[TABLE]

Finally, the soft clauses are ${\mathcal{S}}=\{(n_{1}),(p_{1}),(n_{2}),(p_{2}),(n_{3}),(p_{3})\}$.

The transformation proposed above can be related with the well-known dual-rail encoding, used in different settings [19, 47, 62, 42, 60]. To our best knowledge, the use of a dual-rail encoding for deriving a pure Horn formula has not been proposed in earlier work.

Lemma 1**.**

Given $\langle{\mathcal{H}},{\mathcal{S}}\rangle=\textsf{HEnc}({\mathcal{F}})$, there can be no more than $N$ satisfied soft clauses.

• Proof.

By construction of $\langle{\mathcal{H}},{\mathcal{S}}\rangle$, for any $x_{i}$, there is no assignment that satisfies ${\mathcal{H}}$ with $n_{i}=1$ and $p_{i}=1$. ∎

Lemma 2**.**

Let ${\mathcal{F}}$ have a satisfying assignment $\nu$. Then, there exists an assignment that satisfies ${\mathcal{H}}$ and $N$ soft clauses in $\langle{\mathcal{H}},{\mathcal{S}}\rangle=\textsf{HEnc}({\mathcal{F}})$.

• Proof.

Given $\nu$, we create an assignment $\nu^{\prime}$ to the $n_{i}$ and $p_{i}$ variables that satisfies the clauses in ${\mathcal{H}}$, and $N$ clauses in ${\mathcal{S}}$. For each $x_{i}$, if $\nu(x_{i})=1$, then set $p_{i}=1$; otherwise set $n_{i}=1$. Thus, there will be $N$ satisfied clauses in ${\mathcal{S}}$. For each clause $c_{j}\in{\mathcal{F}}$, pick a literal $l_{k}$ assigned value

1. If $l_{k}=x_{k}$, then $c^{\prime}_{k}$ contains literal $\neg n_{k}$, and so it is satisfied. If $l_{k}=\neg x_{k}$, then $c^{\prime}_{k}$ contains literal $\neg p_{k}$, and so it is satisfied. Thus every clause in ${\mathcal{H}}$ is satisfied, and $N$ soft clauses are satisfied. ∎

Lemma 3**.**

Let $\nu^{\prime}$ be an assignment that satisfies the clauses in ${\mathcal{H}}$ and $N$ clauses in ${\mathcal{S}}$. Then there exists an assignment $\nu$ that satisfies ${\mathcal{F}}$.

• Proof.

By construction of $\langle{\mathcal{H}},{\mathcal{S}}\rangle$, for each $x_{i}$, either $n_{i}$ is assigned value 1, or $p_{i}$ is assigned value 1, but not both. Let $\nu(x_{i})=1$ if $\nu^{\prime}(p_{i})=1$ and $\nu(x_{i})=0$ if $\nu^{\prime}(n_{i})=1$. All variables $x_{i}$ are either assigned value 0 or 1. For clause $c^{\prime}_{j}$, let $l_{k}$ be a literal assigned value 1. If $l_{k}=\neg n_{k}$, then $x_{k}$ is a literal in $c_{j}$ and since $\nu(x_{i})=1$, then the clause $c_{j}$ is satisfied. Otherwise, if $l_{k}=\neg p_{k}$, then $\neg x_{k}$ is a literal in $c_{j}$ and since $\nu(x_{i})=0$, then the clause $c_{j}$ is satisfied. ∎

1, 2 and 3 yield the following.

Theorem 1**.**

${\mathcal{F}}$* is satisfiable if and only if there exists an assignment that satisfies ${\mathcal{H}}$ and $N$ clauses in ${\mathcal{S}}$.*

The reduction of SAT into HornMaxSAT can also be applied to the $\text{PHP}^{m+1}_{m}$ problem.

Example 2* (Pigeonhole Principle).*

With each variable $x_{ij}$, $1\leq i\leq m+1,1\leq j\leq m$, we associate two new variables: $n_{ij}$ and $p_{ij}$. The set of clauses ${\mathcal{P}}$ prevents a variable $x_{i}$ from being assigned value 0 and 1 simultaneously: ${\mathcal{P}}=\{(\neg n_{ij}\lor\neg p_{ij})\,|\,1\leq i\leq m+1,1\leq j\leq m\}$. ${\mathcal{L}}_{i}$ represents the encoding of each $\textsf{AtLeast}1$ constraint, concretely ${\mathcal{L}}_{i}=(\neg n_{i1}\lor\ldots\lor\neg n_{im})$. ${\mathcal{M}}_{j}$ represents the encoding of each $\textsf{AtMost}1$ constraint, which will depend on the encoding used. The soft clauses ${\mathcal{S}}$ are given by,

[TABLE]

with $|{\mathcal{S}}|=2m(m+1)$. Thus, the complete reduction of PHP into MaxSAT becomes:

[TABLE]

Clearly, given ${\mathcal{P}}$, one cannot satisfy more the $m(m+1)$ soft clauses. By 1, $\text{PHP}^{m+1}_{m}$ is satisfiable if and only if there exists an assignment that satisfies the hard clauses ${\mathcal{H}}$ and $m(m+1)$ soft clauses from ${\mathcal{S}}$.

Reducing the number of variables.

As hinted earlier in this section, one can devise encodings that use fewer variables, while producing a Horn MaxSAT formula. Given ${\mathcal{F}}$, let ${\mathcal{N}}\subseteq{\mathcal{F}}$ denote the set of non-Horn clauses. For each clause $c_{j}\in{\mathcal{N}}$, let $C_{j}$ represent the set of positive literals of $c_{j}$, and let $x_{i}\in C_{j}$. Moreover, let $W=\cup_{j}C_{j}$, i.e. the set of variables causing the clauses in ${\mathcal{N}}$ not to be Horn. Finally, let $r_{i}=1$ if and only if for clause $c_{j}$ variable $x_{i}$ is not dual-rail encoded. Clearly, for $c_{j}$ we must have $\sum_{x_{i}\in C_{j}}r_{i}\leq 1$, i.e. the number of positive literals that remain cannot exceed 1; otherwise the resulting clause would not be Horn. Moreover, we would like to discard as many variables as possible, and so we add a soft clause $(r_{i})$ for each $x_{i}\in W$. This corresponds to finding a maximum independent set, which we can approximate heuristically.

4 Short MaxSAT Proofs for PHP

This section shows that the reduction of $\text{PHP}^{m+1}_{m}$ to HornMaxSAT based on a dual-rail encoding enables both existing core-guided MaxSAT algorithms and also MaxSAT resolution, to prove in polynomial time that the original problem formulation222This section studies the original pairwise encoding of $\text{PHP}^{m+1}_{m}$. However, a similar argument can be applied to $\text{PHP}^{m+1}_{m}$ provided any encoding of AtMost1 constraints ${\mathcal{M}}_{j}$, as confirmed by the experimental results in subsection 5.2. is unsatisfiable. Recall from 1, that $\text{PHP}^{m+1}_{m}$ is satisfiable if and only if, given (5), there exists an assignment that satisfies ${\mathcal{H}}$ and $m(m+1)$ soft clauses in ${\mathcal{S}}$. This section shows that for both core-guided algorithms and for MaxSAT resolution, we can conclude in polynomial time that satisfying ${\mathcal{H}}$ requires falsifying at least $m(m+1)+1$ soft clauses, thus proving $\text{PHP}^{m+1}_{m}$ to be unsatisfiable.

The results in this section should be contrasted with earlier work [18], which proves that MaxSAT resolution requires an exponentially large proof to produce an empty clause, this assuming the original propositional encoding for $\text{PHP}^{m+1}_{m}$.

4.1 A Polynomial Bound on Core-Guided MaxSAT Algorithms

This section shows that a core-guided MaxSAT algorithm will conclude in polynomial time that more than $m(m+1)$ clauses must be falsified, when the hard clauses are satisfied, thus proving the original $\text{PHP}^{m+1}_{m}$ to be unsatisfiable. The analysis assumes the operation of basic core-guided algorithm, MSU3 [49], but similar analyses could be carried out for other families of core-guided algorithms333Basic knowledge of core-guided MaxSAT algorithms is assumed. The reader is referred to recent surveys for more information [54, 2]..

The following observations about (5) are essential to prove the bound on the run time. First, the clauses in the ${\mathcal{L}}_{i}$ constraints do not share variables in common with the clauses in the ${\mathcal{M}}_{j}$ constraints. Second, each constraint ${\mathcal{L}}_{i}$ is of the form $(\neg n_{i1}\lor\ldots\lor\neg n_{im})$ and so its variables are disjoint from any other ${\mathcal{L}}_{k}$, $k\not=i$. Third, assuming a pairwise encoding, each constraint ${\mathcal{M}}_{j}$ is of the form $\land_{r=2}^{m+1}\land_{s=1}^{r-1}(\neg p_{rj}\lor\neg p_{sj})$, and so its variables are disjoint from any other ${\mathcal{M}}_{l}$, $l\not=j$. Since the sets of variables for each constraint are disjoint from the other sets of variables, we can exploit this partition of the clauses, and run a MaxSAT solver separately on each one. (Alternatively, we could assume the MSU3 MaxSAT algorithm to work with disjoint unsatisfiable cores.)

Table 2 summarizes the sequence of unit propagation steps that yields a lower bound on the number of falsified clauses larger than $m(m+1)$.

For each ${\mathcal{L}}_{i}$, the operation is summarized in the second row of Table 2. Unit propagation yields a conflict between $m$ soft clauses and the corresponding hard clause. This means that at least one of these soft clauses must be falsified. Since there are $m+1$ constraints ${\mathcal{L}}_{i}$, defined on disjoint sets of variables, then each will contribute at least one falsified soft clause, which puts the lower bound on the number of falsified clauses at $m+1$.

For each ${\mathcal{M}}_{j}$ the operation is summarized in rows 3 to last of Table 2. Each row indicates a sequence of unit propagation steps that produces a conflict, each on a distinct set of soft clauses. Observe that each soft clause $(p_{kj})$, $k\geq 2$, induces a sequence of unit propagation steps, that causes the AtMost$\{k-1\}$ constraint to become inconsistent. Concretely, for iteration $k$ (where row 3 corresponds to iteration 1), the sequence of unit propagation steps is summarized in Table 3 444The notation $\Phi\operatorname*{\vdash_{\scriptsize{1}}}\bot$ indicates that inconsistency (i.e. a falsified clause) is derived by unit propagation on the propositional encoding of $\Phi$. This is the case with existing encodings of AtMost$k$ constraints. .

Since there are $m$ such rows, then each ${\mathcal{M}}_{j}$ contributes at least $m$ falsified soft clauses. Moreover, the number of ${\mathcal{M}}_{j}$ constraints is $m$, and so the ${\mathcal{M}}_{j}$ constraints increase the bound by $m\cdot m$.

Given the above, in total we are guaranteed to falsify at least $m+1+m\cdot m=m(m+1)+1$ clauses, thus proving that one cannot satisfy $m(m+1)$ soft clauses if the hard clauses are satisfied. In turn, this proves that the $\text{PHP}^{m+1}_{m}$ problem is unsatisfiable.

We can also measure the run time of the sequence of unit propagation steps. For each ${\mathcal{L}}_{i}$, the run time is ${\mathcal{O}}(m)$, and there will be $m$ such unit propagation steps, for a total ${\mathcal{O}}(m^{2})$. For each ${\mathcal{M}}_{j}$ there will be $m$ unit propagation steps, with run time between ${\mathcal{O}}(1)$ and ${\mathcal{O}}(m)$. Thus, the run time of the sequence of unit propagation steps for each ${\mathcal{M}}_{j}$ is ${\mathcal{O}}(m^{2})$. Since there are $m$ constraints ${\mathcal{M}}_{j}$, then the total run time is ${\mathcal{O}}(m^{3})$.

Proposition 1**.**

Given (5), and for a core-guided MSU3-like MaxSAT solver, there is a sequence of unit propagation steps such that a lower bound of $m(m+1)+1$ is computed in ${\mathcal{O}}(m^{3})$ time.

• Proof.

(Sketch) The discussion above. ∎

Moreover, it is important to observe that the unit propagation steps considered in the analysis above avoid the clauses in ${\mathcal{P}}$, i.e. only the clauses in ${\mathcal{L}}_{i}$, ${\mathcal{M}}_{j}$, ${\mathcal{S}}$, and relaxed clauses, are used for deriving the lower bound of $m(m+1)+1$ on the minimum number of falsified soft clauses. As shown in subsection 5.2, and for the concrete case of PHP, the clauses in ${\mathcal{P}}$ are unnecessary and actually impact negatively the performance of core-guided MaxSAT solvers. Finally, and although the proof above assumes an MSU3-like core-guided algorithm, similar ideas could be considered in the case of other variants of core-guided MaxSAT algorithms [36, 54, 2, 56].

4.2 A Polynomial Bound on MaxSAT Resolution

We can now exploit the intuition from the previous section to identify the sequence of MaxSAT resolution steps that enable deriving $m(m+1)+1$ empty clauses, thereby proving that any assignment that satisfies the hard clauses must falsify at least $m(m+1)+1$ soft clauses, and therefore proving that the propositional encoding of PHP is unsatisfiable. As before, we assume that the pairwise encoding is used to encode each constraint ${\mathcal{M}}_{j}$. As indicated earlier in subsection 2.2, we consider a simplified version of MaxSAT resolution [46], which is non-clausal. As explained below, this is not problematic, as just a few clauses are of interest. For the clausal version of MaxSAT resolution, the other clauses, which our analysis ignores, are guaranteed to be linear in the number of variables at each step, and will not be considered again.

Table 4 summarizes the essential aspects of the MaxSAT resolution steps used to derive $m(m+1)+1$ empty clauses. (Also, subsection 4.1 clarifies that the formula can be partitioned if ${\mathcal{P}}$ is ignored.) Similarly to the previous section, the ${\mathcal{L}}_{i}$ constraints serve to derive $m+1$ empty clauses, whereas each ${\mathcal{M}}_{j}$ constraint serves to derive $m$ empty clauses. In total, we derive $m(m+1)+1$ empty clauses, getting the intended result.

As shown in Table 4, for each constraint ${\mathcal{L}}_{i}$, start by applying MaxSAT resolution between the hard clause ${\mathcal{L}}_{i}\triangleq(\neg n_{i1}\lor\ldots\lor\neg n_{im})$ and soft clause $(n_{i1})$ to get soft clause $(\neg n_{i2}\lor\ldots\lor\neg n_{im})$, and a few other clauses (which are irrelevant for our purposes). Next, apply $m-1$ additional MaxSAT resolution steps, resolving soft clause $(\neg n_{ik}\lor\ldots\lor\neg n_{im})$ with soft clause $(n_{ik})$ to get soft clause $(\neg n_{ik+1}\lor\ldots\lor\neg n_{im})$. Clearly, the final MaxSAT resolution step will yield an empty clause. Therefore, over all $m+1$ ${\mathcal{L}}_{i}$ constraints, we derive $m+1$ empty clauses.

Table 4 also illustrates the application of the MaxSAT resolution steps to the pairwise encoding of ${\mathcal{M}}_{j}$. At iteration $i$, with $2\leq i\leq m+1$, we apply $i$ MaxSAT resolution steps to derive another empty clause. In total, we derive $m$ empty clauses for each ${\mathcal{M}}_{j}$. An essential aspect is selecting the initial clause from which each sequence of MaxSAT resolution steps is executed. These reused clauses are highlighted in Table 4, and are crucial for getting the right sequence of MaxSAT resolution steps. For each ${\mathcal{M}}_{j}$, the MaxSAT resolution steps can be organized in $m$ phases, each yielding an empty soft clause. For phase $l$, the previous phase $l-1$ produces the clause $(p_{1j}\lor p_{2j}\lor\ldots\lor p_{lj},1)$, which is then iteratively simplified, using unit soft clauses, until the empty soft clause for phase $l$ is derived. It should be noted that the first phase uses two unit soft clauses to produce $(p_{1j}\lor p_{2j},1)$, which is then used in the second phase. As in subsection 4.1, is is immediate that each soft clause is never reused.

Regarding the run time complexity, observe that each MaxSAT resolution step runs in time linear on the number of literals in the clauses. The clauses in the problem formulation have no more than ${\mathcal{O}}(m)$ literals. This also holds true as MaxSAT resolution steps are applied. By analogy with the analysis of the core-guided algorithm, a total of ${\mathcal{O}}(m^{2})$ empty soft clauses will be derived. From the analysis above, summarized in Table 4, deriving the ${\mathcal{O}}(m^{2})$ empty clauses requires a total of ${\mathcal{O}}(m^{3})$ MaxSAT resolution steps. For non-clausal MaxSAT resolution, since the number of generated (non-clausal) terms is constant for each MaxSAT resolution step, then the run time is ${\mathcal{O}}(m^{3})$. In contrast, for clausal MaxSAT resolution [18, Definition 1], since the number of literals for each resolution step is ${\mathcal{O}}(m^{2})$, then the run time becomes ${\mathcal{O}}(m^{5})$.

Proposition 2**.**

For the HornMaxSAT encoding of $\textnormal{PHP}^{m+1}_{m}$, there exists a polynomial sequence of MaxSAT resolution steps, each producing a number of constraints polynomial in the size of the problem formulation, that produces $m(m+1)+1$ soft empty clauses.

• Proof.

(Sketch) The discussion above. ∎

4.3 Integration in SAT Solvers

This section shows that off-the-shelf MaxSAT solvers, which build on CDCL SAT solvers, can solve $\text{PHP}^{m+1}_{m}$ in polynomial time, provided the right order of conflicts is chosen. In turn, this motivates integrating core-guided MaxSAT reasoning into SAT solvers. Similarly, one could consider integrating MaxSAT resolution (or a mix of both [56]) but, like resolution, MaxSAT resolution is harder to implement in practice. The proposed problem transformation can be applied on demand, and the operation of CDCL can be modified to integrate some form of core-guided reasoning. In contrast to other attempts at extending CDCL, the use of MaxSAT reasoning, will build also on CDCL itself.

MaxHS-like Horn MaxSAT.

The reduction to Horn MaxSAT also motivates the development of dedicated MaxSAT solvers. One approach is to build upon MaxHS-solvers [29, 63], since in this case the SAT checks can be made to run in linear time, e.g. using an implementation of LTUR [52]. As indicated above, similar technique can possibly be integrated into SAT solvers.

Handling ${\mathcal{P}}$ clauses.

The ${\mathcal{P}}$ clauses prevent assigning a variable simultaneously value 0 and value 1. As the analysis for the PHP instances suggests, and the experimental results confirm, these clauses can be responsible for non-polynomial run times. One can envision attempting to solve problems without considering the ${\mathcal{P}}$ clauses, and then adding these clauses on demand, as deemed necessary to block non-solutions. The operation is similar to the well-known counterexample-guided abstraction refinement paradigm (CEGAR) [24].

5 Experimental Evaluation

This section evaluates the ideas proposed in the paper in practice, for the case of formulas that are known to be hard for resolution-based reasoning. Concretely, the experimental evaluation shows that the performance gains are provided by the proposed problem transformation and the follow-up core-guided MaxSAT solving.

5.1 Experimental Setup

To illustrate the main points of the paper, a number of solvers were tested. However and in order to save space, the results are detailed below only for some of the tested competitors.555The discussion focuses on the results of the best performing representatives of the considered families of solvers. Solvers that are missing in the discussion are meant to be “dominated” by their representatives, i.e. these solve fewer instances. The families of the evaluated solvers as well as the chosen representatives for the families are listed in Table 5. The family of CDCL SAT solvers comprises MiniSat 2.2 (minisat) and Glucose 3 (glucose) while the family of SAT solvers strengthened with the use of other powerful techniques (e.g. Gaussian elimination, GA and/or cardinality-based reasoning, CBR) includes lingeling (lgl) and CryptoMiniSat (crypto). The MaxSAT solvers include the known tools based on implicit minimum-size hitting set enumeration, i.e. MaxHS (maxhs) and LMHS (lmhs), and also a number of core-guided solvers shown to be best for industrial instances in a series of recent MaxSAT Evaluations666http://www.maxsat.udl.cat, e.g. MSCG (mscg), OpenWBO16 (wbo) and WPM3 (wpm3), as well as the recent MaxSAT solver Eva500a (eva) based on MaxSAT resolution. Other competitors considered include CPLEX (lp), OPB solvers cdcl-cuttingplanes (cc) and Sat4j (sat4j) as well as a solver based on ZBDDs called ZRes (zres).

Note that three configurations of CPLEX were tested: (1) the default configuration and the configurations used in (2) MaxHS and (3) LMHS. Given the overall performance, we decided to present the results for one best performing configuration, which turned out to be the default one. Also, the performance of CPLEX was measured for the following two types of LP instances: (1) the instances encoded to LP directly from the original CNF formulas (see lp-cnf) and (2) the instances obtained from the HornMaxSAT formulas (lp-wcnf). A similar remark can be made with regard to the cc solver: it can deal with the original CNF formulas as well as their OPB encodings (the corresponding configurations of the solver are cc-cnf and cc-opb777The two tested versions of cc-opb (implementing linear and binary search) behave almost identically with a minor advantage of linear search. As a result, cc-opb stands for the linear search version of the solver., respectively).

Regarding the IHS-based MaxSAT solvers, both MaxHS and LMHS implement the Eq-Seeding constraints [30]. Given that all soft clauses constructed by the proposed HornMaxSAT transformation are unit and that the set of all variables of HornMaxSAT formulas is covered by the soft clauses, these eq-seeding constraints replicate the complete MaxSAT formula on the MIP side. As a result, after all disjoint unsatisfiable cores are enumerated by MaxHS or LMHS, only one call to an MIP solver is needed to compute the optimum solution. In order to show the performance of an IHS-based MaxSAT solver with this feature disabled, we additionally considered another configuration of LMHS called lmhs-nes.888We chose LMHS (not MaxHS) because it has a command-line option to disable eq-seeding.

All the conducted experiments were performed in Ubuntu Linux on an Intel Xeon E5-2630 2.60GHz processor with 64GByte of memory. The time limit was set to 1800s and the memory limit to 10GByte for each individual process to run.

5.2 Experimental Results

The efficiency of the selected competitors was assessed on the benchmark suite consisting of 3 sets: (1) pigeonhole formulas (PHP) [27], (2) Urquhart formulas (URQ) [68], and (3) their combinations (COMB).

5.2.1 Pigeonhole Principle benchmarks.

The set of PHP formulas contains 2 families of benchmarks differing in the way $\textsf{AtMost}1$ constraints are encoded: (1) standard pairwise-encoded (PHP-pw) and (2) encoded with sequential counters [65] (PHP-sc). Each of the families contains 46 CNF formulas encoding the pigeonhole principle for 5 to 100 pigeons. Figure 1999Note that all the shown cactus plots below scale the Y axis logarithmically. shows the performance of the solver on sets PHP-pw and PHP-sc. As can be seen, the MaxSAT solvers (except eva and wbo) and also lp-$\ast$ are able to solve all instances. As expected, CDCL SAT solvers perform poorly for PHP with the exception of lingeling, which in some cases detects cardinality constraints in PHP-pw. However, disabling cardinality constraints reasoning or considering the PHP-sc benchmarks impairs its performance tremendously. Also note that we were unable to reproduce the performance of zres applied to PHP reported in [22].

5.2.2 On discarding ${\mathcal{P}}$ clauses.

To confirm the conjecture that the ${\mathcal{P}}$ clauses can hamper a MaxSAT solver’s ability to get good unsatisfiable cores, we also considered both PHP-pw and PHP-sc instances without the ${\mathcal{P}}$ clauses. Figure 2 compares the performance of the MaxSAT solvers working on PHP formulas w/ and w/o the ${\mathcal{P}}$ clauses. The lines with (no P) denote solvers working on the formulas w/o ${\mathcal{P}}$ (except maxhs and lmhs whose performance is not affected by removal of ${\mathcal{P}}$). As detailed in 2(c), the efficiency of wbo is improved by a few orders of magnitude if the ${\mathcal{P}}$ clauses are discarded. Also, as shown in 2(b), mscg gets about an order of magnitude performance improvement outperforming all the other solvers.

5.2.3 Urquhart benchmarks and combined instances.

The URQ instances are known to be hard for resolution [68], but not for BDD-based reasoning [22]. Here, we follow the encoding of [22] to obtain the formulas of varying size given the parameter $n$ of the encoder. In the experiments, we generated 3 CNF formulas for each $n$ from 3 to 30 (i.e. $\text{URQ}_{n,i}$ for $n\in\{3,\ldots,30\}$ and $i\in\{1,2,3\}$), which resulted in 84 instances. As expected, the best performance on the URQ instances is demonstrated by zres. Both maxhs and lmhs are not far behind. Note that both maxhs and lmhs do exactly 1 call to CPLEX (due to eq-seeding) after enumerating disjoint unsatisfiable cores. This contrasts sharply with the poor performance of lp-wcnf, which is fed with the same problem instances. Lingeling if augmented with Gaussian elimination (GA, see lgl in 3(a)) performs reasonably well being able to solve 29 instances. However, as the result for lgl-nogauss suggests, GA is crucial for lgl to efficiently decide URQ. Note that lp-cnf and cc-opb are not shown in 3(a) due to their inability to solve any instance.

The COMB benchmark set is supposed to inherit the complexity of both PHP and URQ instances and contains formulas $\text{PHP}_{m}^{m+1}\lor\text{URQ}_{n,i}$ with the PHP part being pairwise-encoded, where $m\in\{7,9,11,13\}$, $n\in\{3,\ldots,10\}$, and $i\in\{1,2,3\}$, i.e. $|\text{COMB}|=96$. As one can observe in 3(b), even these small $m$ and $n$ result in instances that are hard for most of the competitors. All IHS-based MaxSAT solvers (maxhs, lmhs, and lmhs-nes) perform well and solve most of the instances. Note that lgl is confused by the structure of the formulas (neither CBR nor GA helps it solve these instances). The same holds for zres. As for CPLEX, while lp-cnf is still unable to solve any instance from the COMB set, lp-wcnf can also solve only 18 instances. The opposite observation can be made for cc-cnf and cc-opb.

5.2.4 Summary.

As shown in Table 6, given all the considered benchmarks sets, the proposed problem transformation and the follow-up IHS-based MaxSAT solving can cope with by far the largest number of instances overall (see the data for maxhs, lmhs, and lmhs-nes). The core-guided and also resolution based MaxSAT solvers generally perform well on the pigeonhole formulas (except wbo, and this has to be investigated further), which supports the theoretical claims of papers. However, using them does not help solving the URQ and also COMB benchmarks. Also, as shown in Figure 2, the ${\mathcal{P}}$ clauses can be harmful for MaxSAT solvers. As expected, SAT solvers cannot deal with most of the considered formulas as long as they do not utilize more powerful reasoning (e.g. GA or CBR). However, and as the COMB instances demonstrate, it is easy to construct instances that are hard for the state-of-the-art SAT solvers strengthened with GA and CBR. Finally, one should note the performance gap between maxhs (also lmhs) and lp-wcnf given that they solve the same instances by one call to the same MIP solver with the only difference being the disjoint cores precomputed by maxhs and lmhs.

6 Conclusions & Research Directions

Resolution is at the core of CDCL SAT solving, but it also represents its Achilles’ heel. Many crafted formulas are known to be hard for resolution, with pigeonhole formulas representing a well-known example [27]. More importantly, some of these examples can occur naturally in some practical settings. In the context of MaxSAT, researchers have proposed a dedicated form of resolution, i.e. MaxSAT resolution [18, 46], which was also shown not to be more powerful than propositional resolution [18] for the concrete case of pigeonhole formulas [27].

This paper proposes a general transformation for CNF formulas, by encoding the SAT decision problem as a MaxSAT problem over Horn formulas. The transformation is based on the well-known dual-rail encoding, but it is modified such that all clauses are Horn. More importantly, the paper shows that, on this modified formula, MaxSAT resolution can identify in polynomial time a large enough number of empty soft clauses such that this number implies the unsatisfiability of the original pigeonhole formula. Furthermore, the paper shows that the same argument can be used to prove a polynomial run time for the well-known class of core-guided MaxSAT solvers [54].

Experimental results, obtained on formulas known to be hard for SAT solvers, show that different families of MaxSAT solvers perform far better than the best performing SAT solvers, and also ILP solvers, on these instances.

As the paper also hints at, future work will investigate effective mechanisms for integrating Horn MaxSAT problem transformation and MaxSAT reasoning techniques into SAT solvers. In contrast to cutting planes or extended resolution, MaxSAT algorithms already build on CDCL SAT solvers; this is expected to facilitate integration. Another research direction is to investigate similar transformations for the many other examples for which resolution has exponential lower bounds, but also when to opt to apply such transformations.