# reducing_sat_to_max2sat__714452e0.pdf

Reducing SAT to Max2SAT

Carlos Ans otegui1 and Jordi Levy2

1Logic & Optimization Group (LOG), University of Lleida 2IIIA-CSIC carlos.ansotegui@udl.cat, levy@iiia.csic.es

In the literature we ﬁnd reductions from 3SAT to Max2SAT. These reductions are based on the usage of a gadget, i.e., a combinatorial structure that allows translating constraints of one problem to constraints of another. Unfortunately, the generation of these gadgets lacks an intuitive or efﬁcient method. In this paper, we provide an efﬁcient and constructive method for Reducing SAT to Max2SAT and show empirical results of how Max SAT solvers are more efﬁcient than SAT solvers solving the translation of hard formulas for Resolution.

1 Introduction The SAT problem asks to determine whether there is an assignment to the Boolean variables in a Boolean formula in Conjunctive Normal Form (CNF) that satisﬁes all clauses (constraints). Its optimization version, the Maximum Satisﬁability (Max SAT) problem is the task of ﬁnding an assignment to the variables of the formula such that a maximum number of clauses is satisﬁed. In this paper, we review the reductions from 3SAT into Max2SAT from [Garey et al., 1976] and [Trevisan et al., 2000] (allowing to prove that Max2SAT is NP-Complete). These reductions are based on the usage of a gadget, i.e., a ﬁnite combinatorial structure that allows translating constraints of one problem to constraints of another. Obviously, we also have to ensure that the gadgets can be constructed in polynomial time. Unfortunately, in general, the gadgets available in the literature lack an intuitive and efﬁcient construction method. As stated in [Trevisan et al., 2000]: Despite their importance, the construction of gadgets has always been a black art with no general methods of construction known . The ﬁrst known gadget from 3SAT to Max2SAT was provided by [Garey et al., 1976] and later on in [Trevisan et al., 2000] a gadget of better quality, actually optimal, was automatically computed. In general, we are not just interested in any gadget but those of high quality. Roughly speaking, a (α, β)-gadget from a family of constraints F1 to F2 is a translation of every F1 constraint into β-many F2 constraints such that when the original constraint is falsiﬁed, α 1 many new constraints are falsiﬁed, and when the original constraint is satisﬁed, α

new constraints are satisﬁed. One of the main applications of gadgets is to translate results of in/approximability from one constraint problem to another. A ρ-approximation algorithm for a family of constraint problems F is a polynomial algorithm that computes an assignment that satisﬁes a fraction ρ of the maximum number of satisﬁable constraints. If we have a (α, β)-gadget from F1 to F2 and a ρ-approximation algorithm for F2, then we can obtain a (1 α(1 ρ))- approximation algorithm for F1. Therefore, the smaller the parameter α is, the better the translation works. Notice that, for α = 1, the translation is somehow perfect. [Trevisan et al., 2000], using an optimal (smallest possible α) gadget from 3SAT into Max2SAT, and [Feige and Goemans, 1995] 0.931-approximability result for Max2SAT, were able to prove 0.801-approximability of Max3SAT. However, this approximability bound was later improved with direct techniques, and nowadays it doesn t seem easy to improve approximability or inapproximability results with gadgets. Equipped with gadgets from 3SAT to Max2SAT, SAT can be trivially reduced to Max2SAT by ﬁrst reducing SAT to 3SAT using the folklore gadget that splits a k SAT clause into a set of 3SAT clauses. As we will see, the concatenation of these gadgets is not optimal, even for k = 4. Our ﬁrst contribution in this paper is to provide a new generation method for gadgets from k SAT into Max2SAT to which we refer as the regular gadget. Additionally, we prove the new gadget can be reﬁned by the application of the Max SAT resolution rule, obtaining a gadget with the best α reported so far, for arbitrary k. We also show that the gadget seems to be optimal up to k = 5 by using a MIP solver to prove it. Our second contribution is to prove the usefulness of gadgets to boost SAT solvers. This is an additional application of gadgets not reported so far. In particular, we present an approach that translates SAT into Max2SAT and applies a Max SAT solver. We experiment with several gadgets on SAT instances encoding the Pigeon Hole principle and show the efﬁciency of the new approach. Finally, we sketch a base algorithm that can be used to design a new generation of SAT solvers.

2 Preliminaries A k-ary constraint function is a Boolean function f : {0, 1}k {0, 1}. A constraint family is a set F of con-

Proceedings of the Thirtieth International Joint Conference on Artiﬁcial Intelligence (IJCAI-21)

straint functions (with possibly distinct arities). A constraint, over variables V = {x1, . . . , xn} and constraint family F, is a pair formed by a k-ary constraint function f F and a subset of k variables, noted f(xi1, . . . , xik), or f(x) for simplicity. A (weighted) constraint problem, over variables V and constraint family F, is a multiset of pairs (weight, constraint) over V and F, where the weight is a rational number, noted P = {(w1) f1(x1 i1, . . . , x1 ik1 ), . . . ,(wm) fm(xm i1, . . . , xm ikm )}. In this paper we will focus on constraint functions that may be represented as (weighted) clauses (w) l1 lk, where li s are literals and w a rational weight. An assignment is a function I : {x1, . . . , xn} {0, 1}. We say that an assignment I satisﬁes a constraint f(xi1, . . . , xik), if I(f(x)) =def f(I(xi1), . . . , I(xik)) = 1. The value of an assignment I for a constraint problem P = {(wi) fi(x)}i=1,...,m, is the sum of the weights of the constraints that this assignment satisﬁes, i.e. I(P) = Pm i=1 wi I(fi(x)). An assignment is said to be optimal for a constraint problem if it maximizes its value. We refer to Max Ek SAT as the constraint family deﬁned by the constraint functions of the form f(x1, . . . , xk) = l1 lk, where every li may be either xi or xi. We refer to Max2SAT as the union of the constraint families Max Ei SAT, for 0 i k, and to Max SAT as the union for every i 0.

Deﬁnition 1. An (α, β)-gadget from F1 to F2 is a function that, for any constraint f(x) over F1 returns a weighted constraint problem P = {(wi) gi(x, b)}i=1,...,m over F2 and variables {x} {b}, where b are fresh variables distinct from x, such that β = Pm i=1 wi and, for any assignment I : {x} {0, 1}:

1. If I(f(x)) = 1, for any extension of I to I : {x} {b} {0, 1}, I (P) α and there exists one of such extension with I (P) = α.

2. If I(f(x)) = 0, for any extension of I to I : {x} {b} {0, 1}, I (P) α 1.

Additionally, if there exist one of such extensions with I (P) = α 1, the gadget is said to be strict.

An optimal gadget is a gadget of minimum α.

Lemma 1. The concatenation of a (α1, β1)-gadget from F1 to F2 and a (α2, β2)-gadget from F2 to F3 results into a (β1 (α2 1) + α1, β1β2)-gadget from F1 to F3.

Proof. The ﬁrst gadget multiplies the total weight of constraints by β1, and the second by β2. Therefore, the composition multiplies it by β = β1β2. For any assignment, if the original constraint is falsiﬁed, the optimal extension after the ﬁrst gadget satisﬁes constraints with a weight of α1 1, and falsiﬁes the rest β1 (α1 1). The second gadget satisﬁes constraints for a weight of α2 1 of the falsiﬁed plus α2 of the satisﬁed. Therefore, the composition satisﬁes constraints with a total weight (α2 1)(β1 (α1 1)) + α2(α1 1) = β1(α2 1) + α1 1. If the original constraint is satisﬁed, the optimal extension after the ﬁrst gadget satisﬁes α1 and falsiﬁes the rest β1 α1. After the second gadget the weight of satisﬁed constraints is (α2 1)(β1 α1) + α2α1 = β1(α2 1) + α1.

The difference between both situations is one, hence the composition is a gadget, and α = β1(α2 1) + α1.

3 From 3SAT to Max2SAT In order to show that the Max2SAT problem is NP-hard, it sufﬁces to show that the 3SAT problem can be reduced to the Max2SAT problem. One way to perform such reduction is through the usage of gadgets. Imagine we are given a 3SAT formula. The idea is to replace every clause into the 3SAT formula by a set of Max2SAT clauses polynomial on the size of the clause. The replacement strategy is precisely what we call a gadget. If any clause has fewer than 3 literals, we can simply not apply the gadget. Lemma 2 ([Garey et al., 1976]). Given a 3SAT clause x1 x2 x3, the set of Max2SAT clauses:

Deﬁnes a (7, 10)-gadget from 3SAT to Max2SAT, where b1 is an auxiliary variable.

Proof. Notice that if an assignment satisﬁes x1 x2 x3, then exactly 7 of the 10 Max2SAT clauses can be satisﬁed. On the contrary, if an assignment does not satisfy x1 x2 x3, then exactly 6 of the 10 Max2SAT clauses can be satisﬁed.

Let ϕ be a 3SAT formula of m1 unary, m2 binary and m3 ternary clauses, and ϕ the resulting Max2SAT formula after replacing every ternary clause by the Max2SAT clauses from an (α, β)-gadget from 3SAT into Max2SAT. Then, ϕ is satisﬁable iff the maximum number of satisﬁed clauses in ϕ is m1 +m2 +α m3. As concluded in [Garey et al., 1976], since 3SAT reduces to Max2SAT, it follows that Max2SAT (as a decision problem) is NP-complete.

4 Max SAT Equivalent Gadgets We can further reﬁne the (7, 10)-gadget from [Garey et al., 1976] by applying the Max SAT resolution rule on the set of Max2SAT clauses. This rule was ﬁrst deﬁned by [Larrosa and Heras, 2005; Larrosa et al., 2008], and proven complete by [Bonet et al., 2006; Bonet et al., 2007]. In Max SAT Resolution we proceed by replacing a set of clauses with another set of Max SAT equivalent clauses:

(w) x C1 C2

(w) x C1 C2

Applying the following transformations to the original [Garey et al., 1976] gadget in Lemma 2, and removing the empty clause (2) that we obtain, we get the 3SAT to Max2SAT gadget described in Lemma 3:

Proceedings of the Thirtieth International Joint Conference on Artiﬁcial Intelligence (IJCAI-21)

x1 x1 x2 x2 x3 x1 x3 b1 b1 x1

x1 x3 b1 x1 (2)

Notice that in these gadget transformations we are allowed to remove empty clauses (w) , and it has the effect of reducing the value of α in w (in the case of the [Garey et al., 1976] gadget, from α = 7 to α = 5).

Lemma 3. Given a 3SAT clause x1 x2 x3, the set of Max2SAT clauses:

Deﬁnes a (5, 6)-gadget from 3SAT to Max2SAT, where b1 is an auxiliary variable.

Notice that the set of clauses described in Lemma 3 is unsatisﬁable. Since Max SAT resolution is complete, this means that we could derive an additional empty clause. However, in this refutation process, the rest of the clauses obtained are not binary. Therefore, the process of gadget transformation described in this section, based on Max SAT resolution and empty-clause removal, allows us to simplify and reduce the α of a gadget, but it is not a complete method. In particular, we will see in the next sections that there are more efﬁcient 3SAT to Max2SAT gadgets that cannot be obtained in this way.

5 Computing Gadgets Automatically

In [Trevisan et al., 2000] a gadget from 3SAT to Max2SAT was computed automatically through a Mixed Integer Programming formulation.

Lemma 4 ([Trevisan et al., 2000]). Given a 3SAT clause x1 x2 x3, the set of Max2SAT clauses:

(1/2) x1 x3

(1/2) x1 x3

(1/2) x1 b1

(1/2) x1 b1

(1/2) x3 b1

(1/2) x3 b1

Deﬁnes a (3.5, 4)-gadget from 3SAT to Max2SAT optimal and strict, where b1 is a new fresh auxiliary variable. Notice that all clauses have weight 1/2, except the last one.

We reproduce to some extent the approach in [Trevisan et al., 2000]. The main idea is to limit the search space of possible gadgets to a ﬁnite and reasonably sized one. Given the input k SAT clause x1 xk and a maximum number of auxiliary variables bj, we consider all the possible Max2SAT

k #b α β time 3 1 3.5 4 0.1 4 2 6 7 5 5 3 8.5 10 1200

Table 1: Gadgets for k SAT into Max2SAT automatically computed.

clauses we can build with the xi and bj vars. Then, we create a Mixed Integer Programming formulation that additionally includes a set of positive real variables representing the weight for each of the possible Max2SAT clauses. The idea is to let the MIP solver ﬁnd an assignment to the weight variables that satisﬁes the deﬁnition of an (α, β)-gadget and minimizes the value of α. If the MIT solver ﬁnds weight 0 for a Max2SAT clause, then this clause is not considered in the gadget. In Table 1, we present the results for input clauses of length k and number of auxiliary variables #b. We applied on the MIP formulation the solver Gurobi v9.1. The machine has 2.1GHz and 5GB RAM. We show the α and β of the computed gadget and the time exhausted in less than 8 hours. From the results, we can conclude that we need to come up with a constructive generation method, as we do in the next Section, if we want to scale. However, these results are interesting since they prove that does exist a better gadget in terms of α with a less or equal number of auxiliary variables.

6 From k SAT to Max2SAT A trivial way to reduce Max SAT to Max2SAT is to reduce Max SAT to Max3SAT, and then apply a gadget from Max3SAT into Max2SAT. We can reduce Max SAT to Max3SAT with the following well-known gadget: Lemma 5. Given a k SAT clause x1 . . . xk, the set of Max3SAT clauses:

(1) x1 x2 b1

(1) b1 x3 b2 . . .

(1) bk 4 xk 2 bk 3

(1) bk 3 xk 1 xk

Deﬁnes a (k 2, k 2)-gadget from k SAT to Max3SAT, where b1, b2, . . . , bk 4, bk 3 are fresh auxiliary variables. By Lemma 1, the concatenation of the (k 2, k 2)- gadget from k SAT to Max3SAT (in Lemma 5) with any (α, β)-gadget from Max3SAT to Max2SAT results into a (α(k 2), β(k 2))-gadget from k SAT to Max2SAT. Table 2 shows the result of concatenating the (k 2, k 2)- gadget in Lemma 5 with the (7, 10)-gadget from [Garey et al., 1976] (Lemma 2), with the reﬁned (5, 6)-gadget in Lemma 3 and the (3.5, 4)-gadget from [Trevisan et al., 2000] (Lemma 4), compared with the Regular gadget that we describe below. Now, we introduce a new gadget from k SAT into Max2SAT. The gadget is inspired in the regular encoding [Ans otegui and Many a, 2004] for cardinality constraints. It is not optimal, but easy to generalize for any size of clauses k, it only contains clauses with unit weight and, as we will

Proceedings of the Thirtieth International Joint Conference on Artiﬁcial Intelligence (IJCAI-21)

α β Source 7 (k 2) 10 (k 2) [Garey et al., 1976] 5 (k 2) 6 (k 2) Lemma 3 3.5 (k 2) 4 (k 2) [Trevisan et al., 2000] 2.5 (k 2) + 1 3 (k 2) + 1 Reﬁned Regular

Table 2: Some (α, β)-gadgets from k SAT to Max2SAT.

see later, it can be transformed into a more efﬁcient gadget applying Max SAT resolution.

Theorem 1 (Regular Gadget). Given a k SAT clause x1 . . . xk, the set of Max2SAT clauses, after replacing bk 1 by xk:

(1) xi i = 1, . . . , k

(1) xi bi i = 1, . . . , k 1

(1) xi+1 bi i = 1, . . . , k 2

(1) bi bi+1 i = 1, . . . , k 2

deﬁnes the regular (3 (k 2) + 2, 4 (k 2) + 3)-gadget from k SAT to Max2SAT, where b1, . . . , bk 2 are fresh auxiliary variables.

Proof. When we replace xi by false, for i = 1, . . . , k, and simplify, we get k copies of the empty clause , plus 2k 2 satisﬁed clauses, and the formula {b1 b2, . . . , bk 3 bk 2} that is trivially satisﬁable. Hence, the maximal number of satisﬁed clauses is 3 (k 2) + 1. When some of the xi s are set to true, the number of cases to analyze is bigger. To make it simpler, consider the formula:

ϕ = {xi, xi bi, xi bi 1, bi 1 bi | i = 1, . . . , k}

For any assignment to the original variables, by setting the additional variables b0 = 1, bk = 0 and bk 1 = xk, the number of unsatisﬁed clauses in ϕ is the same as in the original formula (simply, there are 4 more satisﬁed clauses). Let S = {i1, . . . , ir} the ordered list of indexes of variables xi s set to true, where r 1. When we replace the xi s by their values in the formula, and simplify, we get ϕ = {bi 1, bi | i S} {b0 b1, . . . , bk 1 bk}, plus k |S| empty clauses, plus some satisﬁed clauses. For every two consecutive indexes ij, ij+1 S, we get a pairwise disjoint set of minimally unsatisﬁable clauses ϕ j = {bij, bij bij+1, . . . , bij+1 2 bij+1 1, bij+1 1}, and the rest of clauses of ϕ not included in any of these subsets is satisﬁable. Therefore, the minimal number of falsiﬁed clauses in ϕ is |S| 1. Therefore, for any assignment I setting at least one xi to true, the minimal number of falsiﬁed clauses in I(ϕ) is (k |S|) + (|S| 1) = k 1. The same holds for the original set of clauses. Hence the number of satisﬁed clauses is β (k 1) = (4(k 2)+3) (k 1) = 3(k 2)+2 = α.

Now, we show how the process Max SAT resolution and empty-clause elimination described in Section 4, applied to the clauses of this regular gadget (Theorem 1), results into the more efﬁcient gadget described in Theorem 2.

We start transforming

Now, we iterate, for i = 1, . . . , k 2, the following Max SAT resolution (that results from applying 4 times the Max SAT resolution rule):

(1/2) xi+1 bi

(1/2) xi+1 bi+1

(1/2) bi bi+1

(1/2) xi+1 bi

(1/2) xi+1 bi+1

(1/2) bi bi+1

Since xk and bk 1 denote the same variable, we transform

Finally, we remove the clause (k/2) . Theorem 2 (Reﬁned Regular Gadget). Given a k SAT clause x1 . . . xk, the set of Max2SAT clauses, after replacing bk 1 by xk:

(1/2) xi+1 bi, (1/2) xi+1 bi i = 1, . . . , k 2

(1/2) xi+1 bi+1, (1/2) xi+1 bi+1

(1/2) bi bi+1, (1/2) bi bi+1

deﬁnes the (reﬁned) regular (2.5 (k 2) + 1, 3 (k 2) + 1)- gadget from k SAT to Max2SAT, where b1, . . . , bk 2 are fresh auxiliary variables.

Proof. The correctness of this gadget is a consequence of Theorem 1 and the fact that Max SAT resolution and elimination of empty clauses preserve gadgets. The value of β can be easily computed adding the weights of all clauses. The value of alpha can be computed from the original gadget α = 3(k 2) + 2 and removing the weight of the removed empty clauses α = α k/2 = 2.5(k 2) + 1.

Notice that the reﬁned regular gadget, for k = 3, is the same as the [Trevisan et al., 2000] gadget of Lemma 4. Moreover, for k = 3, 4 and 5 the reﬁned regular gadget coincides with the gadgets found automatically in Section 5.

7 Why Reducing SAT to Max2SAT? Suppose that we were able to ﬁnd a (α, β)-gadget from SAT to Max2SAT satisfying α = β. It would allow us to translate any k-clause into a set of binary clauses that is satisﬁable when the original clause is satisﬁed, and unsatisﬁable, when

Proceedings of the Thirtieth International Joint Conference on Artiﬁcial Intelligence (IJCAI-21)

the original clause is unsatisﬁed. In other words, we were able to prove that P=NP. The gadget in Lemma 5 satisﬁes the property α = β reducing SAT to 3SAT, but (obviously) the same is not possible from 3SAT (or SAT) to 2SAT. The following lemma shows us how we can reduce the problem of obtaining (by resolution or similar methods) an empty clause from a formula ϕ, to the problem of obtaining several empty clauses from a 2SAT formula ϕ (by Max SAT resolution or similar methods). In other words, how to solve SAT with a Max SAT solver.

Lemma 6. For any SAT formula ϕ, let ϕ be the formula resulting from replacing every k-clause, with k > 2, by a set of binary clauses using a k SAT to Max2SAT (αk, βk)-gadget. Then ϕ is unsatisﬁable if, and only if, the minimal number of unsatisﬁable clauses in ϕ is at least

(β|C| α|C|)

In the next sections, we will show that this reduction of SAT to Max2SAT makes sense from a practical point of view. Here, we show that it also has some advantages from a theoretical perspective. In particular, we prove that the pigeonhole principle PHPn n 1, which requires exponentially long resolution proofs, when translated into Max2SAT, can be proved applying O(n3) iterations of the Max SAT resolution rule. The idea that Max SAT resolution can be more efﬁcient than the classical resolution to prove some formula was ﬁrst proposed by [Ignatiev et al., 2017; Bonet et al., 2018; Morgado et al., 2019]. There, they prove that after translating the PHPn m principle using the dual-rail encoding, it has polynomial proofs using Max SAT resolution. [Larrosa and Rollon, 2020] prove the same result for Max SAT resolution extended with the split rule and using negative weights. [Atserias and Lauria, 2019] also prove it for circular resolution. Finally, [Bonet and Levy, 2020] prove the equivalence of these last two proof systems and the subsumption of weighted dualrail. In this paper, we take a step forward to the efﬁcient automatization of Max SAT to solve SAT.

Lemma 7. Max SAT resolution obtains (n 1) from Sn i=1{(1) xi} Sn i,j=1 i =j {( ) xi xj} in (n+2)(n 1)

Proof. First, we prove that we can construct the Max SAT resolution proof:

( ) xi xr+1, i = 1, . . . , r

(1) x1 xr+1

in r +1 steps: Cutting (1) x1 xr and ( ) x1 xr+1 we get, among other clauses, (1) x1 xr+1 and (1) x2 xr xr+1. Now, iterativelly, we cut (1) xj xr xr+1 and ( ) xj xr+1 to obtain, among other clauses, (1) xj+1 xr xr+1, for j = 2, . . . , r. Finally we cut (1) xr+1 and

(1) xr+1 to obtain an empty clause.

To obtain the desired proof, we repeat the previous proof iterativelly, for r = 1, ..., n 1, obtaining (n 1) . The total number of rule applications is Pn 1 r=1 r+1 = (n+2)(n 1)

Consider the Pigeon-Hole Problem PHPn m with n pigeons, m holes and n > m where Boolean var xi,j set to true means pigeon i goes in hole j. We have two sets of clauses: a set of At-Least-One (ALO) clauses meaning that a pigeon must go on at least one hole, and a set of At-Most-One (AMO) clauses meaning that no two pigeons can go to the same hole. We can encode this problem into SAT as follows:

i=1 {xi,1 xi,m}

i,i =1 i =i

{xi,j xi ,j}

The translation of the ALO clauses using the (original) regular gadget results into the set of unary clauses Sn i=1 Sm j=1{(1) xi,j} plus some binary clauses. The set of AMO clauses does not need to be translated since they are already binary. Moreover, they can be assigned inﬁnite weight since they must be satisﬁed by the Max SAT solver. In order to conclude the unsatisﬁability of the original PHPn m principle, the Max SAT solver must obtain at least 1 + n(βm αm) = 1+n(4(m 2)+3 (3(m 2)+2) = 1+n(m 1) empty clauses.

Theorem 3. The translation of PHPn m principle to Max2SAT using the original Regular gadget has Max SAT refutation proofs of size O(m n2).

Proof. In the proof, we only need to consider the unary clauses and the binary inﬁnite-weighted clauses (the other binary clauses are not needed in the proof). We can decompose the formula as ϕ = Sm j=1 ϕj, where ϕj = Sn i=1{(1) xi,j} Sn i,i =1 i =i {xi,j xi ,j}. According to Lemma 7, from each

ϕj we can obtain (n 1) in (n+2)(n 1)

2 Max SAT refutation steps. For all the formulas, we will get (m(n 1)) in m (n+2)(n 1)

2 steps. When n > m, the number of empty clauses obtained m(n 1) is bigger than or equal to the number of required empty clauses 1+n(m 1), which proves the unsatisﬁability of PHPn m.

8 Solving SAT Through Max SAT in Practice

In this section, we explore the potential of gadgets from SAT into Max2SAT in order to solve SAT formulas that are hard to Resolution. We evaluate the usefulness of gadgets on the Pigeon Hole Principle. For the experiments, we used a machine of 2.1GHz and 5GB RAM memory. In table 3, we show the experiments we have conducted. In particular, we experimented with SAT solver Ca Di Ca L (version 1.0.3), winner of the SAT Race 2019 [Biere, 2019] and the top performing three Max SAT solvers from the weighted category of the Max SAT Evaluation 2020 [Bacchus et al., 2019]: RC2 [Ignatiev et al., 2019], Max HS [Davies and Bacchus, 2011] and Uwrmaxsat [Piotr ow, 2020]. The Ca Di Ca L SAT solver was run on the SAT instance (say ϕ) that encodes the Pigeon-Hole principle as described in

Proceedings of the Thirtieth International Joint Conference on Artiﬁcial Intelligence (IJCAI-21)

n 12 13 14 15 20 30 50 100 SAT Ca Di Ca L 17.6 91 500 3526 - - - - Max HS 3236 - - - - - - - UWr 988 - - - - - - - Max2SAT [Garey et al., 1976] RC2 0.1 0.1 0.13 0.23 0.74 4.48 43.75 1347 Max HS 0.1 0.1 0.11 0.11 0.43 2.20 58.34 1174 UWr 0.1 0.1 0.13 0.19 0.68 3.97 35.66 1046 Max2SAT [Trevisan et al., 2000] RC2 32 218 11602 - - - - - Max HS 0.1 0.14 0.2 5569 - - - - UWr 380 12835 4288 - - - - - Max2SAT Regular RC2 0 0 0 0.1 0.1 0.22 0.93 10.5 Max HS 0 0 0 0 0 0 0.15 1.35 UWr 0 0.1 0.4 0 0 0.1 0.16 1.39

Table 3: Run times for PHPn n 1 encodings. - stands for timeout.

Section 7. In particular, we created PHP n n 1 SAT instances for n {11, 12, 13, 14, 15, 20, 30, 50, 100}. The Max SAT solvers were run on a Max SAT formula built from the generated PHPn n 1 SAT instance ϕ as follows: the 2SAT clauses in ϕ are assigned weight and the rest (n 1)- ary clauses are translated into Max SAT using a gadget. In the ﬁrst 3 rows of table 3, we can see the result of applying the Ca Di Ca L solver and the Max SAT solvers on the original SAT instances. For the Max SAT solvers, we use as input the Max SAT formula that incorporates with weight all the clauses of the SAT instance (RC2 was not able to accept this input). As we can see, the Max SAT solvers are not as powerful as the Ca Di Ca L SAT solver. Ca Di Ca L can to solve the SAT instances, in less than 8 hours, up to n = 15. In the next 6 rows, we show the behavior of the Max SAT solvers on the concatenation of the gadget from Lemma 5 and the gadgets from [Garey et al., 1976] and [Trevisan et al., 2000], respectively. As we can see, Max SAT solvers with the [Garey et al., 1976] gadget work much better than the SAT approach with Ca Di Ca L, and they are able to solve n = 100 in around 20 minutes. On the other hand, with [Trevisan et al., 2000] we see better results than with Ca Di Ca L but the impact is less obvious. There is also an erratic behaviour of Max HS on n = 14 and 15, and of Uwrmaxsat on n = 13. In the last 3 rows, we present the results with the Regular gadget. Clearly, it is the best performing one and allows all the Max SAT solvers to solve n = 100 in less than 2 seconds. For the regular gadget and n = 100, we additionally shufﬂed the instance 100 times, obtaining the (median, max) results: Uwrmaxsat (3.14, 3.49), Max HS (2.80, 3.19) which conﬁrm the goodness of the gadget and, RC2 (22.4, 383.25) that seems to be affected by the shufﬂing. Finally, based on our ﬁndings we present Algorithm 1 that intends to be a conceptual base for a new generation of SAT solvers. It takes as input the SAT CNF instance to be solved, an (α, β)-gadget and a Max SAT solver. Algorithm 1 relies on two points. First, to ﬁnd a good balance between which clauses we keep as hard and which are translated with the gadget. Second, to preserve as hard that subset of clauses that is not too hard to solve, for example,

Algorithm 1: SAT through Max SAT

1 Input: CNF ϕ, (α, β)-gadget G, Max SAT solver MS

4 while S, ϕ next subset(ϕ) do

5 for C S do

6 if harden(C) then

7 φ φ {( ) C}

10 lb lb + β|C| α|C|

11 opt MS(φ)

12 if opt > lb then

13 return Unsat

14 return Sat

any polynomial class, like 2SAT, Horn, etc. Second, when we apply the gadget to a subset of clauses, we immediately get a lower bound on the cost the Max SAT solver will ﬁnd for that particular set of clauses. That is the sum of β|C| α|C|, for each clause C we translate to Max2SAT through the gadget. Moreover, if for this subset of clauses the Max SAT solver is able to ﬁnd a greater cost than the mentioned lower bound then we can conclude that the original set of k SAT clauses is unsatisﬁable. This way we make SAT solvers approaches able to count, being the absence of this capacity what precisely lies at the very heart of the drawbacks of Resolution. In particular, Algorithm 1 iterates on subsets of the original input SAT instance (line 4) till all the formula has been processed. Then, for every clause in the current subset, it decides whether it has to be hard (function harden at line 6) or it has to be translated into a set of Max2SAT clauses through the input gadget. The resulting Max SAT clauses are added to the working formula ϕ (lines 7 and 9). Whenever a clause is translated through the gadget the lower bound lb is increased according to β|C| α|C| (line 10). If the Max SAT solver executed on ϕ returns a cost greater than lb we can stop and declare the input SAT formula is unsatisﬁable (line 13).

9 Conclusions In this paper, we have contributed to ﬁlling the gap between SAT and Max SAT towards the promise of Max SAT to boost SAT. We have presented a constructive method for generating a new (α,β)-gadget from k SAT into Max2SAT. Although gadgets have been used in the literature to improve approximability and non-approximability results, here we have introduced a new application. In particular, we have shown how these gadgets can be applied to solve efﬁciently SAT formulas that are hard for resolution, which can constitute the base for a new generation of SAT solvers.

Acknowledgements Supported by projects PROOFS (PID2019-109137GB-C21) and EU-H2020-RIP LOGISTAR (No. 769142).

Proceedings of the Thirtieth International Joint Conference on Artiﬁcial Intelligence (IJCAI-21)

[Ans otegui and Many a, 2004] Carlos Ans otegui and Felip Many a. Mapping problems with ﬁnite-domain variables into problems with boolean variables. In SAT 2004 - The Seventh International Conference on Theory and Applications of Satisﬁability Testing, 10-13 May 2004, Vancouver, BC, Canada, Online Proceedings, 2004.

[Atserias and Lauria, 2019] Albert Atserias and Massimo Lauria. Circular (yet sound) proofs. In Mikol as Janota and Inˆes Lynce, editors, Theory and Applications of Satisﬁability Testing - SAT 2019 - 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings, volume 11628 of Lecture Notes in Computer Science, pages 1 18. Springer, 2019.

[Bacchus et al., 2019] Fahiem Bacchus, Matti J arvisalo, and Ruben Martins. Max SAT Evaluation 2019 : Solver and Benchmark Descriptions. Technical Report Department of Computer Science Report Series B-2019-2, University of Helsinki, 2019.

[Biere, 2019] Armin Biere. Ca Di Ca L at the SAT Race 2019. In Marijn Heule, Matti J arvisalo, and Martin Suda, editors, Proc. of SAT Race 2019 Solver and Benchmark Descriptions, volume B-2019-1 of Department of Computer Science Series of Publications B, pages 8 9. University of Helsinki, 2019.

[Bonet and Levy, 2020] Maria Luisa Bonet and Jordi Levy. Equivalence between systems stronger than resolution. In Luca Pulina and Martina Seidl, editors, Theory and Applications of Satisﬁability Testing - SAT 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings, volume 12178 of Lecture Notes in Computer Science, pages 166 181. Springer, 2020.

[Bonet et al., 2006] Maria Luisa Bonet, Jordi Levy, and Felip Many a. A complete calculus for max-sat. In Armin Biere and Carla P. Gomes, editors, Theory and Applications of Satisﬁability Testing - SAT 2006, 9th International Conference, Seattle, WA, USA, August 12-15, 2006, Proceedings, volume 4121 of Lecture Notes in Computer Science, pages 240 251. Springer, 2006.

[Bonet et al., 2007] Maria Luisa Bonet, Jordi Levy, and Felip Many a. Resolution for Max-SAT. Artif. Intell., 171(89):606 618, 2007.

[Bonet et al., 2018] Maria Luisa Bonet, Sam Buss, Alexey Ignatiev, Jo ao Marques-Silva, and Ant onio Morgado. Maxsat resolution with the dual rail encoding. In Sheila A. Mc Ilraith and Kilian Q. Weinberger, editors, AAAI, pages 6565 6572, 2018.

[Davies and Bacchus, 2011] Jessica Davies and Fahiem Bacchus. Solving MAXSAT by solving a sequence of simpler SAT instances. In Jimmy Ho-Man Lee, editor, Principles and Practice of Constraint Programming - CP 2011 - 17th International Conference, CP 2011, Perugia, Italy, September 12-16, 2011. Proceedings, volume 6876 of Lecture Notes in Computer Science, pages 225 239. Springer, 2011.

[Feige and Goemans, 1995] U. Feige and M. Goemans. Approximating the value of two power proof systems, with applications to MAX 2SAT and MAX DICUT. In Proceedings Third Israel Symposium on the Theory of Computing and Systems, pages 182 189, 1995. [Garey et al., 1976] M. R. Garey, David S. Johnson, and Larry J. Stockmeyer. Some simpliﬁed np-complete graph problems. Theor. Comput. Sci., 1(3):237 267, 1976. [Ignatiev et al., 2017] Alexey Ignatiev, Ant onio Morgado, and Jo ao Marques-Silva. On tackling the limits of resolution in SAT solving. In Proc. of the 20th Int. Conf. on Theory and Applications of Satisﬁability Testing, SAT 17, pages 164 183, 2017. [Ignatiev et al., 2019] Alexey Ignatiev, Ant onio Morgado, and Jo ao Marques-Silva. RC2: an efﬁcient maxsat solver. J. Satisf. Boolean Model. Comput., 11(1):53 64, 2019. [Larrosa and Heras, 2005] Javier Larrosa and Federico Heras. Resolution in max-sat and its relation to local consistency in weighted csps. In IJCAI, pages 193 198, 2005. [Larrosa and Rollon, 2020] Javier Larrosa and Emma Rollon. Augmenting the power of (partial) maxsat resolution with extension. In The Thirty-Fourth AAAI Conference on Artiﬁcial Intelligence, AAAI 2020, The Thirty-Second Innovative Applications of Artiﬁcial Intelligence Conference, IAAI 2020, The Tenth AAAI Symposium on Educational Advances in Artiﬁcial Intelligence, EAAI 2020, New York, NY, USA, February 7-12, 2020, pages 1561 1568. AAAI Press, 2020. [Larrosa et al., 2008] Javier Larrosa, Federico Heras, and Simon de Givry. A logical approach to efﬁcient max-sat solving. Artif. Intell., 172(2-3):204 233, 2008. [Morgado et al., 2019] Ant onio Morgado, Alexey Ignatiev, Maria Luisa Bonet, Jo ao Marques-Silva, and Sam Buss. Drmaxsat with maxhs: First contact. In Mikol as Janota and Inˆes Lynce, editors, Theory and Applications of Satisﬁability Testing - SAT 2019 - 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings, volume 11628 of Lecture Notes in Computer Science, pages 239 249. Springer, 2019. [Piotr ow, 2020] Marek Piotr ow. Uwrmaxsat: Efﬁcient solver for maxsat and pseudo-boolean problems. In 32nd IEEE International Conference on Tools with Artiﬁcial Intelligence, ICTAI 2020, Baltimore, MD, USA, November 9-11, 2020, pages 132 136. IEEE, 2020. [Trevisan et al., 2000] Luca Trevisan, Gregory B. Sorkin, Madhu Sudan, and David P. Williamson. Gadgets, approximation, and linear programming. SIAM J. Comput., 29(6):2074 2097, 2000.

Proceedings of the Thirtieth International Joint Conference on Artiﬁcial Intelligence (IJCAI-21)