# an_improved_upper_bound_for_sat__3c71693a.pdf

An Improved Upper Bound for SAT

Huairui Chu, Mingyu Xiao , Zhe Zhang School of Computer Science and Engineering, University of Electronic Science and Technology of China a1444933023@163.com, myxiao@gmail.com, 2017060106011@std.uestc.edu.cn

We show that the CNF satisﬁability problem can be solved O (1.2226m) time, where m is the number of clauses in the formula, improving the known upper bounds O (1.234m) given by Yamamoto 15 years ago and O (1.239m) given by Hirsch 22 years ago. By using an amortized technique and careful case analysis, we successfully avoid the bottlenecks in previous algorithms and get the improvement.

1 Introduction The problem of testing the satisﬁability of a propositional formula in conjunctive normal form (CNF), denoted by SAT, is one of the most fundamental problems in computer science. It is the ﬁrst problem proved to be NP-complete (Cook 1971) and plays an important role in computational complexity and artiﬁcial intelligence (Garey and Johnson 1979). To make the problem tractable, a large number of references studied it from the view of heuristic algorithms, approximation algorithms, randomized algorithms, and exact algorithms. In this paper, we study exact algorithms for SAT with guaranteed theoretical running time bounds.

1.1 Related Works To evaluate the running time bound, there are three frequently used measures: the number of variables n, the number of clauses m, and the length of the whole input L, i.e., the sum of the lengths of all clauses. The trivial algorithm to check all possible assignments runs in O (2n) time1. A nontrivial bound better than O (2n) was obtained in (Dantsin, Hirsch, and Wolpert 2004), which is O (2n(1 2

1/n log m)). Later better upper bounds were introduced in (Dantsin and Wolpert 2004) and (Schuler 2005). However, no algorithm with running time bound O (cn) for some constant c < 2 was found, despite decades of hard work. The nonexistence of these algorithms is known as the Strong Exponential Time Hypothesis (SETH) (Impagliazzo and Paturi 2001). On the other hand, for a restricted version, the k-SAT problem

The corresponding author. Copyright c 2021, Association for the Advancement of Artiﬁcial Intelligence (www.aaai.org). All rights reserved. 1The notation O suppresses all polynomially bounded factors. For two functions f and g, we write f(n) = O (g(n)) if f(n) = g(n)n O(1).

running times references O (1.260m) (Monien, Speckenmeyer, and Vornberger 1981) O (1.239m) (Hirsch 1998) O (1.234m) (Yamamoto 2005) O (1.2226m) This paper

Table 1: Previous and our upper bounds for SAT

(where each clause in the CNF-formula contains at most k literals), a series of signiﬁcant results have been developed. A branch-and-bound technique was introduced in (Monien and Speckenmeyer 1985) and (Dantsin 1983), which can solve k-SAT in O ((αk)n) time where αk is the largest root of the function x = 2 1/xk 1. After this, a series of improvements on the upper bounds for k-SAT have been made. Most of them are based on derandomization, such as the O (2(1 1/2k)n) bound in (Paturi, Pudl ak, and Zane 1997) and the O ((2 2/(k +1))n) bound in (Dantsin et al. 2002). Recently a new randomized algorithm for k-SAT with a better running time bound was introduced (Hansen et al. 2019). However, the running time bound became complicated to present. When the length of the input L is taken as the measure, from the ﬁrst algorithm with running time bound O (1.0927L) by Gelder (1988), the result was improved frequently. Let us quote the bound O (1.0801L) by Kullmann and Luckhardt (1997), O (1.0758L) by Hirsch (1998), O (1.074L) by Hirsch (2000), and O (1.0663L) by Wahlstr om (2005). Currently, the best known bound was O (1.0652L) obtained by Chen and Liu (2009). Another important measure is the number of clauses m. Monien, Speckenmeyer, and Vornberger (1981) gave an O (1.260m)-time algorithm in 1981, which was improved to O (1.239m) by Hirsch (1998) in 1998. Then it took seven years for Yamamoto to slightly improve Hirsch s bound to O (1.234m) (Yamamoto 2005). In this paper, we will signiﬁcantly improve Yamamoto s bound obtained 15 years ago. Previous and our results are listed in Table 1.

1.2 The Techniques All algorithms in Table 1 are branch-and-search algorithms. The branch-and-search idea is simple and practical: we iteratively branch on a literal into two branches by letting

The Thirty-Fifth AAAI Conference on Artificial Intelligence (AAAI-21)

it be 1 or 0. Consider an (a, b)-literal (a literal such that itself appears in a clauses and the negation of it appears in b clauses). In the branching where the literal is assigned 1, we can reduce a clauses; in the branching where the literal is assigned 0, we can reduce b clauses. We hope that the values of a and b are larger so that we can reduce the instance to a greater extent. There are several developed techniques to deal with (a, b)-literals with small values of a and b, say one of them is at most 2. Thus the worst case will become to branch on a (3, 3)-literal, in which we can only get a branching vector of (3, 3) and a branching factor 1.2600. We get the bound of O (1.260m) (Monien, Speckenmeyer, and Vornberger 1981). It seems that branching on (3, 3)-literals is unavoidable. Hirsch (1998) showed that after branching on a (3, 3)-literal we can always branch with a branching vector at least (4, 3) or (3, 4) subsequently. Combining the bad branching vector (3, 3) with the good branching vector (4, 3) or (3, 4), he got a better worst-case and then improved the running time bound to O (1.239m). Yamamoto (2005) further showed that the worst cases in Hirsch s algorithm would not always happen: we can further branch with (4, 3) or (3, 4) at the third level, i.e., after branching with (4, 3) or (3, 4) after branching with (3, 3). Yamamoto considered more levels of the branching but could only slightly improve the bound to O (1.234m). The improvement is very slow, and we seem to have reached the bottleneck. Our algorithm is still a branch-and-search algorithm, following the main framework in the previous algorithms. We still can not avoid branching on (3, 3)-literals, otherwise, the worst case would be to branch on (3, 4)-literals or (4, 3)- literals, and the bound would be improved to O (1.2208m). We also show that after branching on a (3, 3)-literal we can further branch with better branching vectors. However, the traditional analysis to combine several levels of branchings into a big branching is somewhat complicated and limited. To exhibit the relations among good and bad branchings in our algorithm and also to use as many good branchings as possible to even out the bad ones, we will use an amortized technique to analyze the running time bound. To get the claimed result, we also need to use some new reduction and branching rules and deep analysis of the structure. Due to the limited space, the proofs of lemmas marked with * and one case analysis are omitted, which can be found in the full version of this paper (Chu, Xiao, and Zhang 2020).

2 Preliminaries Let V = {x1, x2, . . . , xn} denote a set of n Boolean variables. For each variable xi (i = 1, 2, 3, . . . , n), a literal is either xi or the negation of it xi (we use x to denote the negation of a literal x, and then x = x). A clause on V is a set of literals on V without a negation of any literal in it, which means x and x cannot be contained simultaneously in a clause for any variable x V . A CNF-formula on V is a sequence of clauses F = {C1, C2, C3, . . . , Cm}. We will use m F to denote the number of clauses in F. An assignment for V is a map A : V {0, 1}. A clause Cj on V is satisﬁed by A if and only if there exists a literal x in Cj such that A(x) = 1. A CNF-formula is satisﬁed by an

assignment A if and only if each clause in it is satisﬁed by A. An assignment A that makes a CNF-formula F satisﬁed is called a satisfying assignment for F. Given a CNF-formula F on a set of variables V , the SAT problem is to check the existence of a satisfying assignment for F. The degree of a literal x in F is the number of clauses in F containing it. The total degree of a literal x is the degree of x plus the degree of x. 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 deﬁne (a, b+)-literal, (a, b )-literal, (a+, b+)- literal, (a , b )-literal and so on. Note that a literal x is an (a, b)-literal if and only if x is a (b, a)-literal. A clause containing exactly c literals is called a c-clause. A pair of literals x and y is called a coincident pair if there are at least two clauses containing them simultaneously. Our algorithm will ﬁrst 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. Next, we ﬁrst introduce the reduction rules.

3 Reduction Rules We have ﬁve reduction rules. The ﬁrst two are easy to observe and used in the literature (Davis and Putnam 1960). R-Rule 1. (Elimination of 1-clauses and pure literals) If the CNF-formula contains a 1-clause {x} or an (a, 0)-literal x with a > 0, assign x = 1. R-Rule 2. (Elimination of subsumptions) If the CNFformula contains two clauses C and C such that C C , then delete C . The following proposition is known as the resolution technique in the literature, which was ﬁrst proved in (Robinson 1965), and then used in many SAT algorithms. Deﬁnition 1. (Resolution on a variable) Let F be a CNFformula containing a variable x. Let E1, E2, . . . , Ea be the clauses containing x and D1, D2, . . . , Db be the clauses containing x. Resolving on variable x is to construct a new CNF-formula F\x by the following method: for each i {1, 2, . . . , a} and j {1, 2, . . . , b}, add the clause Fij = Ei Dj \ {x, x} to the formula if it does not contain both a literal and the negation of it; delete Ei (i {1, 2, . . . , a}) and Dj (j {1, 2, . . . , b}) from the formula. We may always use F\x to denote the CNF-formula after resolving a variable x in F. Proposition 1. (Robinson 1965) Let F be a CNF-formula containing a variable x and F\x be the CNF-formula after resolving on variable x. Then F has a satisfying assignment if and only if F\x does. R-Rule 3. (Resolving on some variables) If there is an (a, b)-literal x such that a = 1 and b 1 or a = 2 and b = 2, then resolve x in F, i.e., replace F with F\x. We also introduce a simple but powerful concept, based on which we can design several reduction rules. Deﬁnition 2. (Autarkic sets) A set X of literals is called an autarkic set if each clause containing a negation of a literal in X also contains a literal in X.

Lemma 1. (*) If a CNF-formula F has a satisfying assignment, then it has a satisfying assignment where all literals in an autarkic set are assigned 1. The following reduction rule was ﬁrstly used in (Hirsch 1998). It is an application of a special autarkic set. R-Rule 4. (Hirsch 1998) If each clause containing a (2, 3+)-literal also contains a (3+, 2)-literal, assign 1 to each (3+, 2)-literal. Our algorithm also needs to eliminate another kind of autarkic sets. R-Rule 5. Let X be the set of (4, 3)-literals x such that there is a clause containing both x and a (3, 3+)-literal. If each clause containing a negation of a literal in X also contains a (4, 3)-literal, assign 1 to each literal in X. Each clause containing a negation of a literal x X also contains a (4, 3)-literal y. Since x is a (3, 4)-literal, we know that y is also in X. Thus X is an autarkic set. In this reduction rule, the requirement of a clause containing both x and a (3, 3+)-literal plays no role in establishing X to be an autarkic set. This requirement is used to identify a particular subset of (4, 3)-literals, which will be useful in our analysis. Lemma 2. After applying any of the above reduction rules, the satisﬁability of the formula does not change. Except for the application of R-Rule 3 on a (2, 2)-literal where the number of clauses does not increase, each application of other reduction rules decreases the clause number by at least 1. Deﬁnition 3. (Reduced formulas) A formula is called reduced if none of the ﬁve reduction rules can be applied to the formula. For an instance F, we will use R(F) to denote the resulting reduced formula after iteratively applying the reduction rules on F. Lemma 3. (*) Given a formula, we can apply the ﬁve reduction rules in polynomial time to change it to a reduced formula. Lemma 4. (*) Let F be a reduced formula. Then there is no 1-clause, (2, 2)-literal or (1 , a)-literal with a 1 in F. Furthermore, the total degree of any literal in F is at least 5.

4 Branch-and-Search Paradigms Our algorithm will ﬁrst apply our reduction rules to reduce the instance. When no reduction rule can be applied anymore, we will branch to search for a solution. Our branching rule is simple. We take a literal x and branch on it into two sub-instances. In one sub-instance we assign x = 1 and in the other one we assign x = 0, i.e, we get two sub instances Fx and F x. Selecting different literals to branch will lead to different algorithms. We want to select good literals to branch on such that the size of the sub instances can be reduced fast. We use the number m of clauses to evaluate the size of the formula. Assume the number of clauses of the current instance is m. If a branching operation branches into

l sub-branches such that the number of clauses in the ith sub-instance decreases by at least ci, we say this operation branches with a branching vector (c1, c2, . . . , cl). The largest root of the function f(x) = 1 Pl i=1 x ci is called the branching factor. If γ is the maximum branching factor among all branching factors in an algorithm, then the running time of the algorithm is bounded by O (γm). More details about the analysis and how to solve recurrences can be found in the monograph (Fomin and Kratsch 2010). The following property is frequently used in the paper: for two branching vectors C = (c1, c2, . . . , cl) and B = (b1, b2, . . . , bl), if it holds that ci bi for each i, then we say B covers C. The corresponding branching factor of a branching vector C is not greater than the corresponding branching factor of a branching vector that covers C.

4.1 Good Formulas & Bad Formulas Similar to the technique used by Niedermeier and Rossmanith to solve the 3-hitting set problem (Niedermeier and Rossmanith 2003), we also classify formulas in our algorithm into two classes: good formulas and bad formulas. For good formulas, we may be able to branch with good branching vectors. For bad formulas, we may only be able to get bad branching vectors. We will show that bad formulas will not appear frequently. Then we can use an amortized analysis to get better branching vectors. To make the amortized analysis easy to follow, we will use the substitution method to prove our bounds. The precise deﬁnitions of good and bad formulas are given below. Deﬁnition 4. (Good formulas & bad formulas) A formula F is a bad formula if and only if the following four conditions are satisﬁed (1) F only contains (3, 3)-literals, (3, 4)-literals and (4, 3)- literals. (2) There is no coincident pair. (3) There is no 2-clause. (4) There is no clause containing a (4, 3)-literal and a (3, 3+)-literal simultaneously. A formula is good if it is not a bad formula.

4.2 The Algorithm and Its Analysis The main steps of our algorithm are listed in Algorithm 1. The precise descriptions and analysis of lines 11 and 14 are delayed to Section 6.1 and Section 6.2. Recall that, for an instance F, R(F) is the resulting reduced instance after applying the reduction rules on F, and m F is the number of clauses in F. We have the following important lemmas, which are the base for us to establish the running time bound. Lemma 5. Let F be a CNF-formula. It holds that m R(F) m F. Furthermore, if F is good, then either R(F) is good or m R(F) m F 1.

Proof. By Lemma 2, we have that m R(F) m F. Next, we assume that F is good. If R(F) = F, obviously R(F) is good. So we assume that some R-Rules are applied. By Lemma 2, we know that

Algorithm 1 SAT(F)

1: if {F is not reduced} then 2: Iteratively apply our reduction rules to reduce it. 3: end if 4: if {F is empty} then 5: Return true. 6: end if 7: if {F contains an empty clause} then 8: Return false. 9: end if 10: if {F is a bad formula} then 11: Apply branching rules in Sec.6.1 to search for a solution. 12: end if 13: if {F is a good formula} then 14: Apply branching rules in Sec.6.2 to search for a solution. 15: end if

if m R(F) = m F then only R-Rule 3 is applied on (2, 2)- literals. For any F with a (2, 2)-literal x in it, we show that after applying R-Rule 3 on x the resulting instance F \x is good. Let the two clauses containing x in F be D1 and D2, the two clauses containing x be E1 and E2. If m F = m F \x, then all Eij = Di Ej \ {x, x} for each 1 i, j 2 are in F \x. If one of D1, D2, E1 and E2 contains at least three literals, then we will get some coincident pair. Otherwise, each Eij is a 2-clause. For any case, F \x is good.

Lemma 6. If the formula F is reduced and bad, then our algorithm can branch with either a branching vector covered by (3, 4) or (4, 3), or a branching vector (3, 3) such that the formula in each branch is good.

Lemma 7. If the formula to branch is reduced and good, then our algorithm can branch with either a branching vector covered by one of (3, 5), (5, 3), and (4, 4), or a branching vector (3, 4) or (4, 3) such that the formula in each branch is good.

The proof of Lemma 6 and Lemma 7 are given in Section 6.1 and Section 6.2, respectively. Next, we prove the running time bound of the algorithm based on Lemma 5, Lemma 6, and Lemma 7.

Theorem 1. SAT can be solved in O (1.2226m) time.

Proof. We use T(F) to denote the size of the search tree (number of nodes in the tree) generated by the algorithm running on an instance F. We only need to prove that T(F) = O(1.2226m F ). To prove the theorem, we will show that there are two constants c1 = 2 and c2 = c1/0.9136 such that T(F) c11.2226m F 1, if F is good, (1)

and T(F) c21.2226m F 1, if F is bad. (2)

First of all, we show that we can assume F is a reduced instance without loss of generality. If the current instance F

with m clauses is not a reduced one, our algorithm will apply reduction rules on it to get a reduced instance F with m clauses. To prove that (1) and (2) hold for F, we only need to prove that (1) and (2) hold for F . The reason is based on the following observations. If both of F and F are bad or good, then it holds that ci1.2226m F ci1.2226m F since m F m F by Lemma 5. If F is bad and F is good, then it holds that c11.2226m F c21.2226m F . If F is good and F is bad, then it still holds that c21.2226m F c11.2226m F because now we have m F m F 1 by Lemma 5 and then c1 < 1.2226c2. Next, we simply assume that the instance F is reduced and use F1 and F2 to denote the two sub instances generated by our branching operations. We use the substitution method to prove (1) and (2). Assume that T(F) ci1.2226m F 1 (where ci = c1 if F is good and ci = c2 if F is bad) holds for all instances F with less than m clauses. We show that it also holds for instances with m clauses. First, we consider the case where F is bad. According to Lemma 6, there are two cases. For the ﬁrst case of branching with a vector (3, 4) or (4, 3), we have that T(F) = T(R(F1)) + T(R(F2)) + 1 c21.2226m R(F1) + c21.2226m R(F2) 1 (by the assumption and c1 < c2)

c21.2226m F 3 + c21.2226m F 4 1 c21.2226m F 1. For the second case of branching with a vector (3, 3), the two sub instances are good, we have that T(F) = T(R(F1)) + T(R(F2)) + 1

c11.2226m F 3 + c11.2226m F 3 1 c21.2226m F 1. Second, we consider the case where F is good. According to Lemma 7, there are two cases. In the ﬁrst case, the branching vector is (3, 5) or (5, 3) or (4, 4). If it is (3, 5) or (5, 3), we have that T(F) = T(R(F1)) + T(R(F2)) + 1

ci11.2226m F 3 + ci21.2226m F 5 1

c21.2226m F 3 + c21.2226m F 5 1 c11.2226m F 1, where ci1, ci2 {1, 2}. If the branching vector is (4, 4), we have that T(F) = T(R(F1)) + T(R(F2)) + 1

ci11.2226m F 4 + ci21.2226m F 4 1

2c21.2226m F 4 1 c11.2226m F 1, where ci1, ci2 {1, 2}. For the second case of branching with a vector (3, 4) or (4, 3) such that the two sub instances are good, we have that T(F) = T(R(F1)) + T(R(F2)) + 1

c11.2226m F 3 + c11.2226m F 4 1 c11.2226m F 1.

We have proved that (1) and (2) hold for F. Thus, it holds that T(F) = O(1.2226m F ), no matter F is good or bad.

5 Some Properties Before giving the detailed steps of the branching operations, we give some properties that will be used to simplify our presentation and analysis. In a branching operation, we need to analyze the branching vector, i.e., the number of clauses decreased in each branching. Sometimes we can get a branching vector good enough for our analysis, such as branching vectors (4, 4), (3, 5), and (5, 3). Sometimes the branching vector is not good enough and we still need to prove the remaining formulas are good, which will allow us to use amortization. Usually, we will fall into one of the following two cases: 1. Some variables are assigned values (including applying R-Rule 1) and then some clauses are deleted because some literals in them are assigned 1. We need to prove that the remaining formula is good. 2. R-Rule 3 is applied and we need to prove that the remaining formula is good. We will use the following two lemmas to help us solve these two cases. Lemma 8. (*) Let F be a formula containing a (3 , 0+) or (0+, 2 )-literal y. Assume the total degree of y is a > 0. If we delete from F at most a 1 clauses and some literals other than y and y, where at least one deleted clause contains y, then the resulting formula is good. Corollary 1. (*) Let F be a reduced formula containing only (3 , 3 ), (2, 4+) and (4+, 2)-literals. For any literal x in it with degree at most 4, the formula Fx is good. Lemma 9. Let F be a formula containing a (1, 1+)-literal x and at least two different (2 , 0+)-literals other than x and x. It holds that either m F\x m F 1 and F\x is a good formula or m F\x m F 2.

Proof. Let the unique clause containing x be C and the clauses containing x be D1, D2, . . . Dl. Let y and z be two different (2 , 0+)-literals other than x and x, where y and z can be each other s negation. It is easy to see that resolving on x will decrease the number of clauses by at least 1. We assume that the number of clauses decreases by exactly 1 after resolving on x and show for this case the formula F\x must be good. For this case, the l + 1 clauses C, D1, D2, . . . Dl are deleted and all the l clauses Di C \ {x, x} (i = 1, 2, . . . , l) are added in F\x. Case 1. x is a (1, 1)-literal: after resolving on x, the degree of any literal does not increase and no literal other than x and x disappears. So y and z are still (2 , 0+)-literals, witnessing the goodness of F\x. Case 2. x is a (1, 2+)-literal: We further distinguish two cases: |C| 3 and |C| 2. If |C| 3, then any pair of literals in C \ {x} will be a coincident pair in F\x. Thus, F\x is good. If |C| 2, then at most one literal the degree of who will increase after resolving on x, since only the degree

Cases Literals Vectors Factors Case 1 (3, 4)-literals (3,4) 1.2208 Case 2 (3, 3)-literals (3 , 3 ) 1.2600

Table 2: Branching for Bad Formulas

Cases Literals Vectors Factors Case 1 (3, 5+)-literals (3,5) 1.1939 Case 1 (4+, 4+)-literals (4,4) 1.1893 Case 2 (3, 4)-literals (4,4) 1.1893 (3,5) or (5,3) 1.1939 (3 , 4 ) or (4 , 3 ) 1.2208 Case 3 (2, 3+)-literals (4,4) 1.1893 (3,5) or (5,3) 1.1939 (3 , 4 ) or (4 , 3 ) 1.2208 Case 4 (3, 3)-literals (4,4) 1.1893 (3,5) or (5,3) 1.1939 (3 , 4 ) or (4 , 3 ) 1.2208

Table 3: Branching for Good Formulas

of literals in C \ {x} will increase. So one of y and z will be remained as a (2 , 0+)-literal in F\x. Thus, F\x is good.

6 Detailed Branching Operations In this section, we show the detailed branching operations in Algorithm 1. Recall that we only branch on reduced formulas. The detailed branching steps for bad and good formulas are given in Sec.6.1 and 6.2, respectively. For a bad formula, if there exist (3, 4) or (4, 3)-literals, then deal with them. Else we deal with (3, 3)-literals. For a good formula, we ﬁrst deal with (3, 5+) or (4+, 4+)-literals; second deal with (3, 4)-literals (and also (4, 3)-literals); third deal with (2, 3+)-literals (and also (3+, 2)-literals); last there are only (3, 3)-literals and we deal with them. The main results of these steps are summarized in the following two tables, where the number with in the Vectors column means the corresponding branch will leave a good formula. From the two tables, we can see that direct analysis will get a bound of O (1.2600m) since the largest branching factor is 1.2600. This does not use amortization. Our deep analysis in the proof of theorem 1 shows that we can improve the bound to O (1.2226m).

6.1 F is a Bad Formula Case 1. F contains a (3, 4)-literal x: We branch on x into two branchings Fx and F x. The branching vector is (3, 4).

Case 2. F only contains (3, 3)-literals: We branch on an arbitrary literal x into two branchings Fx and F x. The branching vector is (3, 3). However, the two sub-instances in the two branchings are good formulas by Corollary 1.

6.2 F is a Good Formula Case 1. F contains a (3, 5+) or (4+, 4+)-literal x: Branch on x into two branchings Fx and F x. The branching vector will be at least (3, 5) or (4, 4).

Case 2. F contains a (3, 4)-literal (but no (3, 5+) or (4+, 4+)-literal): We further distinguish several cases to analyze the branching vector. Case 2.1. F also contains a (2, 3+)-literal y: We ﬁrst branch on an arbitrary (3, 4)-literal x into two branchings Fx and F x. If there is a clause containing both x and y, then in the branching Fx, the degree of y is at most 1. Thus y will become a (1, 1+)-literal or (0, 1+)-literal in Fx and we will further apply R-Rule 1 or 3 on y to decrease the number of clauses by at least 1. We can get a branching vector at least (4, 4). If there is a clause containing both x and y, then in the branching F x, the degree of y is at most 1. We apply R-Rule 1 or 3 on y to further decrease the number of clauses by at least 1. We can get a branching vector at least (3, 5). The remaining case is that the clauses containing x or x does not contain y. For this case, we can only get a branching vector (3, 4). However, in each branching of Fx and F x, the new instance is a good formula, because there is at least one (2, 0+)-literal y in them. Case 2.2. F contains only (3, 4)-literals, (4, 3)-literals and (3, 3)-literals: Let Y be the set of (4, 3)-literals x such that there is a clause containing both x and a (3, 3+)-literal. Case 2.2.1. Y = : There is a literal x Y and a clause containing x which does not contain any (4, 3)- literals, otherwise R-Rule 5 could be applied and F would not be a reduced instance. Thus the clause containing x will contain some (3, 3+)-literals. We branch on x with a branching vector (4, 3). By Lemma 8, we know that both branchings Fx and F x are good formulas. Case 2.2.2. Y = : For this case, (4, 3)-literals appear in clauses containing only (4, 3)-literals. Now Conditions (1) and (4) in the deﬁnition of bad formulas hold. Since F is a good formula now, we know either Condition (2) or Condition (3) will not hold. Thus there is either a 2-clause or a coincident pair. First, we assume that F contains a coincident pair {x, y}. If x is a (3, 4)-literal, then y must be a (3, 3+)-literal. For this case, we branch on x into two branchings Fx and F x. In the branching Fx, literal y becomes a (1, 1+)-literal or a (0, 1+)-literal and we can reduce the number of clauses by 1 by applying R-Rule 3 or R-Rule 1 on y. We get a branching vector (4, 4). If both of x and y are (3, 3)-literals, we branch on an arbitrary (3, 4)-literal with a branching vector (3, 4). Furthermore, in each branching, the instance is a good formula because there is either a coincident pair (x, y) or one of x and y becomes a literal of degree at most 2. The remaining case is that both of x and y are (4, 3)- literals. For this case, we branch on x into two branchings Fx and F x with a branching vector (4, 3). The formula Fx is good because literal y becomes a (2 , 1+)-literal. The formula F x is good by Lemma 8. Notice that for this case in F the clauses containing x cannot contain any (4, 3)-literal and then each of them must contain another (3, 3+)-literal. Second, we assume that F does not contain any coincident pair and there is a 2-clause {x, y}. We branch on x into two branchings Fx and F x. In the branching F x, we get a 1-clause containing only y. Furthermore, F x has at least two clauses containing y because y and x do not form

a coincident pair in F. We apply R-Rule 1 on y and can further decrease the number of clauses by at least 2. We get a branching vector at least (3, 5).

Case 3. F contains a (2, 3+)-literal (but no (3, 4+) or (4+, 3)-literal): Now F contains only (2, 3+)-literals, (3+, 2)-literals and (3, 3)-literals. We consider the following subcases. Case 3.1. There is a 2-clause C = {x, y} containing a (3+, 2+)-literal x: For this case, we can branch with a branching vector (3, 4) or (4, 3) leaving a good formula in each branching or a branching vector covered by one of (3, 5), (5, 3), and (4, 4). In this case, there exists a 2-clause and we will do deep analysis based on this special structure. The detailed analysis is omitted here due to the limited space. Some arguments are similar to that for the following Case 3.2. Case 3.2. There is a 2-clause C = {x, y} containing two (2, 3+)-literals: We consider two subcases. Case 3.2.1. There is no clause containing both of y and x: We branch on x. In the branching of Fx, literal y will become a (1 , 2+)-literal. We can reduce one more clause by applying R-Rule 3 on y. In the branching of F x, a 1clause {y} is created and there are two clauses containing y. We can reduce two more clauses by applying R-Rule 1 on y. We get a branching vector of (3, 5). Case 3.2.2. There is a clause D containing both of y and x: If D is also a 2-clause, then there are two 2-clauses {x, y} and { x, y}. We simply assign y = 1 without branching. Next, we assume that D is a 3+-clause. If D is a 3-clause, we branch on y. In the branching of Fy, literal x will become a (1 , 2+)-literal. We can reduce one more clause by applying R-Rule 3 on x. In the branching of F y, we will get two -clauses {x} and {z}, where z is the third literal in D. By applying R-Rule 1 on {x} and {z}, we can reduce two more clauses. We get a branching vector of (3, 5). Else D is a 4+-clause, and we branch on x. In the branching of Fx, literal y will become a (1, 2+)-literal. After applying R-Rule 3 on y, we reduce one more clause leaving a good formula, because D contains at least two literals other than y and x and then there is a coincident pair after applying R-Rule 3 on y. In the branching of F x, we will get a 1-clause {y}. We can reduce one more clause by applying R-Rule 1 on it. Same as before, if just 4 clauses are removed, the remaining instance is good. Thus, we can either get a branching vector (3, 4) with a good formula in each remaining branching or a branching vector covered by (3, 5). Next, we assume that there is no 2-clause. Case 3.3. There is a clause in F containing both a (3, 3)- literal x and a (2, 3+)-literal y: Let C1, C2 and C3 be the three clauses containing x, where we assume that C1 also contains y. Let C4 be the other clause containing y. We ﬁrst branch on x with a branching vector (3, 3). We may decrease the number of clauses more by applying reduction rules for different cases. Case 3.3.1. C4 = C2 or C4 = C3: This means {x, y} is a coincident pair. In the branching Fx, the literal y becomes

a (0, 2+)-literal. We can further remove at least two clauses by applying R-Rule 1 on y. We get a branching vector (5, 3). Next, we assume that C4 = C2 or C3. Case 3.3.2. C4 = C2 and C4 = C3: Notice that C2 and C3 are 3+-clauses and each of them will contain a literal different from {x, x, y, y}. In Fx, there is a (1, 1+)- literal y and two different (2 , 0+)-literals different from {x, x, y, y}. So it satisﬁes the condition in Lemma 9. After resolving y in Fx, we can further either reduce one clause leaving a good formula or reduce at least two clauses. In the branching of F x, we reduce three clauses directly and the remaining formula is good according to Corollary 1. So the branching vector is either (4, 3) with a good formula in each branching or a vector covered by (5, 3). Lemma 10. (*) For a reduced instance F without (3+, 4+)- literals, if there is no 2-clause and no clause contains both a (2, 3+)-literal and a (3, 3)-literal, then either there is no (2, 3+)-literal or there is a clause containing at least three (2, 3+)-literals. By Lemma 10, we know that the remaining case is that Case 3.4. There is a 3+-clause C containing at least three (2, 3+)-literals {x1, x2, x3}: Let Ci be the other clause containing xi (i = 1, 2, 3), where it is possible two of C1, C2 and C3 are the same. Case 3.4.1. Two literals in {x1, x2, x3}, say x1 and x2, form a coincident pair: We branch on x1 with a branching vector (2, 3) ﬁrst. In the branching of Fx1, literal x2 will become a (0, 3+)-literal and we reduce three clauses by applying R-Rule 1 on x2. So we can get a branching vector of (5, 3). Case 3.4.2. At least one of C1, C2 and C3 contains a negation of x1, x2 or x3: Without loss of generality we assume that C2 contains a negation of x1. We ﬁrst branch on x1 with a branching vector (2, 3). In the branching of Fx1, each of x2 and x3 will become a (1, 1+)-literal. We can further reduce the number of clauses by at least 2 by applying R-Rule 3 on x2 and x3 one by one. In the branching of F x1, after deleting the three clauses containing x1 (including C2), the degree of x2 is at most 1. We can reduce one more clause by applying reduction rules on x2. Thus, we can branch with a branching vector (4, 4). Case 3.4.3. None of Case 3.4.1 and Case 3.4.2 happens: We ﬁrst branch on x1 with a branching vector (2, 3). In the branching of Fx1, each of x2 and x3 will become a (1, 3+)- literal. We can reduce two more clauses by applying R-Rule 3 on x2 and x3 one by one. Furthermore, the remaining instance is a good formula, because applying R-Rule 3 will create coincident pairs in this case. In the branching F x2, the formula is a good formula by Corollary 1. We get a branching vector (3, 4) with a good formula in each branching.

Case 4. F contains only (3, 3)-literals: Since F is a good formula, we know that there is either a coincident pair or a 2-clause. Case 4.1. F contains a coincident pair {x, y}: We branch on x into two branchings Fx and F x, and distinguish two subcases to analyze the branching operation. Case 4.1.1. Three clauses contain x and y simultaneously: In the branching of Fx, the literal y will become a (0, 3)-

literal and we can further decrease the number of clauses by at least 3 by applying R-Rule 1. So we can get a branching vector (3, 6) at least. Case 4.1.2. Only two clauses contain x and y simultaneously: we assume without loss of generality that no pair of literals appear in more than two clauses simultaneously now. Assume that one of the clauses containing x is a 2-clause {x, w}, where w can be y. In the branching of Fx, we can apply R-Rule 3 on y to further reduce 1 clause. In the branching of F x, we apply R-Rule 1 on w to further reduce 1 clause. The branching vector will be covered by (4, 4). Next, we assume that any of the three clauses containing x also contains a literal other than y and y. At least two of the three literals are different because no pair of literals appear in three clauses as assumed. Let z1 and z2 be the two different literals. In Fx, literal y will become a (1, 1+)- literal and z1 and z2 will become (2 , 0+)-literals. The condition in Lemma 9 holds. After resolving y in Fx, we can either reduce 1 clause leaving a good formula or reduce at least 2 clauses. In the branching of F x, we reduce three clauses directly and the leaving formula is good according to Corollary 1. The branching vector is either (4, 3) with a good formula in each branching or a vector covered by (5, 3). Case 4.2. F does not contain a coincident pair but contains a 2-clause {x, y}: We branch on x with a branching vector (3, 3). In the branching F x, we will get a 1-clause that only contains y. Furthermore, since F does not contain a coincident pair, we know that there are at least two clauses containing y in F x. We can apply R-Rule 1 on y in F x to further reduce 2 clauses. Thus, we can get a branching vector covered by (3, 5).

7 Conclusion SAT is one of the most widely studied NP-complete problems. There is a large number of references in history, whether from the perspective of experimental algorithms or theoretical algorithms. Many fast solvers have been developed and they can solve medium-large sized instances within a reasonable running time bound. However, theoretical research is relatively backward. It took us decades to improve the running time bound to O (1.2226m). According to the theoretical results, the size of the problems we can solve is much smaller than that of the problems solved by fast practical solvers. The gap between theoretical and experimental results is large. It is interesting to further explore the problem nature and reduce the gap, especially to accelerate the research of theoretical algorithms and explain the fast experimental algorithms.

Acknowledgements The work is supported by the National Natural Science Foundation of China, under grants 61972070 and 61802049, and Sub Project of Independent Scientiﬁc Research Project, under grant ZZKY-ZX-03-02-04.

References Chen, J.; and Liu, Y. 2009. An Improved SAT Algorithm in Terms of Formula Length. In Algorithms and Data Struc-

tures, 11th International Symposium, WADS 2009, Banff, Canada, August 21-23, 2009. Proceedings, 144 155. Chu, H.; Xiao, M.; and Zhang, Z. 2020. An Improved Upper Bound for SAT. Co RR abs/2007.03829. URL https://arxiv. org/abs/2007.03829. Cook, S. A. 1971. The Complexity of Theorem-Proving Procedures. In Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, May 3-5, 1971, Shaker Heights, Ohio, USA, 151 158. Dantsin, E. 1983. Two systems for proving tautologies, based on the split method. Journal of Mathematical Sciences 22: 1293 1305. Dantsin, E.; Goerdt, A.; Hirsch, E. A.; Kannan, R.; Kleinberg, J. M.; Papadimitriou, C. H.; Raghavan, P.; and Sch oning, U. 2002. A deterministic (2-2/(k+1))n algorithm for k-SAT based on local search. Theor. Comput. Sci. 289(1): 69 83. Dantsin, E.; Hirsch, E. A.; and Wolpert, A. 2004. Algorithms for SAT Based on Search in Hamming Balls. In STACS 2004, 21st Annual Symposium on Theoretical Aspects of Computer Science, Montpellier, France, March 25-27, 2004, Proceedings, 141 151. Dantsin, E.; and Wolpert, A. 2004. Derandomization of Schuler s Algorithm for SAT. Electronic Colloquium on Computational Complexity (ECCC) (017). Davis, M.; and Putnam, H. 1960. A Computing Procedure for Quantiﬁcation Theory. J. ACM 7(3): 201 215. Fomin, F. V.; and Kratsch, D. 2010. Exact Exponential Algorithms. Texts in Theoretical Computer Science. An EATCS Series. Springer. Garey, M. R.; and Johnson, D. S. 1979. Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman. Gelder, A. V. 1988. A Satisﬁability Tester for Non-clausal Propositional Calculus. Inf. Comput. 79(1): 1 21. Hansen, T. D.; Kaplan, H.; Zamir, O.; and Zwick, U. 2019. Faster k-SAT algorithms using biased-PPSZ. In Proceedings of the 51st Annual ACM SIGACT Symposium on Theory of Computing, STOC 2019, Phoenix, AZ, USA, June 23-26, 2019, 578 589. Hirsch, E. A. 1998. Two New Upper Bounds for SAT. In Proceedings of the Ninth Annual ACM-SIAM Symposium on Discrete Algorithms, 25-27 January 1998, San Francisco, California, USA, 521 530. Hirsch, E. A. 2000. New Worst-Case Upper Bounds for SAT. J. Autom. Reasoning 24(4): 397 420. Impagliazzo, R.; and Paturi, R. 2001. On the Complexity of k-SAT. J. Comput. Syst. Sci. 62(2): 367 375. Kullmann, O.; and Luckhardt, H. 1997. Deciding propositional tautologies: Algorithms and their complexity. preprint 82. Monien, B.; and Speckenmeyer, E. 1985. Solving satisﬁability in less than 2n steps. Discrete Applied Mathematics 10(3): 287 295.

Monien, B.; Speckenmeyer, E.; and Vornberger, O. 1981. Upper bounds for covering problems. Methods of operations research 43: 419 431. Niedermeier, R.; and Rossmanith, P. 2003. An efﬁcient ﬁxed-parameter algorithm for 3-Hitting Set. Journal of Discrete Algorithms 1(1): 89 102. Paturi, R.; Pudl ak, P.; and Zane, F. 1997. Satisﬁability Coding Lemma. In 38th Annual Symposium on Foundations of Computer Science, FOCS 97, Miami Beach, Florida, USA, October 19-22, 1997, 566 574. Robinson, J. A. 1965. A Machine-Oriented Logic Based on the Resolution Principle. J. ACM 12(1): 23 41. Schuler, R. 2005. An algorithm for the satisﬁability problem of formulas in conjunctive normal form. J. Algorithms 54(1): 40 44. Wahlstr om, M. 2005. Faster Exact Solving of SAT Formulae with a Low Number of Occurrences per Variable. In Theory and Applications of Satisﬁability Testing, 8th International Conference, SAT 2005, St. Andrews, UK, June 19-23, 2005, Proceedings, 309 323. Yamamoto, M. 2005. An Improved O(1.234m)-Time Deterministic Algorithm for SAT. In Algorithms and Computation, 16th International Symposium, ISAAC 2005, Sanya, Hainan, China, December 19-21, 2005, Proceedings, 644 653.