Resolution and Domination: An Improved Exact MaxSAT Algorithm

1 Introduction

The SATISFIABILITY problem and many of its variants are arguably the most influential problems due to their significant applications in a wide range of areas. Though most of these problems turn out to be computationally hard [Garey and Johnson, 1979; Garey et al., 1976; Schaefer, 1978], their significance still drives both theorists and practitioners to derive approaches to solve the problems. Prominent approaches include deriving approximation, randomized, heuristic algorithms, etc. [Poloczek et al., 2017; Bliznets, 2013; Goemans and Williamson, 1994; Luo et al., 2017; Poloczek et al., 2017; Cai et al., 2014]. In addition, many powerful solvers for these problems have been developed [Hutter et al., 2017; Sohanghpurwala et al., 2017]. However, given that these problems are intrinsically hard, none of these heuristic-based solvers is able to solve all instances. Another important and complementary line of research is developing exact algorithms. First, with the rapid development of computer techniques, many exponential-time algorithms (especially singleexponential algorithms) can be also implemented in an acceptable time. This motivates researchers to improve the running times of exact algorithms for many NP-hard problems (see, e.g., [Chen et al., 2010; Gupta et al., 2018]). Second, principles behind exact algorithms might be useful for practitioners to improve their heuristic algorithms. For instance, combined with refined pruning techniques, branching strategies in exact branching algorithms can be employed in heuristic or machine learning algorithms [Sturtevant, 2003; Marques-Silva, 1999], and preprocessing procedures in many exact algorithms can be even directly used in heuristic algorithms [Wang et al., 2018].

∗Contact Author

In this paper, we study an exact algorithm for the (decision version) of the MAXIMUM SATISFIABILITY (MAXSAT) problem, which has significant applications in many areas (see [Morgado et al., 2013] for a survey). Particularly, in this problem, we are given a Conjunctive Normal Form (CNF) formula F with m clauses and n Boolean variables, together with an integer k, and the question is whether there is an assignment satisfying at least k clauses in F. It has long been known that the MaxSAT problem is NP-hard, even in several special cases such as when every clause consists of only two literals and each variable occurs in at most three clauses [Raman et al., 1998]. Our main result is an exact branching algorithm of running time O∗ (1.2989m), which significantly improves the previous best result O∗ (1.3248m) by Chen and Kanj [2004] published 15 years ago. To this end, we propose several new reduction rules to shrink the size of the input instances. Moreover, based on the reduction rules and by refined observations, we put forward novel branching strategies for variables of degrees 3, 4, and 5. Table 1 summarizes recent progress of exact algorithms for the MAXSAT problem.

Finally, it should be pointed out that with respect to the parameter n, the MAXSAT problem cannot be solved in O∗ (2cn ) time for any constant c < 1 in the worst case, assuming the Strong Exponential Time Hypothesis

(SETH) [Impagliazzo and Paturi, 2001]. In addition, Chen and Kanj [2004] also presented an algorithm of running time O∗ (1.3695k ) which has been improved to O∗ (1.325k ) very recently [Chen et al., 2017]. Our algorithm does not improve this bound.

2 Preliminary

We assume that the reader is familiar with the basics of propositional logic. A Boolean variable is a variable that can be assigned either the value 1 (TRUE) or 0 (FALSE). Throughout this paper, we simply use variables for Boolean variables. A literal is either a variable x or its negation x. Note that the negation of x is x, i.e., x = x. A clause is a disjunction of several literals. For instance, C = x1 ∨ x2 ∨ x3 is a clause of three literals x1, x2, and x3. For simplicity, we omit the symbol ∨. Note that the order of the literals in a clause is irrelevant to the clause's identity. Hence, x1x2x3 = x2x1x3. For two clauses C1 and C2, we use C1C2 to denote the clause consisting of all literals included in at least one of C1 and C2. For a clause C and a literal x, C \ x is the clause C without the literal x. A conjunctive norm form (CNF) formula F = C1 ∧ C2 ∧ · · · ∧ Cm is a conjunction of clauses. An assignment f is a function which assigns to each variable x of F a value f(x) ∈ {0, 1}. A clause C is satisfied by f if at least one literal in C gets the value 1. An optimal assignment refers to one that satisfies the maximum number of clauses. For simplicity, for a clause C, we use f(C) = 0 (or C = 0) for that every literal in C has the value 0. In this case, C is unsatisfied by f. However, by f(C) = 1 (or C = 1) we mean that at least one literal of C obtains the value 1 from f, to indicate that the clause C is satisfied by f.

A literal x is an i-literal if x occurs i times in F. In addition, we say that x is an (i, j)-literal if x and x appear respectively i and j times in F. The degree of the variable x is then defined as i + j. A variable x of degree h (resp. at least h) is also called an h-variable (resp. h+-variable). The size of a clause C, denoted |C|, is the number of literals in C. A clause is an h-clause if its size is h, and an h+-clause if its size is at least h. In particular, a 1-clause is also called a unit clause. An (i, 1)-literal x is called a singleton (resp. non-singleton) if the literal x appears in a unit clause x (resp. a 2+-clause).

Resolution on a variable x in F is the operation that for every pair of clauses xC and xD in F , first creates a clause CD, and then removes from F all clauses including the variable x.

3 Reduction Rules

In this section, we present numerous reduction rules, some of which have been studied in the literature but many are new. These reduction rules are designed for eliminating some specific combinatorial structures in order for the applications of branching rules studied in the next section and shrinking the size of the given formula. A CNF formula is reduced by some reduction rules if none of the reduction rules applies to this formula. Let F be a given CNF formula. In the following, before introducing the j-th reduction rule, j > 1, we assume that F is reduced by all the reduction rules introduced before. For two instances (F, k) and (F ′ , k′ ), (F, k) → (F ′ , k′ ) means that a reduction rule transforms (F, k) into (F ′ , k′ ).

Moreover, by Fx=1 we mean a CNF formula obtained from F by assigning x = 1. More precisely, Fx=1 is obtained from F by removing all clauses including the literal x and removing the literal x from all clauses including the literal x. A reduction rule is sound if for every MAXSAT instance I, it holds that I is a YES-instance if and only if the instance obtained from I by applying this rule is a YES-instance. The first six reduction rules have been studied in the literature.

R-Rule 1 ([Bansal and Raman, 1999]).

R-Rule 2 ([Bansal and Raman, 1999]).

(F ∧ xC ∧ xC, k) → (F ∧ C, k - 1).

R-Rule 3 ([Chen and Kanj, 2004]). If there is an (i, j)- literal x in the CNF formula F which contains at least j unit clauses x, then (F, k) → (Fx=1, k - i).

For instance, if there is a (4, 1)-literal x and the five clauses including the variable x are x, xC1, xC2, xC3, and xD, then we can directly assign x the value 1 due to R-Rule 3. Note that a special case of R-Rule 3 is when j = 0, i.e., a variable occurs in all clauses in the same form (positive or negative).

R-Rule 4 ([Bansal and Raman, 1999]). If there is a (1, 1)- literal x, then (F ∧ xC1 ∧ xC2, k) → (F ∧ C1C2, k - 1).

R-Rule 5 ([Bliznets and Golovnev, 2012]). If there is a 3variable x and a 2-clause xy, then

(F ∧ xy ∧ xC ∧ xD, k) → (F ∧ yD ∧ yCD, k - 1).

R-Rule 6 ([Li et al., 2007]). If there are clauses xy, x, and y, then (F ∧ xy ∧ x ∧ y, k) → (F ∧ xy, k - 1).

Inspired by R-Rule 6, we propose a new rule as follows.

R-Rule 7. If there are clauses xyz, x, y, and z, then

(F ∧ xyz ∧ x ∧ y ∧ z, k) → (F ∧ xyz ∧ xz ∧ yz, k).

Lemma 1. R-Rule 7 is sound.

Proof. Let ρ be an assignment. Let F1 = xyz ∧ x ∧ y ∧ z and F2 = xyz ∧ xz ∧ yz. If ρ(x) = ρ(y) = ρ(z) = 1, only one clause in both F1 and F2 is satisfied. If exactly one of ρ(x), ρ(y), and ρ(z) is 0, then exactly two clauses in F1 and F2 are satisfied. Otherwise, exactly three clauses in both F1 and F2 are satisfied.

Notice that in R-Rule 6 we decrease k by one, but in RRule 7 the value of k is unchanged. Now we introduce numerous new reduction rules to eliminate (i, 1)-literals with some specific structures. The worst branching case of the previous best algorithm studied in [Chen and Kanj, 2004] is the (5, 1)- branching at (i, 1)-literals. The new reduction rules help us circumvent such branchings.

R-Rule 8. If there are two clauses xyC1 and xyC2 where x is an (i, 1)-literal, i ≥ 1, then replace xyC1 with xC1.

We show that our new rule is sound.

Lemma 2. R-Rule 8 is sound.

Proof. Let F1 be a formula including two clauses xyC1 and xyC2 as stipulated in R-Rule 8. Moreover, let F2 be the formula obtained from F1 by replacing xyC1 with xC1. Clearly, if an assignment satisfies at least k clauses in F2, it also satisfies at least k clauses in F1. For the other direction, because F1 and F2 differ only at xyC1 and xC1, if an assignment ρ satisfies k clauses in F1, it satisfies at least k - 1 clauses in F2. Moreover, if it satisfies exactly k - 1 clauses in F2, it must be that xC1 is unsatisfied but yxC1 is satisfied by ρ, implying that ρ(x) = 0 and ρ(y) = 1. Then, by resetting x = 1 in ρ we obtain an assignment satisfying k clauses in F2 (and also in F1).

R-Rule 9. If there is an (i, 1)-literal x such that i ≥ 2 and all clauses containing the literal x contains a literal y, then remove the literal y from all clauses including the literal x, and add the literal y in the clause including the literal x, i.e., (F1 := F ∧ xyC1 ∧ xyC2 ∧ · · · ∧ xyCi ∧ xD, k) → (F2 := F ∧ xC1 ∧ xC2 ∧ · · · ∧ xCi ∧ xyD, k).

Lemma 3. R-Rule 9 is sound.

Proof. Assume that there is an assignment ρ1 satisfying k clauses in F1. Clearly, ρ1 satisfies at least k - i - 1 clauses in F. If ρ1 satisfies at least k - i clauses in F, then resetting x = 1 in ρ1 (if ρ(x) = 1 in advance we do nothing) makes at least k clauses in F2 be satisfied; we are done. Otherwise, if ρ1 satisfies exactly k-i-1 clauses in F , then xyC1, xyC2, . . . , xyCi, and xD are all satisfied by ρ1. There can be only 3 cases (1) ρ1(D) = 1; (2) ρ1(y) = 1; (3) none of (1) and (2) and ρ1(C1) = ρ1(C2) = · · · = ρ1(Ci) = 1. In the first and second cases, we reset x = 1 in ρ1, and in the third case we reset x = 0 in ρ1. After the resetting, all the i + 1 clauses including the variable x in F2 are satisfied. The proof for the other direction is analogous.

The following two reduction rules studied in [Chen et al., 2017] are also needed in our algorithm.

R-Rule 10 ([Chen et al., 2017]). If there is an (i, 1)-literal x such that the clause xyD including the literal x contains a (j, 1)-literal y, then resolute on x, i.e.,

(F ∧ xC1 ∧ · · · ∧ xCi ∧ xyD, k) → (F ∧ yC1D ∧ · · · ∧ yCiD, k - 1).

R-Rule 11 ([Chen et al., 2017]). Let x be a (2, 1)-literal, and xC1, xC2, and xD the three clauses including the variable x. If C1C2D contains a positive literal and a negative literal of the same variable, then resolute on x, i.e., (F ∧ xC1 ∧ xC2 ∧ xD, k) → (F ∧ C1D ∧ C2D, k - 1).

We continue to propose new reduction rules to deal with (i, 1)-literals which are now based on the domination relations between literals and clauses. Let F be a CNF formula. A literal x in F is dominated by another literal y (resp. a clause C not necessarily in F) if each clause in F containing the literal x also contains the literal y (resp. some literal in C). In addition, a literal x is almost dominated by a clause D if, except at most one, all clauses in F including the literal x includes some literal in D. For instance, if F = xya ∧ xyb ∧ yc ∧ xd, then the literal x is dominated by the literal y and the clause ab, and is almost dominated by the clause ad. For a clause A = x1 · · · xi, let !A be the clause consists of all negations of literals in A, i.e., !A = x1 · · · xi.

R-Rule 12. Let x be a (2, 1)-literal, and xC1, xC2, and xD be the three clauses including the variable x. If there is some literal y in C1C2D such that the literal y is dominated by !(C1C2D), then resolute on x, i.e., (F1 := F ∧ xC1 ∧ xC2 ∧ xD, k) → (F2 := F ∧C1D∧C2D, k -1).

Lemma 4. R-Rule 12 is sound.

Proof. Let ρ be an optimal assignment satisfying at least k clauses in F1. If D = 1 under ρ, then ρ satisfies at least k-1 clauses in F2 since C1D and C2D are satisfied by ρ. Otherwise, if D = 0 but at least one of C1 and C2, say, C1, is true under ρ, then xC1 in F1 and C1D in F2 are satisfied. Then, the correctness of R-Rule 4 suggests that we can replace xC2 and xD with C2D. Finally, if C1, C2, and D are all false under ρ, we claim that the assignment obtained from ρ by resetting y = 1 is another optimal assignment. As a matter of fact, as y is dominated by !(C1C2D), any clause C ′ including the literal y contains at least one negation of some literal from C1C2D which makes C ′ = 1 under ρ. So, the claim follows and we come to the previous cases. The proof for the other direction is analogous.

R-Rule 13. Let x be a (2, 1)-literal in the clauses xC1, xC2, and xzD. If the literal z is almost dominated by !(C1C2D), then resolute on x and decrease k by one.

R-Rule 14. For a 1-literal x in a clause xzD, if the literal z is almost dominated by !D, then resolute on x and decrease k by one.

R-Rule 15. Let x be a (2, 1)-literal in the clauses xC1, xC2, and xD. If there are two literals y1 and y2 in C1C2 such that the literal y1 is dominated by some literal z and the literal y2 is dominated by the literal z, then resolute on x and decrease k by one.

Similar to the proof of Lemma 4, we can show the soundness of R-Rules 13-15.

Lemma 5. R-Rules 13-15 are sound.

Finally, our algorithm needs the following reduction rule studied in [Chen et al., 2017].

R-Rule 16 ([Chen et al., 2017]). Let x be a (2, 2)-literal in the clauses xC1, xC2, xC3, xC4. If each Ci, 1 ≤ i ≤ 4, contains a singleton literal, then resolute on x.

It should be pointed out that several of the above reductions rules may significantly increase the size of the formula. Nevertheless, thanks to a kernelization algorithm for the MAXSAT problem (see, e.g., [Chen and Kanj, 2004]), this does not diminish the applicability of these rules. In particular, due to this kernelization algorithm, once the size of the formula in an instance gets too large, we can always transform the instance into an equivalent instance whose size is bounded by O(k2 ). Then, given that all our reduction rules never increase the value of k, the above reduction rules can be exhaustively applied in polynomial time.

4 Branching Rules

In this section, we study branching rules for instances induced by all reduction rules studied in the previous section. Let the number of clauses in a CNF formula F be m. Each branching splits an instance I into several subinstances which can be recursively solved. We say that the branching is sound if it holds that I is a YES-instance if and only if at least one of the subinstances is a YES-instance. If branching on F results in r many CNF formulas which include respectively m - d1,m - d2, . . . ,m - dr clauses, we call such a branching a (d1, . . . , dr)-branching, and call (d1, . . . , dr) its branching vector. It is known that the polynomial p(x) = xm - xm-d1 - · · · - xm-dr has a unique positive root not smaller than 1, which is called the branching root of this branching. A branching is inferior to another branching if the branching root of the former is greater than that of the latter. If every branching step in a branching algorithm has its root bounded by a constant c, the running time of the algorithm can be bounded by O∗ (cm).

Now, we are ready to present the branching rules (BRules). We assume that B-Rule j is applied only when none of B-Rules i with i < j is applicable. Let F be a CNF formula reduced by the reduction rules studied in the previous section. By saying branching on a variable x, we mean the branching with x = 1 and x = 0. Clearly, any branching on a variable is sound. In each branching case, the parameter k decreases by the number of clauses satisfied in this branching. We won't point this out in the following branching rules as we analyze the running time with respect to the number of clauses. This section is divided into several subsections each of which is concerned with branching rules for variables of some specific type. We refer to Table 2 for an overview. Observe that any induced instance by R-Rules 1-3 contains only variables of degree at least three.

4.1 Branching on 6+-Variables

In this section, we present two branching rules to deal with variables of degree at least 6. A direct branching on a 7+-variable produces a (6, 1)-branching with branching root 1.2853 < 1.2989 in the worst case. However, a direct branching on a 6-variable only guaranties a (5, 1)- branching with branching root 1.3248. Hence, we need refined branching rules for 6-variables in order to improve the O∗ (1.3248m)-algorithm studied by Chen and Kanj [2004].

Lemma 6 (B-Rule 1). Branching on a 7+-variable, a (3, 3)- or (4, 2)-literal, or on a (5, 1)-singleton is not inferior to the (6, 1)-branching.

Notice that in the branching x = 1 for a (5, 1)-singleton x in B-Rule 1, in addition to the five satisfied clauses which include the literal x, the unite clause x is also reduced, leading to the total decrease of m by 6.

Lemma 7 (B-Rule 2). Let x be an (i, 1)-literal, i ≥ 3, such that the clause xD including the literal x is not unit (i.e., |D| ≥ 1). Then, the branching with x = 1 and x = D = 0 is sound and not inferior to the (i, 1 + 2|D|)-branching, which is not inferior to the (3, 3)-branching.

Proof. To prove the soundness of this rule, it suffices to show that if there is an optimal assignment under which some literal y in D is assigned the value 1, there is another optimal assignment under which x = 1. Assume that σ is an optimal assignment such that that σ(y) = 1 and σ(x) = 0. Then, due to that xD is the only clause containing x, and y = 1 already satisfies this clause, resetting x = 1 does not decrease the number of satisfied clauses.

Now we analyze the branching vector. Let D = y1y2 . . . yh where h ≥ 1. Branching with x = 1 satisfies at least i clauses. On the other hand, because the instance is reduced by R-Rule 10, each yi, 1 ≤ i ≤ h, cannot be a 1-literal. Moreover, as R-Rule 14 is not applicable, branching with x = D = 0 satisfies at least 2|D| clauses. Finally, since R-Rule 1 is not applicable, x = 0 satisfies one more clause xy1 · · · yh. Therefore, the branching is not inferior to the (i, 1 + 2|D|)-branching where i ≥ 3 and 1 + 2|D| ≥ 3.

4.2 Branching on 3-Variables

A direct branching on a 3-variable results in a (2, 1)- branching in the worst case. Bliznets and Golovnev [2012] proposed a smart resolution-involved (6, 1)-branching for 3variables. We further improve this branching significantly to a (8, 1)-branching (B-Rule 3). This improved branching is used as sub-branchings in other branching cases and hence plays an important role in improving the whole algorithm. Our improvement relies on a specific assignment for domination-related literals.

Lemma 8 ([Kulikov and Kutzkov, 2007]). If a literal y dominates another literal x, then the branching with (B1) x = 0, and (B2) x = 1 and y = 0 is sound.

Proof. From an optimal assignment ρ with ρ(x) = ρ(y)= 1, resetting ρ(x) = 0 achieves another optimal assignment since every clause including the literal x is satisfied by y which dominates x. This is covered by the branching x = 0.

Lemma 9 (B-Rule 3). Let x be a 3-variable, and xC1, xC2, and xD the three clauses including the variable x. Then the following branching is sound and leads to a branching not inferior to the (1, 3+|C1|+|C2|+2|D|)-branching, which is not inferior to the (8, 1)-branching: (B1) C1 = C2 = D = 0; (B2) resolute on x and decrease k by one.

Proof. To see the soundness of the branching rule, observe that it is safe to resolute on x if at least one of C1, C2, and D

is true. The case where C1, C2, and D are all false is covered in the branch B1.

In the branch B2, the number of clauses decreases by one. In the branch B1, we can set x = 1 and hence the three clauses including the variable x are reduced (two of them are satisfied). Moreover, due to R-Rules 3, 8-13, there are at least |C1| + |C2| + 2|D| extra clauses, each of which contains at least a negation of some literal in C1C2D, which are satisfied under this branching. Therefore, the number of clauses decreases in total by at least |C1| + |C2| + 2|D| + 3. Now we show that the branching is not inferior to the (8, 1)-branching. Since R-Rule 5 is not applicable, it holds that |C1|, |C2| ≥ 2 and hence |C1| + |C2| + 2|D| + 3 ≥ 7. However, we show that when |C1| + |C2| + 2|D| + 3 = 7, we can further reduce at least one more clause. First, the equality holds only when D = ∅, |C1| = |C2| = 2 and, moreover, every literal in C1C2 is a (j, 1)-literal for some j ≥ 1. Let C1 = y1y2 and C2 = y3y4 where every yi, 1 ≤ i ≤ 4, is a 1-literal. As the instance is reduced by R-Rules 6-7, at least one of the literals y1 and y2 is contained in a 2+-clause, say y1zD′ . As R-Rule 3 is not applicable, there exists at least one clause including the literal z. As D = ∅, the literal z cannot be any literal in !(C1C2) due to R-Rule 12; it cannot be any literal in C1C2 due to R-Rule 10. As y1 is a 1-literal, it holds that z dominates y1. Then, due to Lemma 8, we can set z = 0. Due to R-Rule 15, z cannot be in any clause containing some literal in y2y3y4. This implies that after setting z = 0 at least one more clause is reduced.

4.3 Branching on (3, 2)-Literals

Now we are left with variables of degrees 4 and 5. This section is devoted to branching rules for (3, 2)-literals.

Lemma 10 (B-Rule 4). For a (3, 2)-literal x in a reduced formula F, if there is a unit clause x or x, then branching on x is not inferior to the (4, 2)-branching.

After B-Rule 4, there is no unit clause containing a (3, 2)- or (2, 3)-literal.

Lemma 11 (B-Rule 5). Let xC be a clause where x is a (3, 2)-literal and C contains a literal occurring at most thrice in the clauses without the literal x. Then, branching on x yields a branching not inferior to the (10, 3, 3)-branching.

Lemma 12 (B-Rule 6). Let x be a (3, 2)-literal. If the two clauses with the literal x contain a (4, 1)-singleton y1 and a 5-variable y2, respectively, then branching on y2 leads to a branching not inferior to the (6, 1)-branching.

The following branching rule is for (2, 2)-literals but is used as a sub-branching in the next branching rule dealing with (3, 2)-literals.

Lemma 13 (B-Rule 7). Let x be a (2, 2)-literal such that there is a unit clause x. Let xC1 and xC2 be the two clauses including the literal x. Then the following branching is sound and leads to a branching not inferior to the (4, 2)-branching: (B1) x = 1 and C1 = C2 = 0; (B2) x = 0.

Lemma 14 (B-Rule 8). Let xy1D1 and xy2D2 be two clauses where x is a (3, 2)-literal, and each of y1 and y2 is either a (3, 2)- or a (2, 3)-literal. Then, branching on y1 leads to a branching not inferior to the (2, 4, 12)-branching.

Proof. W.l.o.g. we assume that |D1| ≤ |D2|. We distinguish between two cases: (1) |D2| ≥ 1 and (2) |D2| = |D1| = 0.

In the first case, in the branching y1 = 0, at least two clauses including the literal y1 are reduced. In the branching y1 = 1, all clauses including the literal y1 is reduced, and x becomes an (i, 1)-non-singleton for some i ∈ {1, 2, 3}. If i = 1, y1 is a (3, 2)-literal. Moreover, R-Rule 2 applies, leading to one more clause being reduced. In this case, we have a (2, 4)-branching. If i = 2, then B-Rule 3 is invoked (in the worst case), leading to at least a (1, 9)-subbranching (recall that |D2| ≥ 1 and due to B-Rule 4 any clause including the literal x is of size at least two). In this case, we have a (2, 4, 12)-branching if y1 is a (3, 2)-literal and a (3, 3, 11)- branching if y1 is a (2, 3)-literal. Finally, if i = 3, B-Rule 2 applies, generating at least a (3, 5)-subbranching. In this case, we have a (2, 6, 8)-branching if y1 is a (3, 2)-literal and a (3, 5, 7)-branching if y1 is a (2, 3)-branching. All the above branchings are not inferior to the (2, 4, 12)-branching.

Now we consider the second case. If y1 = 0, xy1 becomes a unit clause and x becomes a (2, 0)-, (2, 1)-, (2, 2)-, or (2, 3)-literal. In the first and second cases, R-Rule 3 is applicable; in the third case, B-Rule 7 is applicable; and in the last case, B-Rule 4 is applicable. All of these cases lead to at least a (4, 2)-subbranching. In the branching y1 = 1, x becomes a (i, 1)-non-singleton where i ∈ {1, 2, 3}. If i = 1, R-Rule 3 applies. If i = 2, either some reduction rules apply or B-Rule 3 applies and a (1, 9)-subbranching is generated. Finally, if i = 3, then either some reduction rules apply or B-Rule 2 applies and a (3, 5)-subbranchings is generated. In the worst case, we have a (4, 6, 4, 12)-branching.

Since the (4, 6, 4, 12)-branching is not inferior to the (2, 4, 12)-branching, the lemma follows.

4.4 Branching on (2, 2)-Literals: theWorst Case

Now, assume that only (4, 1)- and (3, 1)-singletons, and (2, 2)-literals exist in the reduced formula. We present numerous branching rules to eliminate (2, 2)-literals.

Lemma 15 (B-Rule 9). Let x be a (2, 2)-literal. If there is a clause xy1C such that y1 is a (4, 1)-singleton, and the other clause containing the literal x contains another singleton, then branching on y1 leads to a branching not inferior to the (6, 1)-branching.

Proof. In the branching y1 = 0, the clause including y1 is satisfied. In the branching y1 = 1, four clauses including the literal y1 are satisfied and the unsatisfied unit clause y1 is reduced. Moreover, when y1 = 1, x becomes a 1- or 0literal, invoking the application of at least one of R-Rules 2, 3, and 10, further decreasing the number of clauses by one. Therefore, the number of clauses decreases by 6 in total.

Lemma 16 (B-Rule 10). Let x be a (2, 2)-literal. If the two clauses including the literal x contain a singleton y1 and a (2, 2)-literal y2, respectively, then, branching on y2 leads to a branching not inferior to the (10, 3, 3)-branching.

Observe that after the above branching rules, there are no clauses including both a (2, 2)-literal and a (4, 1)-singleton.

In other words, any clause including a (2, 2)-literal can contain only other (2, 2)-literals or (3, 1)-singletons. Moreover, due to R-Rule 16 and B-Rule 7, for each (2, 2)- literal x in clauses xC1, xC2, xD1, xD2, it holds that (1) |C1|, |C2|, |D1|, |D2| ≥ 1, and (2) at least one of C1, C2, D1, and D2 contains only (2, 2)-literals. Therefore, all (2, 2)- literals x as denoted above fall into one of the following categories: either C1C2D1D2 contains only (2, 2)-literals, or C1C2 (resp. D1D2) contains only (2, 2)-literals and D1D2 (resp. C1C2) contains only (3, 1)-singletons. The next two branching rules are to eliminate literals of the second type.

Lemma 17 (B-Rule 11). Let xC be a clause such that x is a (2, 2)-literal, 1 ≤ |C| ≤ 3, and C contains only singletons. Then, branching on x leads to a branching not inferior to the (10, 3, 3)-branching.

After B-Rule 11, if a clause xC contains a (2, 2)-literal x and C contains only singletons, it must be that |C| ≥ 4.

Lemma 18 (B-Rule 12). Let x be a (2, 2)-literal, and xC1, xC2, xyD1, xD2 the clauses including the variable x. If C1C2 contains only singletons, then branching on y leads to a branching not inferior to the (15, 11, 3, 3)-branching.

Now, all (2, 2)-literals are of the first type, i.e., every clause including a (2, 2)-literal contains only (2, 2)-literals.

Lemma 19 (B-Rule 13). Let x be a (2, 2)-literal, and xy1C1 and xy2C2 the two clauses including the literal x. If y1 and y2 are the literals of the same variable (i.e., y1 = y2 or y1 = y2), or there is another clause y1y2C3, then branching on x leads to a branching not inferior to the (10, 3, 3)- branching.

Lemma 20 (B-Rule 14). Let xy and xzC1 be two clauses such that x is a (2, 2)-literal. Then, branching on z leads to a branching not inferior to the (10, 3, 3)-branching.

The last branching rule can be used to eliminate all the remaining (2, 2)-literals.

Lemma 21 (B-Rule 15). For clauses xy1C1, xy2C2, y1D1, and y2D2 where x is a (2, 2)-literal, the following branching is sound and leads to a branching not inferior to the (14, 14, 12, 12, 7, 7, 5, 5)-branching:

• B1. x = 1 and y1 = 0;
• B2. x = y1 = 1 and D1 = 0;
• B3. x = 0 and y2 = 0;
• B4. x =D2 = 0 and y2 = 1.

4.5 Dealing with Singletons and Our Main Result

If none of the reduction rules and branching rules is applicable, then we are left with only (3, 1)- and (4, 1)-singletons. A branching algorithm handling this special case has been studied in the literature, as shown in the following lemma.

Lemma 22 ([Bliznets and Golovnev, 2012]). The MAXSAT problem on formulas with only (3, 1)- and (4, 1)-singletons can be solved in time O∗ (1.2576m).

Now we are able to show our main result, i.e., an exact algorithm of running time O∗ (1.2989m) for the MAXSAT problem. The algorithm applies the branching rules in the order in accordance with their occurrences, and importantly, before each branching we exhaustively apply all reduction rules presented in the previous section. As pointed out in the end of Section 3, it takes polynomial time to exhaustively apply all reduction rules. If none of the branching rules applies, we are left with (3, 1)- and (4, 1)-singletons, and in this case we solve the instance in O∗ (1.2576m) time (Lemma 22). The running time of the whole algorithm is dominated by the branching described in Lemma 21, which has the worst branching root 1.2989 (see Table 2 for a reference).

Theorem 1. The MAXSAT problem can be solved in time O∗ (1.2989m).

5 Concluding Remarks

In this paper, we have proposed an exact branch-and-bound algorithm for the MAXSAT problem whose running time is bounded by O∗ (1.2989m), where m is the number of clauses. Our algorithm considerably improves the previous best result O∗ (1.3248m) published 15 years ago [Chen and Kanj, 2004]. To this end, we put forward many new reduction rules to shrink the size of the given CNF formula in polynomial time. In addition, based on these reduction rules and refined observations, we derived improved branching strategies for variables of degrees 3-5.

It is important to point out that our analysis is purely worst-case based. The performance of our reduction and branching rules in solving practical instances deserves to be further investigated. In fact, the cores of many competitive exact MAXSAT solvers are branch-and-bound procedures (see, e.g., [Davis et al., 1962; Argelich et al., 2018; Abram´e and Habet, 2015; Lin et al., 2008]). Some research even reveals that in some cases branch-and-bound algorithms are the best option [Morgado et al., 2013]. In addition, it makes much sense to study how to efficiently integrate our reduction and branching rules into heuristic algorithms. To employ our branching rules, one may need to resort to powerful pruning approaches, such as approaches based on the phase transition [Coppersmith et al., 2004], or using machine learning algorithms to determine the pruning conditions, which have proved to be useful in solving a variety of problems (see, e.g., [He et al., 2014]). We refer to [Morgado et al., 2013] and references therein for discussions on many other nice ideas of designing (exact or heuristic) branch-and-bound based MaxSAT algorithms.

Acknowledgements

This work was supported by the National Natural Science Foundation of China (Nos. 61420106009, 61872097, 61672536, 61802441, 61872048, 61872450, 61828205, 61702557), 111 Project (No. B18059), Hunan Provincial Science and Technology Program (No. 2018wk4001), and the China Postdoctoral Science Foundation (No. 2017M612584).