Reducing SAT to Max2SAT

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 satisfies all clauses (constraints). Its optimization version, the Maximum Satisfiability (MaxSAT) problem is the task of finding an assignment to the variables of the formula such that a maximum number of clauses is satisfied.

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 finite 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 efficient 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 first 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 falsified, α - 1 many new constraints are falsified, and when the original constraint is satisfied, α

new constraints are satisfied. 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 satisfies a fraction ρ of the maximum number of satisfiable 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 first reducing SAT to 3SAT using the folklore gadget that splits a kSAT clause into a set of 3SAT clauses. As we will see, the concatenation of these gadgets is not optimal, even for k = 4.

Our first contribution in this paper is to provide a new generation method for gadgets from kSAT into Max2SAT to which we refer as the regular gadget. Additionally, we prove the new gadget can be refined by the application of the MaxSAT 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 MaxSAT solver. We experiment with several gadgets on SAT instances encoding the Pigeon Hole principle and show the efficiency 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 constraint 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(x1i1 , . . . , x1ik1 ), . . . ,(wm) fm(xmi1 , . . . , xmikm )}. 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 satisfies 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 satisfies, i.e. I(P) = ∑mi=1 wi I(fi(x)). An assignment is said to be optimal for a constraint problem if it maximizes its value.

We refer to MaxEkSAT as the constraint family defined 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 MaxEiSAT, for 0 ≤ i ≤ k, and to MaxSAT as the union for every i ≥ 0.

Definition 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 β = ∑mi=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 fromF1 to F3.

Proof. The first 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 falsified, the optimal extension after the first gadget satisfies constraints with a weight of α1 - 1, and falsifies the rest β1 - (α1 -

• 1). The second gadget satisfies constraints for a weight of α2 - 1 of the falsified plus α2 of the satisfied. Therefore, the composition satisfies constraints with a total weight (α2 -

1)(β1 - (α1 - 1)) + α2(α1 - 1) = β1(α2 - 1) + α1 - 1. If the original constraint is satisfied, the optimal extension after the first gadget satisfies α1 and falsifies the rest β1 -α1. After the second gadget the weight of satisfied 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 toMax2SAT

In order to show that the Max2SAT problem is NP-hard, it suffices 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:

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

Proof. Notice that if an assignment satisfies x1∨x2∨x3, then exactly 7 of the 10 Max2SAT clauses can be satisfied. On the contrary, if an assignment does not satisfy x1 ∨x2 ∨x3, then exactly 6 of the 10 Max2SAT clauses can be satisfied.

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 satisfiable iff the maximum number of satisfied 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 MaxSAT Equivalent Gadgets

We can further refine the (7, 10)-gadget from [Garey et al., 1976] by applying the MaxSAT resolution rule on the set of Max2SAT clauses. This rule was first defined by [Larrosa and Heras, 2005; Larrosa et al., 2008], and proven complete by [Bonet et al., 2006; Bonet et al., 2007]. In MaxSAT Resolution we proceed by replacing a set of clauses with another set of MaxSAT equivalent clauses:

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:

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:

Defines 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 unsatisfiable. Since MaxSAT 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 MaxSAT 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 efficient 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:

Defines 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 finite and reasonably sized one. Given the input kSAT clause x1 ∨ · · · ∨ xk and a maximum number of auxiliary variables bj , we consider all the possible Max2SAT

5 3 8.5 10 1200

Table 1: Gadgets for kSAT 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 find an assignment to the weight variables that satisfies the definition of an (α, β)-gadget and minimizes the value of α. If the MIT solver finds 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 kSAT toMax2SAT

A trivial way to reduce MaxSAT to Max2SAT is to reduce MaxSAT to Max3SAT, and then apply a gadget from Max3SAT into Max2SAT. We can reduce MaxSAT to Max3SAT with the following well-known gadget:

Lemma 5. Given a kSAT clause x1 ∨ . . . ∨ xk, the set of Max3SAT clauses:

Defines a (k-2, k-2)-gadget from kSAT 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 kSAT to Max3SAT (in Lemma 5) with any (α, β)-gadget from Max3SAT to Max2SAT results into a (α(k - 2), β(k - 2))-gadget from kSAT 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 refined (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 kSAT 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 see later, it can be transformed into a more efficient gadget applying MaxSAT resolution.

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

defines the regular (3 (k - 2) + 2, 4 (k - 2) + 3)-gadget from kSAT 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 satisfied clauses, and the formula {b1 ∨ b2, . . . , bk-3 ∨ bk-2} that is trivially satisfiable. Hence, the maximal number of satisfied 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:

For any assignment to the original variables, by setting the additional variables b0 = 1, bk = 0 and bk-1 = xk, the number of unsatisfied clauses in ϕ is the same as in the original formula (simply, there are 4 more satisfied 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 satisfied clauses. For every two consecutive indexes ij, ij+1 ∈ S, we get a pairwise disjoint set of minimally unsatisfiable 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 satisfiable. Therefore, the minimal number of falsified clauses in ϕ′ is |S|-1. Therefore, for any assignment I setting at least one xi to true, the minimal number of falsified clauses in I(ϕ) is (k - |S|) + (|S| - 1) = k - 1. The same holds for the original set of clauses. Hence the number of satisfied clauses is β-(k-1) = (4(k-2)+3)-(k-1) = 3(k-2)+2 = α.

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

We start transforming

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

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

Finally, we remove the clause (k/2) .

Theorem 2 (Refined Regular Gadget). Given a kSAT clause x1 ∨ . . . ∨ xk, the set of Max2SAT clauses, after replacing bk-1 by xk:

defines the (refined) regular (2.5 (k - 2) + 1, 3 (k - 2) + 1)- gadget from kSAT 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 MaxSAT 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 refined 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 refined regular gadget coincides with the gadgets found automatically in Section 5.

7 Why Reducing SAT toMax2SAT?

Suppose that we were able to find a (α, β)-gadget from SAT to Max2SAT satisfying α = β. It would allow us to translate any k-clause into a set of binary clauses that is satisfiable when the original clause is satisfied, and unsatisfiable, when the original clause is unsatisfied. In other words, we were able to prove that P=NP. The gadget in Lemma 5 satisfies 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 MaxSAT resolution or similar methods). In other words, how to solve SAT with a MaxSAT 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 kSAT to Max2SAT (αk, βk)-gadget. Then ϕ is unsatisfiable if, and only if, the minimal number of unsatisfiable clauses in ϕ′ is at least

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 PHPnn-1 , which requires exponentially long resolution proofs, when translated into Max2SAT, can be proved applying O(n3 ) iterations of the MaxSAT resolution rule.

The idea that MaxSAT resolution can be more efficient than the classical resolution to prove some formula was first proposed by [Ignatiev et al., 2017; Bonet et al., 2018; Morgado et al., 2019]. There, they prove that after translating the PHPnm principle using the dual-rail encoding, it has polynomial proofs using MaxSAT resolution. [Larrosa and Rollon, 2020] prove the same result for MaxSAT 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 efficient automatization of MaxSAT to solve SAT.

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

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 ∑n-1 r=1 r+1 = (n+2)(n-1) 2 .

Consider the Pigeon-Hole Problem PHPnm 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:

The translation of the ALO clauses using the (original) regular gadget results into the set of unary clauses ⋃ni=1 ⋃mj=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 infinite weight since they must be satisfied by the MaxSAT solver. In order to conclude the unsatisfiability of the original PHPnm principle, the MaxSAT 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 PHPnm principle to Max2SAT using the original Regular gadget has MaxSAT refutation proofs of size O(mn2 ).

Proof. In the proof, we only need to consider the unary clauses and the binary infinite-weighted clauses (the other binary clauses are not needed in the proof). We can decompose the formula as ϕ = ⋃mj=1 ϕj , where ϕj = ⋃ni=1 {(1) xi,j} ∪ ⋃ni,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 MaxSAT 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 unsatisfiability of PHPnm.

8 Solving SAT ThroughMaxSAT 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 CaDiCaL (version 1.0.3), winner of the SAT Race 2019 [Biere, 2019] and the top performing three MaxSAT solvers from the weighted category of the MaxSAT Evaluation 2020 [Bacchus et al., 2019]: RC2 [Ignatiev et al., 2019], MaxHS [Davies and Bacchus, 2011] and Uwrmaxsat [Piotr´ow, 2020].

The CaDiCaL SAT solver was run on the SAT instance (say ϕ) that encodes the Pigeon-Hole principle as described in Section 7. In particular, we created PHP n n-1 SAT instances for n ∈ {11, 12, 13, 14, 15, 20, 30, 50, 100}.

The MaxSAT solvers were run on a MaxSAT formula built from the generated PHPnn-1 SAT instance ϕ as follows: the 2SAT clauses in ϕ are assigned ∞weight and the rest (n-1)- ary clauses are translated into MaxSAT using a gadget.

In the first 3 rows of table 3, we can see the result of applying the CaDiCaL solver and the MaxSAT solvers on the original SAT instances. For the MaxSAT solvers, we use as input the MaxSAT 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 MaxSAT solvers are not as powerful as the CaDiCaL SAT solver. CaDiCaL 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 MaxSAT 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, MaxSAT solvers with the [Garey et al., 1976] gadget work much better than the SAT approach with CaDiCaL, 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 CaDiCaL but the impact is less obvious. There is also an erratic behaviour of MaxHS 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 MaxSAT solvers to solve n = 100 in less than 2 seconds. For the regular gadget and n = 100, we additionally shuffled the instance 100 times, obtaining the (median, max) results: Uwrmaxsat (3.14, 3.49), MaxHS (2.80, 3.19) which confirm the goodness of the gadget and, RC2 (22.4, 383.25) that seems to be affected by the shuffling.

Finally, based on our findings 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 MaxSAT solver.

Algorithm 1 relies on two points. First, to find 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 MaxSAT

1 Input: CNF ϕ, (α, β)-gadget G, MaxSAT solver MS 2 lb ← 0 3 φ← ∅ 4 while 〈S, ϕ〉 ←next subset(ϕ) do 5 for C ∈ S do 6 if harden(C) then 7 φ ← φ ∪ {(∞) C} 8 else 9 φ ← φ ∪ G(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 MaxSAT solver will find 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 MaxSAT solver is able to find a greater cost than the mentioned lower bound then we can conclude that the original set of kSAT clauses is unsatisfiable. 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 MaxSAT 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 MaxSAT solver executed on ϕ returns a cost greater than lb we can stop and declare the input SAT formula is unsatisfiable (line 13).

9 Conclusions

In this paper, we have contributed to filling the gap between SAT and MaxSAT towards the promise of MaxSAT to boost SAT. We have presented a constructive method for generating a new (α,β)-gadget from kSAT into Max2SAT. Although gadgets have been used in the literature to improve approximability and non-approximability results, here we have introduced a newapplication. In particular, we have shown how these gadgets can be applied to solve efficiently 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).