An Exact MaxSAT Algorithm: Further Observations and Further Improvements

1 Introduction

The satisfiability problem (SAT) as the first proved NPcomplete problem [Cook, 1971] is one of the most influential problems in computational complexity. Due to the large applications in engineering, artificial intelligence, and many other areas [Garey and Johnson, 1979], this problem and many variants have been extensively studied in the literature. Many practical solvers for these problems have been developed [Hutter et al., 2017; Cai et al., 2017]. Most of these algorithms are heuristic-based and can not solve all instances quickly due to the hardness of the problems. So diverse approaches have been investigated on these problems, including randomized, approximation, exact, parameterized algorithms, etc.

In exact and parameterized algorithms, we aim to find fast exponential algorithms that can optimally solve the problems. These running time bounds may be helpful for us to understand the computational complexity of NP-complete problems and the limitation to solving NP-complete problems. In practice, with the rapid development of hardware and computer techniques, many fast exact algorithms can be implemented to solve middle-size instances within an acceptable time. The most important thing is that many techniques and principles behind exact algorithms can be used to improve heuristic solvers. The reduction rules were used as the preprocessing procedures to simplify the input instance without losing the optimality and some branching rules were used to deal with some dense local structures [Xiao et al., 2021].

All of the above motivates us to follow the hard research line of studying exact algorithms for important NP-complete problems with theoretical running time bounds. It is worth mentioning that for SAT and related problems, several running time bounds of decades ago were improved during the last two years [Chu et al., 2021; Alferov and Bliznets, 2021; Peng and Xiao, 2021; Xu et al., 2019].

In this paper, we will study exact algorithms for the maximum satisfiability problem (MaxSAT). In a CNF-formula, we are given n Boolean variables and m clauses on the variables. SAT asks whether we can give an assignment of the variables to satisfy all the clauses. MaxSAT asks us to satisfy the maximum number of clauses. We consider the decision version of MaxSAT: whether we can satisfy at least k clauses for k being part of the input. Clearly, MaxSAT is more general compared to the original SAT problem. MaxSAT has significant applications and has been extensively studied in theory and application [Morgado et al., 2013; Bonet et al., 2007; Li et al., 2016]. For more progresses in MaxSAT, please see recent surveys [Li and Many`a, 2021; Bacchus et al., 2021].

To exact solve SAT or MaxSAT, the trivial algorithm to check all possible assignments has the running time bound O∗ (2n ). However, no algorithm with running time bound O∗ (cn ) for constant c < 2 was found after decades of hard research, and the Strong Exponential Time Hypothesis (SETH) [Impagliazzo and Paturi, 2001] assumes that this kind of algorithm does not exist. So we turn to consider another natural measure - the number of clauses m. The running time bound under this measure can be significantly improved. The lines of research that attempt to solve SAT and MaxSAT in terms of m are shown in Tables 1 and 2. Previously, SAT and MaxSAT can be solved in O∗ (1.2226m) and O∗ (1.2989m) time, respectively. In this paper, we further improve the running time bound for MaxSAT to O∗ (1.2886m). We also mention another frequently used measure L, which is the total length of all clauses. In terms of L, very recently, the running time bounds for SAT and MaxSAT were improved to O∗ (1.0646L) [Peng and Xiao, 2021] and O∗ (1.0927L) [Alferov and Bliznets, 2021], respectively.

Most previous algorithms are branch-and-search algorithms that will search for a solution by letting a variable (or a literal) be 1 or 0. For an (a, b)-literal x (x appears in a clauses and x appears in b clauses), the simple branch will decrease the number of clauses by a and b, respectively, in the two subbranches. When a+b is large, the numbers of clauses decrease greatly and we may be able to get a good complexity. So the bottleneck will happen when all the variables have a low degree. On the other hand, when the degree of a variable is at most 2, we can reduce the instance directly. For variables of degree 3, we may also have fast branching rules to deal with them. So usually the bottleneck cases are to deal with variables of degree 4 or 5. Chen and Kanj [2004] showed that their worst case was to branch on (3, 2)-literals and then got the running time bound O∗ (1.3248m). Xu et al. [2019] showed that the previous bottleneck would not always happen and improved the bound to O∗ (1.2989m). Their worst case is to deal with some (2, 2)-literals, which needs to consider many cases and combine several following subbranches. The bottleneck branching vector is (14, 14, 12, 12, 7, 7, 5, 5) that contains eight subbranches. In this paper, we avoid the previous bottleneck of dealing with (2, 2)-literals by using new reduction rules and deep analysis. Our bottleneck comes back to deal with (3, 2)-literals. We get the following neat result that for the worst case: after branch on a (3, 2)-literal, we can branch with (3, 3) at least in each subbranch. Thus, our worst branching case is (6, 6, 5, 5), the corresponding complexity (branching factor) is 1.2886.

Our algorithm uses several reduction rules and techniques developed in previous papers. Compared to the work in [Chen and Kanj, 2004], we further show that after their bottleneck we always have good branchings. Compared to the work in [Xu et al., 2019], our branching complexity to deal with (2, 2)-literals and (3, 2)-literals are improved to 1.2872 and 1.2886, respectively, while their results were 1.2989 and 1.2937.

2 Preliminaries

For a Boolean variable x, a literal is either x or the negation of it. We use x (resp., C for a set of literals C) to denote the negation of a literal x (resp., the set of negations of literals in C). Thus, we have x = x. A clause is a set of literals and it is satisfied if there is at least one literal that is assigned 1. Given a set V of n Boolean variables, a CNF formula F is given by a set of m clauses on V . The MaxSAT problem asks whether there is an assignment on the Boolean variables to satisfy at least k clauses, where k is also a part of the input. AMaxSAT instance is denoted by a pair (F, k).

For two sets of literals C1 and C2, we may simply use C1C2 to denote the union of them. A set of a single element {x} may be simply written as x. For a set C of literals, C = 1 (resp., C = 0) means to assign 1 (resp., 0) to each literal in C, FC=1 means to delete all clauses containing a literal in C and delete literals in C from all clauses in F, and FC=0 = FC=1 . Sometimes, we may simply use C = 1 and C = 0 to denote FC=1 and FC=0, respectively.

If a literal appears in a clauses in F, then it is called an a-literal and its degree is a. The degree of a variable x is the degree of the literal x plus the degree of the literal x. A variable of degree a is also called an a-variable. If the degree of x is a (resp., at least a or at most a) and the degree of x is b, we say x is an (a, b)-literal (resp., an (a+, b)-literal or an (a-, b)-literal). Similarly, we can define (a, b+)-literals, (a, b-)-literals, (a+, b+)-literals, (a-, b-)-literals and so on. A literal x is an (a, b)-literal if and only if x is a (b, a)- literal. A clause containing c literals is called a c-clause and its length is c. A clause of length 1 is called a unit clause. An (i, 1)-literal x is called a singleton if the unique clause containing x is a unit clause and non-singleton otherwise.

Resolution [Robinson, 1965] is a frequently used technique in SAT problems. Resolution on a variable x in F, denoted by F\x, is the operation that for each pair of clauses xC and xD in F, generate a new clause CD, and then remove all original clauses containing x or x.

2.1 Framework of Branching Algorithms

We introduce the framework of our branching algorithm. It will first apply reduction rules to reduce the instance and then apply branching rules to search for a solution when the instance can not be further reduced.

A reduction rule will transfer an instance I = (F, k) to an equivalent instance I ′ = (F ′ , k′ ) in polynomial time, where I is yes if and only if I ′ is yes. We will use (F, k) → (F ′ , k′ ) to denote the reduction. Usually, the resulting instance I ′ has a smaller number of variables or clauses or k′ < k. Reduction rules can simplify the input instance without exponentially increasing the running time bound. So they are frequently used as preprocessing in many algorithms. We will use some known reduction rules and also introduce some new rules.

When the instance can not be reduced any more, we will branch. The branching operation will generate a search tree and the size of the tree is related to the exponential part of the running time. We use T(m) to denote the maximum size of the search tree on any instance with at most m clauses. In a branching operation, if it generates l sub-branches with mi < m clauses in the ith sub-branch, then we get a recurrence relation

Let ai = m-mi. The above recurrence is represented by a branching vector (a1, a2, . . . , al). The largest root of the function f(x) = 1 - ∑li=1 x-ai is called the branching factor of the recurrence. If the maximum branching factor for all branching operations in the algorithm is at most γ, then T(m) = O(γm). See [Fomin and Kratsch, 2010] for more details about analyzing branching algorithms. So we want to minimize the biggest branching factor in the algorithm. We will say a branching vector is not worse than another one if the corresponding branching factor is not greater than that of the latter.

3 Reduction Rules

We first present the reduction rules.

• R-Rule 1. (F ′ ∧ xxC, k) → (F ′ , k -1).

R-Rule 2. ([Bansal and Raman, 1999]) For a (1, 1)-literal x containing in two clause xC and xD, let (F ′ ∧ xC ∧ xD, k) → (F ∧ CD, k - 1).

Another easy case is to deal (i, 0)-literal x. We only need to let x = 1. This case is included in the following rule as a special case.

• R-Rule 3. ([Chen and Kanj, 2004]) For an (i, j)-literal x in F, if there are at least j unit clauses x, then (F, k) → (Fx=1, k - i).

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

• R-Rule 5. ([Bliznets and Golovnev, 2012]) If there is a 2clause xy containing a (2, 1)-literal x, then (F ′ ∧ xy ∧ xC ∧ xD, k) → (F ′ ∧ yD ∧ yCD, k - 1).

R-Rule 6. ([Chen et al., 2017]) If there is an (i, 1)-literal x such that the unit clause containing x also contains a (j, 1)- literal y, then (F ′ ∧ xC1 ∧ · · · ∧ xCi ∧ xyD, k) → (F ′ ∧ yC1D ∧ · · · ∧ yCiD, k - 1).

In F, a literal x dominates another literal y if each clause containing y also contains x. We give the following new reduction rules.

R-Rule 7. If there are two literals x and y such that x dominates y and y dominates x, then replace y with x (and also y with x) in F.

• R-Rule 8. If there are two literals x and y such that x dominates y and there is a clause C containing both of x and y, then delete the clause C and decrease k by 1.

R-Rule 9. If there is a (2, 2)-literal x such that the two clauses containing x contain the same singleton, then resolute on x, i.e., (F, k) → (F\x, k).

The correctness of this rule is based on the following observation. Let S = {xC1, xC2, xyD1, xyD2} be the four clauses containing x or x, where y is a singleton. In F\x, S is replaced with S′ = {C1yD1,C1yD2,C2yD1,C2yD2}. For any optimal solution f to F, at most one clause in S ∪ {y} is not satisfied. If all of them are satisfied, then y = 0 and either C1 = C2 = 1 or D1 = D2 = 1 under f. For this case, all clauses in S′ ∪{y} are also satisfied under f. If one clause in S ∪ {y} is not satisfied under f, we can always assume that it is y (thus, x = y = 1). For this case, only one clause y in S′ ∪ {y} is not satisfied under f.

For any optimal solution f ′ to F\x, also at most one clause in S′ ∪ {y} is not satisfied. If all of them are satisfied, then y = 0 and either C1 = C2 = 1 or D1 = D2 = 1 under f ′ . For this case, all clauses in S ∪{y} are also satisfied under f ′

and x = 1 for D1 = D2 = 1 and x = 0 for C1 = C2 = 1. If one clause in S′ ∪ {y} is not satisfied under f ′ , then we can always assume that it is y (thus, y = 1). For this case, only one clause y in S ∪ {y} is not satisfied under f ′ and x = 1.

Definition 1. A formula is reduced if none of the above reduction rules can be applied to the formula.

Lemma 1. Applying any reduction rule will not increase the number of clauses, and for any input formula, it takes polynomial time to apply the reduction rules to transfer it to a reduced one.

4 Branching Operations

When no reduction rule can be applied to the formula, we will apply our branching rules. We have seven branching steps, each of which is going to deal with some type of literals. First of all, we give the overview of the branching vectors and branching factors of all steps in Table 3.

4.1 Three Special Cases

Before giving the detailed branching steps, we first analyze three special cases that will lead to good branching vectors. These three cases will frequently appear in some subbranches after a bad branching in our algorithm. So when we meet a bad branching, we may be able to combine it with the following good branchings to get an improved branching. These special cases are to deal with (i, 1)-no-singletons, 3-variables, and literals appearing in many unit clauses. The first two special cases were deeply studied in the previous paper by Xu et al. [2019]. Note that in these lemmas, we do not require the formula to be reduced.

Lemma 2. ([Xu et al., 2019]) Let F be an arbitrary formula, x be an (i, 1)-literal, i > 0, in F, and ¯xD be the unique clause containing ¯x. We can either (i) reduce at least one clause by applying reduction rules, or (ii) safely branch with x = 1 and xD = 0 and get a branching vector covered by (i, 1 + 2|D|). If x is (i, 1)-no-singleton with i ≥ 3, then the branching vector is at least (3, 3).

Lemma 2 can be used to deal (i, 1)-no-singletons. The next lemma will be used to deal with 3-variables.

Lemma 3. ([Xu et al., 2019]) Let F be an arbitrary formula containing a 3-variable x, where xC1, xC2 and ¯xD are the three clauses containing the variable x. We can either (i) reduce the number of clauses by at least 1 by applying reduction rules, or (ii) safely branch with (B1) C1C2D = 0 and (B2) F\x and k decreases by 1, and get a branching vector covered by (τ, 1), where τ = max{8, 7 + 2|D|}.

Lemma 3 can be obtained from Lemma 9 in [Xu et al., 2019]. We slightly refine the form of the result. Note that if |C1| < 2 or |C2| < 2, we can directly reduce one clause by applying R-Rule 3 or 5. So we can get the branching vector (7 + 2|D|, 1).

Remark: To obtain Lemmas 2 and 3, we may need to use more reduction rules that are omitted here. We present the two lemmas by citing the references and the absence of these reduction rules do not affect other parts but may improve the readability of the paper.

We also deeply analyze another structure where literals appear in many unit clauses. R-Rule 3 shows that if an (i, j)- literal x appears in at least j unit clauses x, then we can reduce the instance directly. Here we show that we can get a good branch if the condition relaxes a little.

Lemma 4. Let x be an (i, j)-literal appearing in exactly j-1 unit clauses x, where i ≥ j ≥ 2. Let the i+j clauses containing x and x be x, . . . , x, xC1, . . . , xCi-j+1, xD1, . . . , xDj . We can either (i) reduce the number of clauses by at least 1, or (ii) safely branch with (B1) x = 1 and (B2) x = D1 = · · · = Dj = 0, and get a branching vector not worse than (i, 2j + 1).

The proof is omitted here due to the limited space.

Next, we are going to describe our branching steps. When we introduce one, we assume that the current instance is a reduced instance and previous steps can not be applied.

4.2 Step 1: 6+-Variables

We show that if the formula contains a 6+-variable x, we can always branch with a branching vector not worse than (6, 1). Directly branching on a 7+-variable or a (3, 3)-literal or a (4, 2)-literal will result in a branching vector not worse than (6, 1). Branching on a (5, 1)-singleton x will also lead to a branching vector (6, 1). Because in the branching x = 1, the five clauses containing x will be satisfied and reduced, and the unit clause x is also reduced. So the number of clauses decreases by 6 at least in this branching. For (5, 1)-nosingletons, we will deal with them in the next step.

4.3 Step 2: (i, 1)-Non-Singletons With i ≥ 3

We simply use the branching rule in Lemma 2, which will generate a branching vector (i ≥ 3, 1 + 2|D|). Since the variable is not a singleton, we have that |D| ≥ 1 and then the branching vector is not worse than (3, 3).

Note that (i, 1)-literals with i ≤ 1 will be reduced by RRule 2 or R-Rule 3. For (2, 1)-literals, we will deal with them in the next step.

4.4 Step 3: 3-Variables

Assume there is a 3-variable x with three clauses xC1, xC2 and xD. The instance is reduced and R-Rules 3 and 5 can not be applied. So we know that |C1|, |C2| ≥ 2. We use the branching rule in Lemma 3. Then we can branch with (8, 1) at least when D = ∅ and (9, 1) at least when D ̸= ∅.

4.5 Step 4: Literals Appearing inMany Unit Clauses

If there is an (i, j ≥ 2)-literal x that appears in at least j-1 unit clauses x, we directly use the rule in Lemma 4 to decrease the number of clauses or branch with (5, 2) at least.

This step will deal with (2, 2)/(3, 2)-literals x containing in one unit clause. If x is a (2, 2)-literal, the branching vector is at least (2, 5). If x is a (3, 2)-literal, the branching vector is at least (3, 5).

4.6 Step 5: (3, 2)-Literals

In this step, we dealing with (3, 2)-literals. Now the formula only contains (3, 2)/(2, 3)/(2, 2)-literals and (4, 1)/(3, 1)- singletons. Let x be a (3, 2)-literal with five clauses xC1, xC2, xC3, xD1, and xD2. Note that none of C1, C2, and C3 can be empty since this case will be handled in Step 4.

Step 5.1: There is a unit clause x. For this case, we can branch on x with a branching vector not worse than (4, 2).

Note that no matter whether x = 1 or 0, all unit clauses x will be reduced in both subbranches. We can directly get a branching vector (3, 2) by branching on x. In the branching x = 1, we can further reduce one unit clause x and get a branching vector (4, 2).

Next we assume that none of C1,C2,C3,D1 and D2 is empty.

Step 5.2: D1 or D2 contains a (2,2)-literal y. We show that we can branch with a branching vector not worse than (11, 3, 3).

We branch on x. First, we look at the branching x = 0. After deleting the two clauses containing x, if y becomes a (0, 1)/(0,2)/(1,1)-literal, we can reduce one more clause by applying R-Rules 2-3 on y. For this case, we get a branching vector (3, 3). Otherwise y will become a (1,2)-literal. Let yE be the clause containing y. If E is not empty, then By Lemma 3 (with |D| ≥ 1), we can either further reduce one clause by reductions or further branch with a branching vector (1,9) at least. Thus, we can get a branching vector (3, 2 + 1, 2 + 9) = (3, 3, 11) at least. If E becomes empty, then we know that E = x (it is impossible that before branching the clause containing y is a unit clause, otherwise Step 4 would be applied on y). For this case, in each branching of x = 0 and x = 1, y will become a variable of degree at most 3. We can either reduce the number of clauses by one or branch with (1, 8) at least by Lemma 3. So we can branch with (3 + 1, 3 + 8, 2 + 1, 2 + 8) = (4, 11, 3, 10) at least.

Step 5.3: One of D1 and D2 contains a 5-variable and the other contains a singleton. We show that we can branch with a branching vector not worse than (6, 1).

Without loss of generality, we assume that D1 contains a singleton y1 and D2 contains an (i1, i2)-literal y2, where i1 +

i2 = 5. Since R-Rule 3 and Step 5.2 can not be applied now, we have that i1 ≥ 2 and i2 ≥ 1. If y2 = y1, then we branch on x. In the branching x = 0, we can further reduce at least one clause by applying R-Rule 3 on y1. Thus, we can always get (3, 3) for this case. Next, we assume that y1 ̸= y2. We will branch on y2. In the branching y2 = 0, we reduce i2 clauses containing y2 directly. In the branching y2 = 1, we first reduce i1 clauses containing y2. After deleting the i1 clauses, if x becomes a (0,1) or (i > 0,0)-literal, then we can further reduce at least one clause by applying R-Rule 3. Otherwise x becomes an (i > 0,1)-literal. Since y1 ̸= y2, we know that y1 is a singleton still left in the clause containing x. Thus, the condition of R-Rule 6 holds and we can further reduce one clause by applying R-Rule 6. So we can always branching with a branching vector (i1 + 1, i2). If i1 = 2 or 3, the branching vector is (3, 3) or (4, 2). Next we consider i1 = 4. Now y2 is a singleton since Step 2 could be applied on y2 now. Then in the branching y2 = 0, we can further reduce the unit clause y2. Thus, we can indeed get (6, 1).

Step 5.4: D1 and D2 contain only 5-variables. We show that we can branch with (6, 6, 5, 5) at least.

A (3,2)-literal x′ is called good if a variable of degree at most 3 or an (i, 1)-literal is created after deleting the three clauses containing x′ . In this step, we select x as a good (3,2)-literal if this kind of literals exists.

Assume that y1 ∈ D1 and y2 ∈ D2 are 5-variables. If D1 = y1 and D2 = y2, then R-Rule 4 would be applied. So D1 or D2 must contain another 5-variable and then we can assume that y1 ̸= y2. Furthermore, y1 and y2 can only be (2, 3)- and (3, 2)-literals.

Case 1: x is not good. According to the choice of x, we know that all (3, 2)-literals are not good. Now y1 and y2 are (2, 3)-literals since if they were (3, 2)-literals they would be good. We also know that y1 and y2 are not in C1C2C3, otherwise x would be good. If D2 contains y1 or y1, we branch on x. In the branching x = 0, y1 will become a 3-variable and the clause containing y1 has length at least 2 otherwise Step 5.1 would be applied before this step. So we can further reduce one clause or branch on y1 with at least (1, 9) by Lemma 3 (with |D| ≥ 1). Thus, we can branch with (3, 2 + 1, 2 + 9) = (3, 3, 11) at least. It is the same of the case that D1 contains y2 or y2.

Next we further assume that y1, y1 ̸∈ D2 and y2, y2 ̸∈ D1. We branch on y1. In Fy1=1, x is a (3,1)-lateral and y2 is a variable of degree at least 4 by the above assumptions. If y2 is a (1,3)/(2,3)-literal, we further branch with (B1) x = 1 and (B2) x = y2 = 0, which create a branching vector (3, 4). In total, we get a branching vector not worse than (2 + 3, 2 + 4, 3) = (5, 6, 3). Else y2 is a (2,2)-literal, we further branch on y2. In the branching y2 = 1, we can further reduce the three clauses containing x (which do not contain y2 by the above assumptions). So we can get branching vector (5, 2) at least. In total, we get a branching vector not worse than (2 + 5, 2 + 2, 3) = (7, 4, 3).

Case 2: x is good. We say x is excellent if a variable of degree at most 3 or an (i, 1)-literal is created after deleting the two clauses containing x. We first consider the case that x is excellent. For this case, we branch on x. In each subbranch, we can either reduce one more clause or branch with either (3,3) by Lemma 2 or (1,8) by Lemma 3. The worst case is to branch with (3,3) in both subbranches. Thus, we can always branch with (2 + 3, 2 + 3, 3 + 3, 3 + 3) = (5, 5, 6, 6) at least.

Next we assume that x is not excellent. Now Both of y1 and y2 are (3, 2)-literals, y1, y1 ̸∈ D2, and y2, y2 ̸∈ D1, otherwise x would be excellent. We further distinguish two cases.

Case 2.1: one of |D1| and |D2|, say |D1| is one, i.e., y1 = D1. We branch on y1. In the branching y1 = 1, x will become a (1, i ≤ 3)-literal. We can either reduce one more clause or branch with either (3,3) by Lemma 2 or (1,8) by Lemma 3. In the branching y1 = 0, x becomes a (2, i)-literal with one unit clause x. By Lemma 4, we can either further reduce one clause or branch with (2, 5) at least. In the worst case, we can branch with (3 + 3, 3 + 3, 2 + 2, 2 + 5) = (6, 6, 4, 7) at least. Case 2.2: |D1|, |D2| ≥ 2. We branch on y1. In the branching y1 = 1, x will become a (1, i ≤ 3)-literal with the clause xD2 containing x unchanged. If x is a (1, i ≤ 1)-literal, then we can reduce one more clause directly by applying RReductions 1 or 2. If x is a (1, 2)-literal, then we can branch with at least (1, 11) by Lemma 3 (with |D| ≥ 2). If x is a (1, 3)-literal, then we can branch with at least (3, 5) by Lemma 2 (with |D| ≥ 2). In the worst case, we can branch with (3 + 1, 3 + 11, 2) = (4, 14, 2) at least.

Step 5.5: D1 and D2 contain only (3,1)-singletons. We will get a branching vector not worse than (11, 10, 4, 3).

None of D1 and D2 is empty now, and D1 and D2 can not contain the same singleton otherwise R-Rule 9 would be applied. We assume that y1 ∈ D1 and y2 ∈ D2 are two different (3,1)-singletons. We will first branch on x. In the branching x = 1, we reduce three clauses. In the branching x = 0, the two clauses containing x will be removed and both of y1 and y2 become (2,1)-singletons. Then, we can reduce one clause directly or branch on y1 with (1,8) at least by Lemma 3. Note that in the first branch of (1, 8) it is to resolute the (2,1)-singleton y2, which will not change the degree of any other literals. So y2 will still be left as a (2,1)-singleton. So we can further reduce one clause directly or branch on y2 with (1,8) at least by Lemma 3. For the worst case, we can branch with (3, 3 + 1, 3 + 8, 10) = (3, 4, 11, 10).

4.7 Step 6: DealingWith (2, 2)-Literals

After Step 5, there are only (2,2)-literals, (3, 1)-singletons, and (4, 1)-singletons. Let x be a (2, 2)-literal with the four clauses xC1, xC2, xD1, and xD2. None of C1,C2,D1, and D2 is empty, otherwise there would be a unit clause containing a (2,2)-literal, and Step 4 could be applied.

Step 6.1: D1 and D2 contain the same literal. Assume that D1 and D2 contain the same literal y. We can branch on x with a branching vector not worse than (4, 2).

Note that y can not be a (3, 1)/(4, 1)-singleton, otherwise R-Rule 9 could be applied. So y is a (2, 2)-literal. Furthermore, literal y is not in C1 or C2 otherwise R-Rules 7 or 8 would be applied. In the branching x = 1, we reduce two clauses. In the branching x = 0, we can reduce four clauses containing x or y. We can branch with (2, 4) at least.

Step 6.2: each of D1 and D2 contains a singleton and at least one is a (4, 1)-singleton. Assume that y1 ∈ D1 is a

(4,1)-singleton and y2 ∈ D2 is a singleton. We can branch on y1 with a branching vector not worse than (6, 1).

In the branching y1 = 1, four clauses containing y1 and the unit clause y are reduced. Furthermore, x becomes a (2,1)- literal with singleton y2 in the clause containing x. We can further reduce one clause by applying R-Rule 6. Thus, we can get a branching vector (6, 1) at least.

The proofs of the following two properties were omitted due to the limited space.

Property 1. If D1D2 (resp.,C1C2) contains only (3, 1)- singletons, then in the branching x = 0 (reps., x = 1), we can branch with (18, 11, 11, 4) at least.

Property 2. If D1D2 (resp.,C1C2) contains a (2,2)-literal, then in the branching x = 0 (reps., x = 1) we can branch with (11, 3) or (11, 10, 4) at least.

It seems that we can use Properties 1 and 2 to handle the remaining cases. However, direct application of them can not get a good enough branching rule. For example, we branch on x, and in each branching, we get a branching vector (11, 3). Then we can only get (11, 11, 3, 3), which has a branching factor 1.3 > 1.2886. So we still consider the following two cases.

Step 6.3: D1 contains a (2, 2)-literal y1 and D2 contains a singleton y2. We show that we can branch with a branching vector not worse than (11, 3, 3).

We branch on the (2, 2)-literal y1. In the branching y1 = 1, we first reduce the two clauses containing y1. After this, x will become a (2,1)-literal such that the clause containing x also contains a singleton y2 and we can further reduce at least one clause by applying R-Rule 6. So m decreases by at least 3 in this branching. In the branching y1 = 0, we can branch with either (11, 3) or (11, 10, 4) or (18, 11, 11, 4) by Properties 1 and 2. For the worst case, we can branch with (11, 3, 3) for this step.

By the symmetry, Step 6.3 will also deal with the case that one of C1 and C2 contains a (2, 2)-literal and the other contains a singleton.

Step 6.4: There still exists a (2, 2)-literal x. For this case, we can branch with (18, 18, 11, 11, 11, 11, 4, 4) at least.

We branch on the (2, 2)-literal x. We analyze the branching x = 0. Assume there is a (2, 2)-literal y1 ∈ D1. Since Step 6.3 is not applicable now, we know that there is another (2, 2)-literal y2 ∈ D2. Both of y1 and y2 will become 3variables after assigning x = 0, where literal y1 is a (1,2)- literal such that the clause containing y has length at least 2 otherwise R-Rule 4 would be applied before assigning x = 0. By Lemma 3 with |D| ≥ 1, we can branch on y1 with (9, 1) first, and in the branching F\y1 , we still can branch on 3variable y2 with (8, 1) at least. So we get the branching vector (2 + 9, 2 + 1 + 8, 2 + 1 + 1) = (11, 11, 4). Next we can assume that none of D1 and D2 contains (2, 2)-literals. By Property 1, we can branch with (18, 11, 11, 4) at least. So we can always branch with (18, 11, 11, 4) at least. For the branching x = 1, we can get the same result by symmetry. So we can always branch with (18, 18, 11, 11, 11, 11, 4, 4).

4.8 Step 7: Only (3, 1)/(4, 1)-Singletons

This case can be reduced to a set cover problem. Assume in the MaxSAT instance, there are m clauses and n (i, 1)- singletons x (i = 3, 4). Besides the n clauses x, all the other m- n clauses are considered as the elements to be covered. Each (i, 1)-singleton x is regarded as a set that covers exactly i elements corresponding to the i clauses containing x. So the MaxSAT problem is equal to find a minimum number of sets to cover all elements. As shown in [Bliznets and Golovnev, 2012], this case can be quickly solved by using fast algorithms for the set cover problem.

Lemma 5. ([Bliznets andGolovnev, 2012]) MaxSATwith the formula containing only (3, 1)/(4, 1)-singletons can be solved in O∗ (1.2576m) time.

5 The Final Result

Now we present our main result that MaxSAT can be solved in O∗ (1.2886m) time. The algorithm will apply the above seven branching steps in order. However, before applying each branching step, we first iteratively apply our reduction rules in order until the instance becomes reduced. We only execute our branching operations on reduced instances. All the reductions can be done in polynomial time. For the first six branching steps, the biggest branching vector is 1.2886, which is corresponding to the branching vector (6,6,5,5) in Step 5.4. In the last step, we solve the remaining instance in O∗ (1.2576m) time directly by Lemma 5. So we can solve the whole instance in time O∗ (1.2886m). It is clear that each step of the algorithm uses only polynomial space.

Theorem 1. MaxSAT can be solved in O∗ (1.2886m) time and polynomial space.

6 Conclusion

In this paper, we give a new algorithm for MaxSAT and improve the running time bound from O∗ (1.2989m) to O∗ (1.2886m). For such a classic problem, any small progress is not easy nowadays. To get the improvement, we need to well understand previous techniques and bottleneck cases, and also need to use new reduction and analysis techniques. While improving the running time bound, we reveal more properties of the problem and refine the branching strategies for (2, 2)-variables and (3, 2)-variables.

Our running time bound was obtained by purely worst-case analysis. In practice, some reduction and branching operations may have a good performance on practical instances, which deserves further study. As mentioned in [Morgado et al., 2013] in some cases branch-and-search algorithms are the best option to solve the problem. So it is also interesting to integrate our reduction and branching techniques to fast solvers.

Acknowledgements

The work is supported by the National Natural Science Foundation of China, under grant 61972070.