A Fast Algorithm for MaxSAT above Half Number of Clauses

1 Introduction

The BOOLEAN SATISFIABILITY problem (SAT), as the first proven NP-complete problem [Cook, 1971], is a cornerstone of computational complexity theory. Its optimization version, the MAXIMUM SATISFIABILITY problem (MaxSAT), holds an equal level of significance. Given a CNF formula, SAT is to find an assignment of the variables to satisfy all clauses, while MaxSAT is to satisfy the maximum number of clauses (or at least k clauses for an input integer k). SAT, MaxSAT, and many of their variants are arguably the most influential problems due to their significant applications in Computer Science, Artificial Intelligence, and many other fields. Although most of these problems are shown computationally hard [Schaefer, 1978; Garey and Johnson, 1979], their significance still drives various approaches to solve them, including heuristic, approximation, exact, and parameterized algorithms, etc. We refer to [Biere et al., 2021; Fichte et al., 2023] for more comprehensive surveys.

There has been extensive research on moderately exact exponential algorithms for SAT, MaxSAT, and their variants. The trivial algorithm that enumerates all possible assignments runs in time O∗ (2n ), where n is the number of variables. The popular Strong Exponential Time Hypothesis [Impagliazzo and Paturi, 2001] asserts that no algorithm solves SAT and MaxSAT in time O∗ ((2-ϵ)n ) for any constant ϵ > 0. Therefore, different restricted versions and various measures or parameters have been considered [Dantsin and Hirsch, 2021; Samer and Szeider, 2021].

∗Contact Author

In recent years, several upper bounds for these problems have been improved. For SAT, Chu et al. (2021) presented an O∗ (1.2226m)-time algorithm, where m is the number of clauses in the formula, and Peng and Xiao (2023) designed an O∗ (1.0641L)-time algorithm, where L is the length of the formula. For MaxSAT, the upper bounds have been improved to O∗ (1.2886m) [Xiao, 2022] and O∗ (1.0911L) [Brilliantov et al., 2023], respectively. Prior to this, most of these bounds had not seen any progress for decades. While pursuing better exact exponential algorithms for important NPhard problems is worthwhile on its own theoretical side, this might also be potentially helpful for practical solving. Several techniques and principles behind these algorithms have been used in practical solvers [Chu et al., 2023; Li et al., 2023; Fichte et al., 2023]. In addition, the bottlenecks and revealed structural obstructions might suggest some directions for understanding hard instances [Al-Yahya et al., 2023].

We will study exact algorithms for MaxSAT. When measuring the computational complexity of MaxSAT, in addition to parameters n (the number of variables), m (the number of clauses) and L (the length of the input) mentioned above, there is another natural parameter: the number of satisfied clauses k. From the first algorithm with runtime O∗ (1.6181k ) by Mahajan and Raman [1999], the upper bound in terms of k has been improved several times. Currently, the best result is O∗ (1.3248k ) [Chen et al., 2017]. For the case that k is small, MaxSAT can be solved efficiently. However, MaxSAT is only interesting for the case that k is relatively large (k > ⌈m/2⌉), since for any CNF formula with m clauses, either the alltrue or the all-false assignment can satisfy at least ⌈m/2⌉ clauses. Motivated by this, Mahajan and Raman [1999] introduced the following "above guarantee" parameterization of MaxSAT with parameter µ, which is the excess of the number of satisfied clauses k over the lower bound ⌈m/2⌉.

MAXSAT ABOVE HALF (MaxSAT-AH)

Input: A CNF formula F with n variables and m clauses, and a positive integer µ (the parameter).

Question: Does there exist an assignment of n variables that satisfy at least ⌈m/2⌉ + µ clauses?

Can we solve MaxSAT-AH efficiently when µ is small, i.e., when k is close to ⌈m/2⌉? Mahajan and Raman [1999] affirmatively answered this question by proving that an O∗ (ck )- time algorithm implies an O∗ (c6µ )-time algorithm. Previously, MaxSAT-AH can be solved in time O∗ (5.4064µ ), which was derived from the current best result O∗ (1.3248k ) by using the above result [Chen et al., 2017]. To the best of our knowledge, all previous improvements in the runtime bound with respect to µ were derived from improvements with respect to k. In other words, for the parameter µ, the paradigm for improvements introduced in [Mahajan and Raman, 1999] had stood as the sole one for more than two decades. This poses the following question: is there another way to achieve further improvements on the runtime bound with respect to µ?

We also highlight that since the introduction of the "above guarantee" parameterization for MaxSAT and MaxCut by Mahajan and Raman [1999], analysis of parameterization above guarantee has become a highly active and fruitful line of research, not only for MaxSAT-related problems [Gutin and Yeo, 2017], but also for many other important NP-hard problems. Examples include VERTEX COVER [Lokshtanov et al., 2014; Garg and Philip, 2016], MULTIWAY CUT [Cygan et al., 2013], and several others [Mahajan et al., 2009]. For more comprehensive surveys, we refer to [Gutin and Yeo, 2017; Gutin and Mnich, 2022]. Currently, the "above guarantee" parameterization has become a standard and active research topic in Parameterized Complexity.

Our Contribution. In this paper, we prove that MaxSATAH can be solved in time O∗ (2.1479µ ) by developing a new algorithm that is tailored to the "above guarantee" parameter µ. This result significantly improves the previous O∗ (5.4064µ ). Our algorithm does not use the paradigm introduced by Mahajan and Raman [1999]. Thus, this is the first algorithm parameterized by µ that does not invoke algorithms parameterized by k in over two decades.

Our algorithm follows the branch-and-bound paradigm. Most previous algorithms for SAT and MaxSAT are also branch-and-bound algorithms and frequently use the simplest branching scheme that branches on a variable into two subbranches by assigning value 1 or 0 to it. To get a running-time bound in terms of a parameter, we need to analyze how much the parameter decreases in each sub-branch. However, for the parameter µ = k-⌈m/2⌉, it may not always decrease even in a simple branching operation. For example, in a sub-branch, if the decrease of k is d, the decrease of mmay be more than 2d. The situation will get more complicated if the branching rule needs to assign several variables simultaneously. In general, there are several structural obstructions that prevent our parameter from decreasing, and these are the reasons why the existing branch-and-bound algorithms for MaxSAT can not be directly used to analyze a runtime bound with respect to µ. To address this issue, we develop two novel reduction rules, namely R-Rule 5 and R-Rule 6, to overcome these obstructions. As a result, our algorithm manages to efficiently decrease the parameter µ in each sub-branch, even if we apply some complicated branching operations.

In the last step of our algorithm, we handle a special case of the problem by reducing it to the MINIMUM SET COVER problem (MSC). This approach has already been used in the literature [Bliznets and Golovnev, 2012; Chen et al., 2017; Xiao, 2022]. However, our case is different from those in the literature, and the methods used in [Bliznets and Golovnev, 2012; Chen et al., 2017; Xiao, 2022] are not efficient enough to achieve our result. For this issue, we still employ this approach but make certain adaptations, which enable us to utilize the existing algorithm for MSC [van Rooij and Bodlaender, 2011] more effectively to avoid a bottleneck.

Finally, we can prove that the worst branch in our algorithm will generate a branching vector not worse than (0.5, 1.5) (branching into two sub-branches: one reduces µ by at least 0.5 and the other reduces µ by at least 1.5), which implies our upper bound O∗ (2.1479µ ).

Proofs of lemmas marked with ♣ are deferred to the full version of the paper due to space limitations.

2 Preliminaries

A boolean variable (or simply variable) can be assigned value 1 (TRUE) or 0 (FALSE). A variable has two corresponding literals: the positive literal x and the negative literal x. We use x to denote the negation of literal x, and thus x = x. A clause is a set of literals. Given a set V of variables, a CNF formula (or simply formula) is a set of clauses on V . An assignment for V is a map A : V → {0, 1}. A clause is satisfied by an assignment if at least one literal in it gets value 1 under the assignment. An assignment is an optimal assignment to a formula F if it satisfies the maximum number of clauses in F. An instance of the MaxSAT problem, denoted by (F, k), asks whether there is an assignment for the variables that satisfies at least k clauses in F.

In a formula F, a variable x is called a d-variable (resp., a d+-variable) if x appears d (resp., at least d) times in F, and a literal z is called an (i, j)-literal (resp., an (i+, j)-literal or (i-, j)-literal) if z appears i (resp., at least i or at most i) times and z appears j times in F. Similarly, we can define (i, j+)-literal, (i+, j+)-literal, etc. The length of a clause C, denoted by |C|, is the number of literals in C. A clause is a k-clause (resp., k+-clause) if the length of it is k (resp., at least k). A clause C is called unit clause (resp., non-unit clause) if |C| = 1 (resp., |C| ≥ 2). A literal x is called a singleton if all of its negations x are contained in unit clauses, and non-singleton otherwise. Let C be a set of literals in formula F, we use CLS(C) to denote the set of all clauses in F that contain some literal in C, and use UT(C) to denote the set of all clauses that only contain literals in C, i.e.,

For two sets of literals C1 and C2, we may simply write their union as C1C2. A clause containing a single literal x may be simply written as x. For a set of literals C, we use C to denote the set of negations of literals in C and use C = 1 (resp., C = 0) to denote that each literal in C is assigned value 1 (resp., 0). For a formula F, we denote F[C = 1] as the resulting formula obtained from F by removing all clauses containing some literal in C and removing all literals in C from all clauses in F, and let F[C = 0] = F[C = 1].

2.1 Branch-and-Bound Algorithms

Our algorithm is a branch-and-bound algorithm, which first exhaustively applies some reduction rule to reduce the instance and then searches for a solution by branching.

A reduction rule transforms, in polynomial time, an instance I = (F, k) into another instance I ′ = (F ′ , k′ ). A reduction rule is correct if I is a YES-instance if and only if I ′ is a YES-instance. We will use (F, k) → (F ′ , k′ ) to denote a reduction rule. In our algorithm, k > k′ holds for all reduction rules, and so they can only be applied a polynomial number of times and do not exponentially increase the running-time bound.

When no reduction rule can be applied, we do branching. The branching operation will generate a search tree and the size of the tree is related to the exponential part of the running-time bound. Let µ(·) be the measure of an instance. In our algorithm, the measure will not increase in each step, and the problem can be solved in polynomial time if the measure becomes non-positive. A branching rule will branch on the current instance I into several sub-instances I1, . . . , Il such that µ(Ii) < µ(I) for each index i ∈ [l]. The branching rule is called safe if it holds that I is a YESinstance if and only if at least one of the sub-instances is a YES-instance. Let T(µ) be an upper bound on the size of the search tree generated by the algorithm on any instance with the measure of at most µ. For a branching rule, we will obtain a recurrence relation T(µ) ≤ ∑i∈[l] T(µ - di), where di = µ - µ(Ii) for i ∈ [l]. This is also represented by a branching vector (d1, . . . , dl). The largest root of the function f(x) = 1- ∑li=1 x-di is called the branching factor of the branching vector. If the largest branching factor among that of all branching vectors is γ, then T(µ) = O(γ µ ). More details about analyzing branching algorithms can be found in [Fomin and Kratsch, 2010]. We say that one branching vector is not worse than another if its corresponding branching factor is not greater than that of the latter.

2.2 The Measure

It should be emphasized that once the measure µ ≤ 0, i.e., k ≤ ⌈m/2⌉, the algorithm can report that the instance is a YES-instance and terminate since there is always an assignment satisfying at least ⌈m/2⌉ clauses. To facilitate the analysis, we will use the measure µ = k -m/2 instead of k-⌈m/2⌉. This will not affect the running-time bound since there is only a constant difference between them.

3 Reduction Rules

In this section, we introduce reduction rules (R-Rules for short) used in our algorithm. Reduction rules are typically developed to handle some special structures of the instance, and then we may be able to design more efficient branching rules for the problem. Although previous algorithms for MaxSAT have various reduction rules, our algorithm only employs four of them. This is because we must ensure that when applying a reduction rule, our measure µ does not increase, thus guaranteeing efficient running time. As a result, certain reduction rules from previous algorithms may not be applicable to our algorithm. Our algorithm consists of a total of six reduction rules, with the first four being well-known and used in the literature. The last two rules, which are newly developed, serve as crucial components of our algorithm.

R-Rule 3 (Bansal and Raman 1999). (F ′ ∧ xC ∧ xC, k) → (F ′ ∧ C, k - 1).

R-Rule 2 (Bansal and Raman 1999). If there is an (1, 1)- literal x contained in clauses xC and xD, then (F ′ ∧ xC ∧ xD, k) → (F ′ ∧ CD, k - 1).

In R-Rule 3, we allow C = ∅. For this case, it is equivalent to deleting two clauses {x} and {x} and decreasing k by 1.

Note that if there is an (1+, 0)-literal x, we can simply assign x = 1. Actually, this is a special case of R-Rule 4.

R-Rule 4 (Chen and Kanj 2004). If there is an (a, b)-literal x contained in at least b unit clauses x, then (F, k) → (F[x = 1], k - a).

The following R-Rules 5 and 6 are newly introduced and crucial in our algorithm. They can guarantee a good complexity for our branching rules introduced later.

R-Rule 5. Let x be an (a, 1)-non-singleton and xD be the unique clause containing literal x. Assume that there are p clauses containing some literal from D but no literal x or x, and q clauses only containing literals fromD. If p ≤ q, then (F, k) → (F[x = 1], k - a).

Lemma 1. R-Rule 5 is correct.

Proof. It is sufficient to prove that there is optimal assignment A′ to F such that x is assigned to value 1.

Let A be an optimal assignment to F that sets x = 0. If D is satisfied by A, then replacing x = 0 with x = 1 in A would not decrease the number of satisfied clauses since xD is the unique clause containing literal x that is already satisfied. Next, we assume that D = 0 in assignment A.

Let A′ be an assignment obtained from A by replacing xD = 0 with xD = 0 (i.e., each literal in xD is assigned 1 in A′ ). We show that A′ is still an optimal assignment to F.

Let G be the set of clauses containing literals in xD or xD, i.e., G = CLS({x} ∪ {x} ∪ D ∪ D). Note that the number of satisfied clauses in F \ G under assignments A and A′ is equal. Therefore, we focus on the clauses in G. On the one hand, at least q clauses in G are unsatisfied under assignment A because there are q clauses only containing literals in D, and assignment A sets D = 0. On the other hand, under the assignment A′ , at most p clauses in G would be unsatisfied. This is due to the fact that all clauses containing literals in xD are satisfied, and there are at most p clauses containing literals in xD but no literals in xD, which are the only possible clauses that might be unsatisfied. Since p ≤ q, the number of satisfied clauses in F under assignment A′ is not less than that under assignment A. This implies that A′ is also an optimal assignment to F such that x = 1.

R-Rule 6. Let x be an (a, b)-literal such that there are a-1 unit clauses {x}, and let xC1, · · · , xCa be the clauses containing literal x. Assume that there are p clauses containing some literal in ⋃ai=1 Ci but no literal x or x, and q clauses only containing literals in ⋃ai=1 Ci. If p ≤ q + a - 1, then (F, k) → (F[x = 0], k - b).

Lemma 2. R-Rule 6 is correct.

Proof. It suffices to show that there is an optimal assignment A′ to F where x is assigned to value 0.

Let A be an optimal assignment to F that sets x = 1. If at least one of Ci(1 ≤ i ≤ a) is satisfied under A, then replacing x = 1 with x = 0 in A would not decrease the number of satisfied clauses. This is because setting x = 0 satisfies a - 1 unit clauses {x}, and makes at most a - 1 clauses among xC1, · · · , xCa become unsatisfied. Next, we assume that assignment A sets LC = 0, where LC = ⋃ai=1 Ci.

Let A′ be an assignment obtained from A by replacing xLC = 0 with xLC = 0 (i.e., x = 0 and each literal in LC is assigned 1 in A′ ). We show that A′ is still an optimal assignment to F.

Let G be the set of clauses containing some literals in xLc or xLc, i.e., G = CLS({x}∪{x}∪Lc ∪Lc). We only need to consider the clauses in G since assignment A and A′ satisfy an equal number of clauses in F \G. There are a-1 unit clauses {x} and q clauses only containing literals in LC, which are all unsatisfied under assignment A since x = 1 and LC = 0 in A. Thus, the number of clauses in G that are not satisfied under assignment A is at least q+a-1. However, assignment A′ only results in a maximum of p unsatisfied clauses in G. This is because under assignment A′ , all clauses containing literals in xLC (which include all clauses with literal x or x) are satisfied. Additionally, there are at most p clauses that contain some literals in xLC but no literals in xLC, which are the only possible clauses that might not be satisfied under assignment A′ . Since p ≤ q + a - 1, the number of satisfied clauses in F under assignment A′ is not less than that under assignment A. Therefore, assignment A′ is also an optimal assignment to F where x = 0.

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

Lemma 3 (♣). For any formula F, applying any reduction rule will not increase the measure µ. Moreover, it takes polynomial time and polynomial space to apply the reduction rules to transfer F to a reduced one.

Lemma 4 (♣). In a reduced formula, all variables are 3+- variables.

Lemma 5. Let F be a reduced formula and S be a set of distinct literals without complementary literals. Then, after assigning value 1 to all literals in S, the measure decreases by at least |CLS(S)|-|UT(S)| 2 , i.e., µ(F) - µ(F[S = 1]) ≥ |CLS(S)|-|UT(S)| 2 .

Proof. After assigning value 1 to all literals in S, all clauses containing some literals from S (i.e., CLS(S)) would be satisfied and be removed from the formula. Besides, all clauses only containing literals from S (i.e., UT(S)) would be removed from the formula since all literals in them are assigned value 0. Note that CLS(S) and UT(S) are disjoint. Consequently, after assigning value 1 to all literals in S, parameter m, the number of clauses, decreases by |CLS(S)|+|UT(S)|, and parameter k, the number of clauses that need to be satisfied, decreases by |CLS(S)|. Therefore, the measure µ =

Lemma 6. Let F be a reduced formula and x be an (a, b)- literal in it. If there are t unit clauses x (resp., x) in F, then branching on x results in a branching vector not worse than ( a2 , b-t 2 ) (resp., ( a-t 2 , b2 )).

Proof. If t = 0, then the lemma holds by applying Lemma 5 to both sub-branches. Consider the case that there are t > 0 unit clauses {x}. Since R-Rule 3 can not be applied, there is no unit clause {x}. Thus, by Lemma 5, the measure decreases by a-0 2 (resp., b-t 2 ) after assigning x = 1 (resp., x = 0). Similarly, for the case that there is t > 0 unit clauses {x}, the branching vector is not worse than ( a-t 2 , b2 ).

4 The Main Algorithm

Our algorithm consists of three main parts: (1) applying the reduction rules iteratively until obtaining a reduced formula; (2) checking if µ ≤ 0 and, if so, reporting that the current instance is a YES-instance and terminating the algorithm; (3) employing branching rules to search for a solution. We have six branching steps, each of which is going to handle some type of literals. The branching vectors and branching factors in each step are listed in Table 1.

Before giving the detailed branching steps, we first show two frequently used properties.

Lemma 7. Let x be an (a, 1)-literal with the unique clause containing literal x being xD. It is safe to branch with (B1) x = 1; (B2) x = 0 and D = 0.

Proof. Let A be an optimal assignment to F that sets x = 0. If D is satisfied by A, then setting x = 1 in A would not decrease the number of satisfied clauses since xD is the unique clause containing literal x that is already satisfied. Hence, there exists an optimal assignment with either x = 1 or with x = 0 and D = 0.

Lemma 8. Let x be an (a, b)-literal such that there are a - 1 unit clauses {x}. Let the clauses containing literal x be xC1, · · · , xCa. It is safe to branch with (B1) x = 0; (B2) x = 1 and Ci = 0 for 1 ≤ i ≤ a.

Proof. Let A be an optimal assignment to F that sets x = 1. If at least one of Ci(1 ≤ i ≤ a) is satisfied under A, setting x = 1 would make a - 1 unit clauses {x} to be satisfied, but only at most a - 1 clauses among xC1, · · · , xCa to be unsatisfied. Hence, there exists an optimal assignment with either x = 0 or with x = 1 and Ci = 0 for 1 ≤ i ≤ a.

Next, we are going to present our branching steps. When introducing one branching step, we assume that the current instance is a reduced instance and no previous branching step can be applied to it.

4.1 Step 1: 6+-Variables and (4, 1)-Literals

Directly branching on a high-degree variable leads to a good branching vector. In this step, we deal with such variables.

• B-Rule 1. If there is a 6+-variable or a (4, 1)-literal x, then branch with (B1) x = 1; (B2) x = 0.

Lemma 9. The branching vector of B-Rule 1 is not worse than (1.5, 0.5).

Proof. The following three cases cover all possible configurations for x.

Case 1: x is a (4+, 1)-literal. There is no unit clause x since R-Rule 4 is not applicable, and there is at most one unit clause x. By Lemma 6, we know that the branching vector is not worse than ( 4-1 2 , 12 ) = (1.5, 0.5).

Case 2: x is a (4+, 2)-literal. There is at most one unit clause x by R-Rule 4 and if there is a unit clause x, then there is no unit clause x by R-Rule 3. There are at most two unit clauses x, and if there is a unit clause x, then there is no unit clause x by R-Rule 3. By Lemma 6, the branching vector is not worse than ( 42 , 2-1 2 ) = (2, 0.5) or ( 4-2 2 , 22 ) = (1, 1).

Case 3: x is an (a, b)-literal, where a ≥ b ≥ 3. Since R-Rule 4 and R-Rule 3 can not be applied, we know that the formula does not contain unit clauses x and x simultaneously and it contains at most b-1 unit clauses x or at most min{a1, b} unit clauses x. By Lemma 6, the branching vector is not worse than ( a2 , b-(b-1) 2 ) = ( a2 , 1 2 ) for the former case and not worse than ( a-(a-1) 2 , b2 ) = ( 12 , b2 ) for the latter case. Since a, b ≥ 3, the branching vector is not worse than (1.5, 0.5).

4.2 Step 2: (3, 2)-Literals

In this step, we deal with (3, 2)-literals. Let x be a (3, 2)- literal with five clauses xC1, xC2, xC3, xD1, and xD2.

B-Rule 2. If D1 ∪ D2 ̸= ∅, branch with (B1) x = 1; (B2) x = 0.

Lemma 10. The branching vector of B-Rule 2 is not worse than (1.5, 0.5).

Proof. There is at most one unit clause x since D1 ∪D2 ̸= ∅. If there is no unit clause x, then there is at most one unit clause x by R-Rule 4. By Lemma 6, the branching vector is not worse than ( 32 , 2-1 2 ) = (1.5, 0.5). If there is one unit clause x, then there is no unit clause x by R-Rule 3 and the branching vector is not worse than ( 3-1 2 , 22 ) = (1, 1) by Lemma 6, which is also not worse than (1.5, 0.5).

B-Rule 3. If D1 = D2 = ∅, branch with (B1) x = 0; (B2) x = 1 and C1 = C2 = C3 = 0 according to Lemma 8.

Lemma 11. The branching vector of B-Rule 3 is not worse than (1, 2).

Proof. There are two unit clauses x (i.e., |UT(x)| = 2) by the condition of this rule and no unit clause x by R-Rule 3. By Lemma 5, the measure decreases by at least 2-0 2 = 1 in the first sub-branch and |CLS(xC1C2C3)|-|UT(xC1C2C3)| 2 in the second sub-branch. Let p = |CLS(C1C2C3) \ CLS(x ∪ x)| and q = |UT(C1C2C3) \ CLS(x ∪ x)|. We have p ≥ q + 3 since R-Rule 6 can not be applied. With |CLS(x)| = 3 and |UT(x)| = 2, it holds that |CLS(xC1C2C3)| - |UT(xC1C2C3)| = (|CLS(x)| + p) - (UT(x) + q) = (3 + p) - (2 + q) = 1 + p - q ≥ 4. Thus, the branching vector is not worse than (1, 42 ) = (1, 2).

4.3 Step 3: (2+, 1)-Non-Singletons

B-Rule 4. If there is an (2+, 1)-non-singleton x with the unique clause containing x being xD, then branch with (B1) x = 1; (B2) x = 0 and D = 0 according to Lemma 7.

Lemma 12. The branching vector of B-Rule 4 is not worse than (1, 1).

Proof. Let x be an (a, 1)-non-singleton such that a ≥ 2. By Lemma 5, the measure decreases by at least a-0 2 = a2 in the first sub-branch since D ̸= ∅, and at least |CLS(xD)|-|UT(xD)| 2 in the second sub-branch. Since that x is an (a, 1)-nonsingleton and R-Rule 4 is not applicable, we know that |CLS(x)| = 1 and |UT(x)| = 0. Let p = |CLS(D) \ CLS(x ∪ x)| and q = |UT(D) \ CLS(x ∪ x)|. we have p ≥ q + 1, other R-Rule 5 can be applied. Thus, it holds that |CLS(xD)|-|UT(xD)| = (|CLS(x)|+p)-(|UT(x)|+q) = 1 + p - q ≥ 2. Thus, the branching vector is not worse than ( a2 , 22 ), and so not worse than (1, 1) since a ≥ 2.

1. Step 4: (2, 2)-Literals and (2, 1)-Singletons B-Rule 5. If there is a (2, 2)-literal x such that there is no unit clause x or x, then branch with (B1) x = 1; (B2) x = 0.

Lemma 13. The branching vector of B-Rule 5 is not worse than (1, 1).

Proof. By Lemma 6, the branching vector is not worse than ( 2-0 2 , 2-0 2 ) = (1, 1).

B-Rule 6. Let x be a (2, 2)-literal or (2, 1)-literal such that there is exactly one unit clause x. Let the two clauses containing x be xC1 and xC2. Branch with (B1) x = 0; (B2) x = 1 and C1 = C2 = 0 according to Lemma 8.

Lemma 14. The branching vector of B-Rule 6 is not worse than (0.5, 1.5).

Proof. There is no unit clause x, otherwise R-Rule 3 can be applied. Thus, we know C1, C2 ̸= ∅. By Lemma 5, in the first sub-branch, the measure decreases by at least 2-0 2 = 1 if x is a (2, 2)-literal and at least 1-0 2 = 0.5 if x is a (2, 1)-literal.

By Lemma 5 again the measure decreases by at least |CLS(xC1C2)|-|UT(xC1C2)| 2 in the second sub-branch. Let p = |CLS(xC1C2) \ CLS(x ∪ x)| and q = |UT(xC1C2) \ CLS(x ∪ x)|. We have p ≥ q + 2, otherwise R-Rule 6 can be applied. With |CLS(x)| = 2 and |UT(x)| = 1, we have |CLS(xC1C2)| - |UT(xC1C2)| = (|CLS(x)| + p) - (|UT(x)| + q) = (2 + p) - (1 + q) = 1 + p - q ≥ 3.

Lemma 15. After Step 4, the formula only contains (3, 1)- singletons and their negations.

Proof. By Lemma 4, all variables in a reduced formula are 3+-variables. Step 1 deals with all 6+-variables and (4, 1)- literals. Step 2 deals with all (3, 2)-literals. After Step 2, the formula only contains 4-variables and 3-variables. For a (2, 1)-literal, it is handled by Step 3 if it is a (2, 1)-nonsingleton and handled by Step 4 otherwise. All (2, 2)-literals are handled by Step 4. Moreover, all (3, 1)-non-singletons are handled by Step 3. Consequently, the remaining literals in the formula are (3, 1)-singletons and their negations.

4.5 Step 5: (3, 1)-Singletons in Short Clauses

In this step, we are going to deal with (3, 1)-singletons contained in clauses with a length of 2 or 3.

Definition 2. An instance is simplified if the formula only contains (2+, 1)-singletons and their negations.

By Lemma 15, we know that the current instance is a simplified instance. We assume w.l.o.g. that all literals in unit clauses are negative literals in a simplified instance. By this assumption, we have that |CLS(x)| = 3 for any positive literal x in the formula and |UT(x)| = 1 for any negative literal x in the formula.

First, we introduce a structural property of simplified instances, which allows us to apply a better branching.

Lemma 16. A simplified instance has an optimal assignment that satisfies all non-unit clauses.

Proof. Let A be an optimal assignment that satisfies the maximum number of non-unit clauses. Assume that there is a non-unit clause C that is unsatisfied under A. Let x be some literal in C. Then assignment A sets x = 0. Since x is a (2+, 1)-singleton, there is only one unit clause x that contains x and it is satisfied by A. Let A′ be the assignment obtained from A by replacing x = 0 with x = 1. Then, assignment A′ satisfies the non-unit clause C and makes at most one unit clause x unsatisfied. This shows that the number of clauses satisfied by A′ is not less than that by A. However, the number of non-unit clauses satisfied by A′ is greater than that by A, a contradiction to the assumption on A.

Based on Lemma 16, we apply the following two branching rules to eliminate 2-clauses and 3-clauses.

B-Rule 7. If there is a 2-clause xy, then branch with (B1) x = 1; (B2) x = 0 and y = 1.

Lemma 17. The branching vector of B-Rule 7 is not worse than (1, 1.5).

Proof. By Lemma 5, we know that the measure decreases by at least 3-1 2 = 1 in the first sub-branch and at least |CLS(xy)|-|UT(xy)| in the second sub-branch.

2 Since that a negative literal is contained in a unique unit clause, and a unit clause only contains a negative literal, we have that |CLS(xy)| = |CLS(x)| + |CLS(y)| = 1 + 3 = 4 and |UT(xy)| = |UT(x)| + |UT(y)| = 0 + 1 = 1. Thus, the branching vector is not worse than (1, |CLS(xy)|-|UT(xy)| 2 ) = (1, 4-1 2 ) = (1, 1.5).

B-Rule 8. If there is a 3-clause xyz, then branch with (B1) x = 1; (B2) x = 0 and y = 1; (B3) x = y = 0 and z = 1.

Lemma 18. The branching vector of B-Rule 8 is not worse than (1, 1.5, 2).

Proof. By the same argument in the proof of Lemma 17, we can show that the measure decreases by at least 1 and 1.5 in the first and second sub-branches respectively.

Consider the third sub-branch. We have |CLS(xyz)| = |CLS(x)| + |CLS(y)| + |CLS(z)| = 1 + 1 + 3 = 5 since that a negative literal is only contained in a unit clause, and a unit clause only contains negative literal. Note that all 2clauses have been handled by B-Rule 7, the length of a nonunit clause is at least 3 now. Thus, |UT(xyz)| = |UT(xy)|+ |UT(z)| = 0 + 1 = 1 holds. By Lemma 5, the measure decreases by at least |CLS(xyz)|-|UT(xyz)| 2 = 5-1 2 = 2. Therefore, the branching vector is not worse than (1, 1.5, 2).

4.6 Step 6: Fast Solving the Remaining Part

After Step 5, all non-unit clauses in F are 4+-clauses. Recall that we denote by n the number of variables and by m the number of clauses in F, and there are n unit clauses and m-n non-unit clauses in F.

Lemma 19. If 0.7m + 0.037n ≥ k holds in a simplified instance (F, k) with all non-unit clauses being 4+-clauses, then we can find an assignment satisfying at least k clauses in polynomial time.

Proof. We set p = 0.26 and assign each variable with value 1 with probability p. Then, each unit clause is satisfied with a probability of 1 - p. Since every non-unit clause contains at least 4 positive literals, a non-unit clause is satisfied with a probability of 1 - (1 - p)4 . Thus, by the linearity of expectation and setting p = 0.26, the expected number of satisfied clauses under this random assignment would be

By using the method of conditional expectation, we can deterministically construct an assignment that satisfies at least k clauses in polynomial time.

Next, we assume that 0.7m+ 0.037n < k. Thus, 0.6m+ 0.11n < 3(k - 0.5m) = 3µ. For this case, we follow the approach proposed in [Bliznets and Golovnev, 2012] and reduce the problem to the MINIMUM SET COVER problem, which is formally defined as follows.

MINIMUM SET COVER (MSC)

Input: A universe U and a family S of subsets of U; A positive integer s.

Question: Does there exist a subfamily C ⊆ S such that |C| ≤ s and the union of C is U?

An instance of MSC is denoted by (U, S, s). A subfamily C ⊆ S is a set cover for S if ⋃D∈C D = U. We use |U| to denote the number of elements in universe U and |S| to denote the number of subsets in family S. For an element e ∈ U, the frequency of e, denoted by f(e), is defined as the number of subsets in S that contain e. It was shown in [van Rooij and Bodlaender, 2011] that MINIMUM SET COVER can be solved in time O∗ (1.28759k(U,S) ), where k(U, S) = ∑e∈U v(f(e)) + ∑S∈S w(|S|), and v and w are weight functions N → R+. The maximum value of v is 0.595723 and the maximum value of w is 1. We note that the maximum value of w for sets of size at most 3 is 0.706023 (refer to the end of section 3 in [van Rooij and Bodlaender, 2011]). Thus, the following result can be utilized.

Lemma 20 (van Rooij and Bodlaender 2011). If each subset in S has a size of at most 3, then MINIMUM SET COVER can be solved in time O∗ (1.287590.595723|U|+0.706023|S| ) ⊆ O∗ (1.290.6|U|+0.71|S| ) and polynomial space.

Given a simplified instance I = (F, k) of MaxSAT, we reduce it to an instance I ′ = (UF, SF,m - k) of MSC as follows. For each non-unit clause Cz in F, there is an element eCz in the universe UF. For each variable xi in F, there is a subset Sxi = {eCz | literal xi appears in clause Cz} in the family SF . We have |UF | = m-n and |SF | = n. Moreover, each subset in SF has a size of 3, since each positive literal xi is a (3, 1)-singleton. This reduction has been used in several algorithms for MaxSAT. The proof of the correctness of this reduction (i.e., Lemma 21) is deferred to the full version of this paper.

Lemma 21 (♣). The simplified instance I of MaxSAT is a YES-instance if and only if the instance I ′ of MSC is a YESinstance.

Lemma 22. Each execution of Step 6 can be done in time O∗ (2.1467µ ) and polynomial space.

Proof. By reducing a simplified instance to an instance of MCS with |U| = m- n and |S| = n, we can solve the problem in time O∗ (1.290.6n+0.71(m-n) ) by Lemma 20. Note that 0.6(m - n) + 0.71n = 0.6m + 0.11n < 3µ, we have 1.293k < 2.1467k , which proves the lemma.

4.7 The Final Result

Now we are prepared to present our main result. The algorithm will execute the above six branching steps in order. Before applying each branching step, reduction rules are exhaustively applied until the instance is reduced. It is important to note that, before each step, if the measure µ ≤ 0, then the algorithm will report that the input instance is a YESinstance and terminate. All reduction rules can be executed in polynomial time. As shown in Table 1, for the first five steps, the largest branching factor is 2.1479, corresponding to the branching vector (1.5, 0.5) in Steps 1, 2, 4, and 5. The last step (Step 6) can be executed in time O∗ (2.1467µ ) by Lemma 22. Thus, the problem can be solved in time O∗ (2.1479µ ). Clearly, each step requires only polynomial space. In conclusion, we obtain Theorem 1. MaxSAT can be solved in O∗ (2.1479µ ) time and polynomial space, where µ = k - ⌈m/2⌉.

5 Discussion and Conclusion

In this paper, we have presented a new algorithm for MaxSAT with running-time bound O∗ (2.1479µ ), where µ = k - ⌈m/2⌉. We compare our algorithm with the algorithms parameterized by k and m. Denote by Aµ our algorithm, by Ak the O∗ (1.3248k )-time algorithm [Chen et al., 2017], and by Am the O∗ (1.2886m)-time algorithm [Xiao, 2022]. Let r = k/m be the ratio of clauses in a formula that one wants to satisfy. The bounds O∗ (1.3248k ) and O∗ (2.1479µ ) can be expressed in terms of m, i.e., O∗ (1.3248rm) and O∗ (2.1479(r-0.5)m), respectively. Figure 1 shows the front line of these algorithms, which indicates that our algorithm Aµ is faster when 0.5 < r ≤ 0.791, Ak is superior for 0.791 < r ≤ 0.901, and Am excels for 0.901 < r ≤ 1.

In our algorithm, the two newly introduced reductions RRule 5 and R-Rule 6 are crucial in our worst-case-based analysis. Whether they also have a good performance and application scenarios in practical solving deserves further research.

Another direction for further study is to consider other "above guarantee" parameterizations of MaxSAT. Given a formula F and a parameter µ′ , an "above guarantee" parameterization of MaxSAT asks whether g(F) + µ′ clauses can be satisfied. Here, g(F) is a lower bound on the maximum number of clauses that can be satisfied. The lower bound considered in this paper is ⌈m/2⌉. Different lower bounds can be obtained if some constraints are imposed on the input CNF-formula. For MaxSAT above other lower bounds, most existing algorithms are based on reducing to other problems [Kim and Williams, 2011; Crowston et al., 2012; Gutin et al., 2013]. It would be interesting to investigate whether other paradigms (e.g., the branch-and-bound paradigm) are applicable to design better algorithms for these "above guarantee" parameterizations of MaxSAT.

Acknowledgements

This work is supported by National Natural Science Foundation of China under grants 62372095 and 62172077, and Natural Science Foundation of Sichuan Province of China under grant 2023NSFSC0059.