Fast Algorithms for SAT with Bounded Occurrences of Variables

1 Introduction

The Boolean Satisfiability Problem (SAT) is the problem of testing propositional satisfiability for formulas in conjunctive normal form (CNF). As the first proved NP-complete problem [Cook, 1971], it has become one of the most foundational problems in computer science, AI, and math. SAT also has great applications in engineering. For these reasons, SAT and its variants are studied in a wide range of fields, such as heuristic algorithms, randomized algorithms, approximation algorithms, exact and parameterized algorithms, etc.

In exact algorithms, we are devoted to finding fast algorithms in which the correctness and the worst-case runningtime bound are theoretically guaranteed. These running-time bounds are beneficial to understand the computational complexity of NP-complete problems and the limitation of solving these problems. Also, the methodology behind exact algorithms can make an impact on practical solvers.

In this paper, we study exact algorithms for SAT, where one is asked to decide the satisfiability of a given CNF with n variables. For the general case where there are no restrictions on the input CNF, the trivial algorithm to enumerate all possible assignments runs in time O∗ (2n ). The first non-trivial bound O∗ (2n(1-1/α) ) where α = √n log n/2 was obtained in [Dantsin et al., 2004]. Later better bounds were achieved in [Schuler, 2005] and [Dantsin et al., 2006]. Despite decades of research, no algorithm in time O∗ (cn ) for some constant c < 2 was found. The Strong Exponential Time Hypothesis (SETH) [Impagliazzo and Paturi, 2001] conjectures that such an algorithm does not exist. There has also been considerable research on two other natural measures: the number of clauses in the formula m and the length of the formula L. There is a series of improvements in the running-time bounds measured by m and L, respectively. Recently, the results were improved to O∗ (1.2226m) [Chu et al., 2021] and O∗ (1.0646L) [Peng and Xiao, 2021].

Better bounds of O∗ (cn ) with c < 2 can be achieved for various restricted versions of SAT. One notable example is k-SAT, where every clause in the CNF is restricted to contain at most k literals. This problem is polynomial-time solvable for k = 2 and NP-complete for k ≥ 3. Regarding kSAT algorithms, two prevailing paradigms are local search algorithms, exemplified by Sch¨oning's algorithm [Sch¨oning, 1999], and random restriction algorithms, such as PPZ [Paturi et al., 1999] and PPSZ [Paturi et al., 2005]. Both paradigms have a running time of 2n(1-c/k+o(1/k)) , where c is specific to the algorithm. The study of 3-SAT is of independent interest and has a rich history of improvements. Currently, the fastest known algorithms for 3-SAT include a deterministic one with time complexity O∗ (1.32793n ) [Liu, 2018] and a probabilistic one with time complexity O∗ (1.30698n ) [Scheder, 2021].

Another restriction is limiting the occurrence of each variable in the formula to at most d, which is the main focus of this paper. This problem can be solved in linear time when d = 2 and becomes NP-complete when d ≥ 3 [Tovey, 1984]. Oliver and Luckhardt [1997] obtained a non-trivial bound O∗ (3n/9 ) ⊆ O∗ (1.1299n ) for the case d = 3. Subsequently, Wahlstr¨om [2005b] gave an improved O∗ (1.1279(d-2)n )- time algorithm for d ≥ 3. For d = 3 and 4, the algorithm runs in O∗ (1.1279n ) and O∗ (1.2721n ) time, respectively. These results are the best known for d = 3 and 4, and they have been utilized as sub-algorithms in several algorithms measured by the formula length L [Wahlstr¨om, 2005a; Chen and Liu, 2009; Peng and Xiao, 2021]. Specifically, they invoked Wahlstr¨om's algorithm when the maximum occurrence of variables is 3 or 4. Consequently, their focus narrows down to scenarios where there is a variable with at least 5 occurrences. We also remark that the cases d = 3 and 4 have become the bottleneck cases in these previous algorithms.

Our Contribution. In this paper, we show that SAT with each variable appearing at least twice in the formula can be solved in time O∗ (1.1238(d-2)n ) or O∗ (1.0641dn ), where d can be the average occurrences of variables in the formula. The first running-time bound implies the results of O∗ (1.1238n ) for d = 3 and O∗ (1.2628n ) for d = 4, which are the first improvements from Wahlstr¨om's results. Note that dn ≥ L. Our second running-time bound implies that SAT can be solved in time O∗ (1.0641L), slightly improving the previous result O∗ (1.0646L) [Peng and Xiao, 2021]. We consider our results for the cases d = 3 and 4 as the major contribution since our improvements for d ≥ 5 are also based on those for the cases d = 3 and 4. We summarize the previous and our results for d = 3 and 4 in Table 1.

Our algorithms follow the branch-and-search approach, similar to previous algorithms. In these algorithms, variables are typically dealt in descending order of their degrees, where the degree of a variable refers to the number of its occurrences in the formula. When the degree of a variable is large enough, we can get a good branch directly. On the other hand, a variable with degree at most 2 can be easily handled by reduction rules. The most challenging cases usually involve variables with degrees 3 and 4. In the previous algorithm for d = 3 and 4 [Wahlstr¨om, 2005b], the worst branch will generate a branching vector of (4, 8) (branching into two sub-branches: one reduces 4 degree-3 variables and one reduces 8 degree-3 variables), the corresponding complexity factor is 1.1279. In this paper, we improve the worst branching vector to (5, 7) (the corresponding complexity factor is 1.1238) through several techniques: (1) introducing new reduction rules, such as R-Rule 8 and R-Rules 12-14; (2) replacing some degree-4 variables with degree-3 variables, simplifying the handling of degree-4 case and avoiding one previous bottleneck; (3) using refined analyses to avoid previous bottlenecks in dealing with degree-3 variables and the remaining degree-4 variables.

For d ≥ 5, we adopt a general analytical framework to simplify the analysis, where we assign varying weights for variables based on their degrees to capture their contributions to the complexity. A key technique in this framework is the introduction of a tunable parameter in the weights, which allows us to derive different running-time bounds for the same algorithm by adjusting its value. Specifically, our dervied bound takes the form of O∗ (c(d-λ)n λ ), where λ is the tunable parameter, and cλ is a constant related to λ. For d = 3 and 4, the bound will be better by setting λ = 2, and for d ≥ 5, the bound will be better by setting λ = 0.

Other Related Work. We also mention the maximum satisfiability problem (MaxSAT), which is closely related to SAT. In MaxSAT, the objective is to satisfy the maximum number of clauses in a given CNF formula. The three parameters n, m, and L mentioned above were also considered for MaxSAT. For the number of variables n, the trivial bound O∗ (2n ) is also unlikely to break under SETH. For the number of clauses m and the length of the formula L, the bounds were recently improved to O∗ (1.2886m) [Xiao, 2022] and O∗ (1.0926L) [Alferov and Bliznets, 2021], respectively. There is also a series of results on the restricted version that the occurrence of each variable in the input CNF is at most d = 3. Since the first algorithm with running-time bound O∗ (1.732n ) [Raman et al., 1998] was proposed, the results were frequently improved: O∗ (1.3248n ) [Bansal and Raman, 1999], O∗ (1.27203n ) [Kulikov and Kutskov, 2009], O∗ (1.2600n ) [Bliznets, 2013], O∗ (1.237n ) [Xu et al., 2019], O∗ (1.194n ) [Xu et al., 2021], and O∗ (1.191n ) [Belova and Bliznets, 2020]. Very recently, Brilliantov et al. [2023] improved the result to O∗ (1.1749n ). Based on this result, they can improve the result evaluated by L to O∗ (1.0911L).

The proofs of lemmas and theorems marked with ♣ can be found in the full version of this paper.

2 Preliminaries

2.1 Notations

For a boolean variable x, it has two corresponding literals: the positive literal x and the negative literal x. We use x to denote the negation of a literal x and thus x = x. Given a set of variables V , a clause on V is a subset of literals on V , and a formula is set of clauses. 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, and a formula is satisfied by an assignment if all clauses in it are satisfied. A formula is satisfiable if it can be satisfied by at least one assignment.

A clause containing a single literal x may be simply written as x. We use C1C2 to denote the clause containing all literals in clauses C1 and C2. For a clause C, we use C to denote the set of negations of literals in C, and use C = 1 (resp., C = 0) to indicate that we assign 1 (resp., 0) to all literals in C. For a formula F, we denote FC=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 FC=0 = FC=1 .

In a formula F, 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. A literal z is pure if z is an (1+, 0)-literal. A variable x appears in a formula or a set of literals C if x or x is contained in C. For a variable or a literal x in formula F, the degree of it, denoted by deg(x), is the occurrences of x and x in F, i.e., deg(x) = i + j for an (i, j)-literal x or x. A variable x is a d-variable (resp., d+-variable) if deg(x) = d (resp., deg(x) ≥ d). The degree of a formula F, denoted by deg(F), is the maximum degree of all variables in F. For a clause or a formula C, the set of variables appearing in C is denoted by var(C). A formula F is d-regular if all variables in F are d-variables.

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 formula F is k-CNF if each clause in F has a length of at most k. A clause is a Pmonotone (resp., N-monotone) clause if it contains only positive (resp., negative) literals. A clause is a monotone clause if it is P-monotone or N-monotone. Otherwise, the clause is non-monotone. A monotone formula is a formula where each clause in it is monotone.

In a formula F, a literal x is called a neighbor of a literal z if there is a clause containing both z and x. The set of neighbors of a literal z in a formula F is denoted by N(z, F). We also use N (k) (x,F) (resp., N (k+) (z,F)) to denote the neighbors of z in k-clauses (resp., k+-clauses) in F, i.e., for any z′ ∈ N (k) (z, F) (resp., z′ ∈ N (k+) (z, F)), there exists a k-clause (resp., k+-clause) containing both z and z′ .

Resolution [Davis and Putnam, 1960] is a frequently used technique for SAT. For two clauses xC and xD in formula F, the resolvent of C and D by variable x is the clause CD. The resolvent CD is trivial if it contains both v and v for some literal v, or there is another clause E in F such that E ⊆ CD. We assume that duplicate literals in a resolvent are removed. A resolution on x in formula F is to construct a new formula DPx(F) by adding all non-trivial resolvents by x to F and removing all clauses containing variable x.

We assume that in the initial formula, each variable appears at least twice, although 1-variables may be generated during the algorithm. Note that 1-variables can be easily reduced but they may affect the average degree of the formula.

2.2 Branch-and-Search Algorithms

Our algorithm is a classical branch-and-search algorithm, which first applies reduction rules to reduce the instance and then searches for a solution by branching. We need to use a measure to evaluate the size of the search tree generated in the algorithm. Let µ be the measure and 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 µ. A branching operation, which branches on the instance into l branches with the measure decreasing by at least ai in the i-th branch, is usually represented by a recurrence relation

or simply 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(µ) = 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. We need to find the worst branching vector with the largest branching factor in the algorithm. We will frequently use the following property, which can be obtained from Lemmas 2.2 and 2.3 in [Fomin and Kratsch, 2010].

Lemma 1. The branching vector [∆0,∆1] is not worse than [q, p - q] if ∆0 + ∆1 ≥ p and min(∆0, ∆1) ≥ q.

2.3 The Measure

We use the measure-and-conquer method [Fomin et al., 2009] to analyze the running-time bound. Specifically, we introduce a weight to each variable according to its degree. Let w : Z+ → R+. We adopt the following measure of a formula F:

Let ni be the number of variables with a degree of i in the formula, L be the length of the formula, and d = L/n be the average occurrence of variables in the formula. We also introduce a tunable parameter λ ≥ 0 and restrict that wi ≤ i - λ for i > 1. The tunable parameter is important. For the same algorithm, we will get different running-time bounds under different values of the tunable parameter. Recalling our assumption that there are no 1-variables in the initial formula, thus n1 = 0 holds. For the initial formula F, we have

If we get a running-time bound of O∗ (cµ(F) ), then we also get a bound of O∗ (c(d-λ)n ). When λ = 0, the running-time bound will be O∗ (cdn ) = O∗ (cL).

Let δi = wi -wi-1 for i > 1. To guarantee that the measure does not increase during the algorithm and to simplify certain arguments, we impose some constraints on wi and λ:

Based on the above constraints, we have

With these constraints, we can see that once we determine the value of λ and w3, then we can determine all weights.

3 Reduction Rules

We have 15 reduction rules. When we introduce one we assume that all previous rules can not be applied.

R-Rule 1. F ′ ∧ xxC →F ′ ∧ xC.

R-Rule 2. F ′ ∧C ∧CD→F ′ ∧C.

R-Rule 3. F ′ ∧ xxC →F ′ .

R-Rule 4. If there is a 1-clause x or a (1+, 0)-literal x, then F → Fx=1.

R-Rule 5. If there is a variable x with deg(x) ≤ 4 such that the degree of each variable in DPx(F) is not greater than that in F, then F →DPx(F).

When none of the above rules is applicable, all variables in the formula are 3+-variables. R-Rules 6 to 9 are going to deal with some pairs of clauses containing two common variables.

R-Rule 6 ([Chen and Liu, 2009]). If there is a 2-clause xy and another clause xyC, then F ′ ∧xy∧xyC → F ′ ∧xy∧xC.

R-Rule 7 ([Peng and Xiao, 2021]). Let x be a (2+, 1)-literal. If there are clauses xyC1 and xyC2, then F ′ ∧ xyC1 ∧ xyC2 → F ′ ∧ xC1 ∧ xyC2.

R-Rule 8 (♣). Let x be a (2+, 1)-literal. If there are clauses xyC1 and xyC2, then F ′ ∧ xyC1 ∧ xyC2 → F ′ ∧ xyC2.

R-Rule 9 ([Chen and Liu, 2009]). If there are two clauses CD1 and CD2 such that |C| ≥ 2 and |D1|, |D2| ≥ 1, then F ′ ∧ CD1 ∧ CD2 → F ′ ∧ xC ∧ xD1 ∧ xD2, where x is a new 3-variable.

R-Rule 10 ([Chen and Liu, 2009]). If there is a 2-clause xy such that x and y are not both (1, 2)-literals and x is an (1, 2+)-literal, then replace x with y and apply R-Rule 3.

R-Rule 11. If there is a (2, 2)-literal x and four clauses xC1, xC2, xD1, and xD2, then F ′ ∧ xC1 ∧ xC2 ∧ xD1 ∧ xD2 → F ′ ∧ y1C1 ∧ y1C2 ∧ y2D1 ∧ y2D2 ∧ y1y2, where y1 and y2 are two new (2, 1)-literals.

R-Rule 11 is like the backward version of R-Rule 10. Note that our setting can avoid endless loops between them.

R-Rule 12 (♣). Let x, y1, · · · , yk (k ≥ 2) be (2+, 1)- literals. If there are clauses xy1C1, y1y2D1, · · · , yiyi+1Di, · · · , yk-1ykDk-1, and xykC2, then remove clause xy1C1.

R-Rule 13 (♣). Let x be a (2, 1)-literal. If there are clauses xyC1, xaC2, xC3, and D such that |C1| ≤ 1, and D = ya or D = yaC4 and literal a is a (2, 1)-literal, then F ′ ∧ xyC1 ∧ xaC2 ∧ D ∧ xC3 → F ′ ∧ aC1C2 ∧ yC1C3 ∧ D.

R-Rule 14 (♣). Let x, y, z, and a be (2, 1)-literals. If there are clauses xy, xa, yzb, zaC, and zD, then F ′ ∧ xy ∧ xa ∧ yzb ∧ zaC ∧ zD → F ′ ∧ abC ∧ xbD ∧ xa.

R-Rule 15. If there is a negative (2, 1)-literal x, then replace x with x to make it a positive (2, 1)-literal.

Definition 1. A formula is reduced if none of R-Rules 1-15 is applicable. We use R(F) to denote the reduced formula obtained by iteratively applying R-Rules 1-15 on F.

Lemma 2 (♣). For any formula F, applying any reduction rule on it will not increase the measure µ. Moreover, it takes polynomial time to obtain R(F) from F.

Lemma 3 (♣). In a reduced formula, there are no (i, 0)- literals and all variables are 3+-variables.

Lemma 4 (♣). In a reduced formula, if there is a 2-clause xy, then no other clause contains xy, xy, or xy. Moreover, if x is a (2+, 1)-literal, then no other clause contains xy.

Lemma 5 (♣). In a reduced formula, any two clauses contain at most one common 3-variable.

Lemma 6 (♣). In a reduced 3-regular formula, the two literals in any 2-clause are both negative (1, 2)-literals or both positive (2, 1)-literals.

Lemma 7 (♣). Let C = xy be a 2-clause that contains two negative (1, 2)-literals in a reduced 3-regular formula. It holds that var(N(x, F)) ∩ var(N (2) (y, F)) = ∅.

4 Main Algorithm

After obtaining a reduced formula by applying reduction rules, we apply branching rules. We have six branching steps.

The worst cases of the branching vectors in each step are listed in Table 2. Recall that we have a tunable parameter λ in the weights. We will use the results for λ = 2 and 0. The responding branching factors are also given in Table 2.

Before going into the detailed branching steps, we first introduce some lower bounds on the decrease of measure in two frequently-used branchings. We use the following notations.

Definition 2. For a literal x in a formula F, we define

• pi(x) = |{y : y ∈ N(x, F) and deg(y) = i}| and
• qi(x) = |{y : y ∈ N (2) (x, F) and deg(y) = i}|.

In other words, pi(x) is the number of literals with a degree of i in N(x,F), and qi(x) is the number of literals with a degree of i in N (2) (x, F).

The following two lemmas can be easily obtained from Lemmas 6 and 9 in [Peng and Xiao, 2021]. We remark that the conditions of the two lemmas also hold in our algorithm.

Lemma 8 (♣). Let x be a literal of a d-variable in a reduced formula F where deg(F) = d. It holds that ∆ = µ(F) - µ(R(Fx=1)) ≥ wd + ∑di=3 pi(x)δd.

Lemma 9 (♣). Let x be a literal of a d-variable in a reduced formula F such that deg(F) = d, and ∆1 = µ(F) - µ(R(Fx=1)) and ∆0 = µ(F) - µ(R(Fx=0)). It holds that ∆1 + ∆0 ≥ 2wd + 2dδd + ∑di=3 (qi(x) + qi(x))(2w3 - 2δd).

The following lemma will be frequently used.

Lemma 10 (♣). Let x be a (d - 1, 1)-literal in a reduced formula F with d = deg(F) ≥ 4. Assume that the clauses containing x or x are xC1, · · · , xCd-1 and xD. It is safe to branch with (1) x = 1 ; (2) x = 0 and D = 0. Let ∆1 = µ(F) - µ(R(Fx=1)) and ∆0 = µ(F) - µ(R(Fx=0&D=0)). It holds that ∆1 + ∆0 ≥ 2wd + (2d - 3)δd + 3w3 and min(∆1, ∆0) ≥ wd + min((d - 1)δd, 2w3 + δd).

4.1 Step 1: 6+-variables

If there is a 6+-variable in the formula, we pick up a variable x of maximum degree and branch with (1) x = 1; (2) x = 0.

We show that the branching vector is not worse than (w6 + 1, w6+11). Let d = deg(x) ≥ 6, ∆1 = µ(F)-µ(R(Fx=1)), and ∆0 = µ(F) - µ(R(Fx=0)). Note that δd = δ6 = 1 since d ≥ 6. By Lemma 9, we have ∆1 + ∆0 ≥ 2wd + 2dδd ≥ 2w6 + 12. By Lemma 8, we have ∆1 ≥ wd + ∑di=3 pi(x)δd ≥ w6+1 since ∑di=3 pi(x) ≥ 1. Similarly, we have ∆0 ≥ w6 + 1. Thus, min(∆1, ∆0) ≥ w6 + 1. Together with ∆1+∆0 ≥ 2w6+12, we know that the branching vector is not worse than (w6 + 1, w6 + 11) by Lemma 1.

4.2 Step 2: 4-variables and 5-variables

In this step, we deal with 4-variables and 5-variables. Note that all (2, 2)-literals are reduced by R-Rule 11.

Step 2.1: If there is a (4, 1)-literal x, where xD is assumed to be the unique clause containing x, then branch with (1) x = 0 and D = 0; (2) x = 1. Let ∆1 = µ(F)-µ(R(Fx=1)) and ∆0 = µ(F) - µ(R(Fx=0&D=0)). By Lemma 10, we know that ∆1 +∆0 ≥ 2w5 +7δ5 +3w3 and min(∆1, ∆0) ≥ w5 +min(4δ5, 2w3 +δ5) ≥ w5 +2w3 since w3 < 2δ5. Thus, the branching vector is not worse than (w5 +2w3, w5 +w3 + 7δ5) by Lemma 1.

Step 2.2: If there is a (2, 3)-literal x, then branch with (1) x = 1; (2) x = 0. Let ∆1 = µ(F) - µ(R(Fx=1)) and ∆0 = µ(F) - µ(R(Fx=0)). We consider two cases.

Case 1: There is at least one 2-clause containing x or x, i.e., ∑5i=3 (qi(x) + qi(x)) ≥ 1. By Lemma 9, we have ∆1+∆0 ≥ 2w5+10δ5+∑5i=3 (qi(x)+qi(x))(2w3-2δ5) ≥ 2w5 + 2w3 + 8δ5. By Lemma 8, we have ∆1 ≥ w5 + ∑5i=3 pi(x)δ5 ≥ w5 + 2δ5 and ∆0 ≥ w5 + ∑5i=3 pi(x)δ5 ≥ w5 + 3δ5 since x is a (2, 3)-literal. Thus min(∆1,∆0) ≥ w5 + 2δ5. Together with ∆0 + ∆1 ≥ 2w5 + 2w3 + 8δ5, we know that the branching vector is not worse than (w5 + 2δ5, w5 + 2w3 + 6δ5) by Lemma 1.

Case 2: All clauses containing x or x are 3+-clauses. Then we have ∑5i=3 pi(x) ≥ 4 and ∑5i=3 pi(x) ≥ 6. It follows that ∆1 ≥ w5 + 4δ5 and ∆0 ≥ w5 + 6δ5 by Lemma 8. Thus, the branching vector is not worse than (w5 + 4δ5, w5 + 6δ5).

Step 2.3: If there is a (3, 1)-literal x, where xD is assumed to be the unique clause containing x, then we branch with (1) x = 0 and D = 0; (2) x = 1. The branching vector is not worse than (5w3, 7w3). Let ∆1 = µ(F) - µ(R(Fx=1)) and ∆0 = µ(F) - µ(R(Fx=0&D=0)). By Lemma 10 we know that ∆1 + ∆0 ≥ 2w4 + 5δ4 + 3w3 = 12w3 and min(∆1,∆0) ≥ w4 + min(3δ4, 2w3 + δ4) = 5w3 since w4 = 2w3 and δ4 = w3. Thus, the branching vector is not worse than (5w3, 7w3) by Lemma 1.

4.3 3-regular Formula (Steps 3-6)

Now the formula is a reduced 3-regular formula. Moreover, all positive literals appear twice and all negative literals appear once in the formula since R-Rule 15 is not applicable. The removal of any literal of a 3-variable will make it a 2variable, and reduction rules will reduce the 2-variable. So when a literal of a 3-variable is removed, we will regard this variable as reduced. This property will be frequently used. We have four steps to deal with different cases.

Step 3: Good N-monotone 2-clauses

Assume that there is an N-monotone 2-clause xy. There is no other clause that contains both x and y by Lemma 5. Let the four clauses containing x and y be xC1, xC2, yC3, and yC4, where we also assume, w.l.o.g., that |C1| ≤ |C2|, |C3| ≤ |C4|, and |C1| ≤ |C3|.

An N-monotone 2-clause xy is called good if it holds at least one of the following conditions: (i) |C1| ≥ 2; (ii) |C1| = |C3| = 1; (iii) |C1| = 1 and |C2|, |C3| ≥ 2; (iv) |C1| = |C2| = 1, |C3| = 2, and |C4| ≥ 3; (v) There is a negative (1, 2)-literal in N(x, F) or N(y, F). Thus, if xy is not good, then it holds that |C1| = |C2| = 1, |C3| = |C4| = 2, and all clauses containing x or y are P-monotone.

This step is going to deal with good N-monotone 2-clauses if they exist. Let xy be a good N-monotone 2-clause. We branch with (1) x = 1 and y = 0; (2) x = 0 and y = 1.

Lemma 11. The branching vector generated by Step 3 is not worse than (5w3, 7w3).

Proof. We denote ∆1 = µ(F) - µ(R(Fx=1&y=0)) and ∆0 = µ(F) - µ(R(Fx=0&y=1)). Let tx and ty be the number of 2-clauses containing literal x and literal y, respectively. In the branch x = 1 and y = 0, all variables in var(C1) and var(C2) are reduced, and all literals in N (2) (y, F) will get assignment by R-Rule 4 since the clauses containing them become 1-clauses. By Lemma 5, we have {x, y} ∩ (var(C1C2) ∪ var(C3C4)) = ∅. By Lemma 7, we know that var(C1C2) ∩ var(N (2) (y, F)) = ∅. So the number of reduced variables is at least |{x, y}| + |var(C1C2)| + |var(N (2) (y, F))| = 2 + |C1| + |C2| + ty, and then we have

Similarly, in the branch x = 0 and y = 1, we have

Thus, it holds that ∆0+∆1 ≥ (4+∑4i=1 |Ci|+tx+ty)w3 ≥ (4 + ∑4i=1 max(|Ci|, 2))w3 ≥ (4 + 8)w3 = 12w3 since that for each Ci, it contributes to ∆0 + ∆1 at least 2w3 when |Ci| = 1 and at least |Ci|w3 when |Ci| ≥ 2.

We first claim that if at least one of conditions (i)-(iii) is satisfied, then we have min(∆0,∆1) ≥ 5w3, which is sufficient to get a branching vector not worse than (5w3, 7w3) since ∆0 +∆1 ≥ 12w3 by Lemma 1. If condition (i) is satisfied, we have |C2| ≥ |C1| ≥ 2 and |C4| ≥ |C3| ≥ |C1| ≥ 2. It holds that ∆1 ≥ (2+|C1|+|C2|)w3 ≥ 6w3 and ∆0 ≥ (2+ |C3| + |C4|)w3 ≥ 6w3. Thus, we have min(∆0, ∆1) ≥ 6w3. If condition (ii) is satisfied, we have tx ≥ 1 and ty ≥ 1. It holds that ∆1 ≥ (2 + |C1| + |C2| + ty)w3 ≥ 5w3 and ∆0 ≥ (2 + |C3| + |C4| + tx)w3 ≥ 5w3. And then we have min(∆0,∆1) ≥ 5w3. If condition (iii) is satisfied, we have |C1| = 1, |C2| ≥ 2, and |C4| ≥ |C3| ≥ 2. It holds that ∆1 ≥ (2 + |C1| + |C2|)w3 ≥ 5w3 and ∆0 ≥ (2 + |C3| + |C4|)w3 ≥ 6w3. Then we have min(∆0, ∆1) ≥ 5w3.

If condition (iv) is satisfied, we have tx = 2. Then it holds that ∆1 ≥ (2 + |C1| + |C2|)w3 = (2 + 1 + 1)w3 = 4w3 and ∆0 ≥ (2 + |C3| + |C4| + tx)w3 ≥ (2 + 2 + 3 + 2)w3 = 9w3. Thus the branching vector is not worse than (4w3, 9w3), which is better than (5w3, 7w3).

Next, we assume that only condition (v) is satisfied. This will be the hardest case. We have |C1| = |C2| = 1, |C3| = |C4| = 2, and tx = 2, and we show the branching vector is not worse than (4w3, 9w3).

By Lemma 6 and |C1| = |C2| = 1, we know that both xC1 and xC2 are P-monotone, and thus we can assume, w.l.o.g, that C3 = zα, where z is a negative (1, 2)-literal and α is an (1, 2)/(2, 1)-literal by the condition (v). In the branch x = 1 and y = 0, we have ∆1 ≥ (2+|C1|+|C2|)w3 = 4w3. In the branch x = 0 and y = 1, based on the previous analysis, we can first get ∆0 ≥ (2 + |C3| + |C4| + tx)w3 = 8w3, where only variables in S = {x, y}∪var(C1C2)∪var(C3C4) were taken into consideration. We show that we can further reduce one more variable besides S to get ∆0 ≥ 9w3.

After assigning x = 0 and y = 1, literal z becomes pure. We can assign z = 1 by R-Rule 4 and further reduce var(N(z,F)). Let zE1 and zE2 be the two clauses containing litearl z, i.e., N(z,F) = E1E2. By Lemma 7, we have x /∈ E1E2. By Lemma 5, we have y /∈ E1E2 and var(E1E2) ∩var(C3) = ∅. Let v be a positive (2, 1)-literal in C1C2. We can apply R-Rule 14 if v ∈ E1E2 and apply R-Rule 12 in the case of k = 3 if v ∈ E1E2. So we have var(C1C2) ∩ var(E1E2) = ∅. If |var(E1E2)\var(C4)| ≥ 1, then we can reduce at least |S ∪ var(Nz)| = |{x, y}| + |var(C1C2)| + |var(C3C4)| + |var(E1E2) \ var(C4)| ≥ 2 + 2 + 4 + 1 = 9 variables. Next, we assume var(E1E2) ⊆ var(C4) and show that we still can further reduce one more variable besides S.

We have |E1| = |E2| = 1 since var(E1E2) ⊆ var(C4) and |C4| = 2. Let var(C4) = {a, b} and assume, w.l.o.g., that E1 = a and E2 = b since that both zE1 and zE2 are P-monotone by Lemma 6. If both literals in C4 are negative (1, 2)-literals, then R-Rule 13 should be applicable. If there is only one negative (1, 2)-literal in C4, say a, then DPa(F) satisfies the requirement of R-Rule 5. Thus, both literals in C4 are positive (2, 1)-literals, i.e., C4 = ab. Let aG1 and bG2 be the clauses containing a and b. We can reduce variables in var(G1G2) by assigning a = b = 1 since they become pure after assigning x = 0, y = 1, and z = 1. Recall that C3 = zα and a is a positive (2, 1)-literal contained in za. We can apply R-Rule 13 if α ∈ G1G2 and R-Rule 12 in the case of k = 2 if α ∈ G1G2. With Lemma 5, we have var(G1G2) ∩ ({x, y} ∪ var(C3C4)) = ∅. If |G1| = 1, then aG1 is an N-monotone 2-clause by Lemma 6, and it satisfies one of conditions (i)-(iv) since that there are clauses za and yab. Thus, we have |G1| ≥ 2, and similarly, |G2| ≥ 2. This together with Lemma 5 yields that |var(G1G2)| ≥ 3. So we have |var(G1G2)\var(C1C2)| ≥ 1 since |var(C1C2)| = 2. Therefore, in the case var(E1E2) ⊆ var(C3C4), we can reduce at least |S∪var(G1G2)| ≥ |{x, y}|+|var(C1C2)|+ |var(C3C4)|+var(G1G2)\var(C1C2) ≥ 2+2+4+1 = 9 variables. This completes the proof.

Step 4: Making the Formula Monotone

In this step, we pick up a positive literal x in a non-monotone clause C (if it exists) and branch on x. We will show that the branching vector is not worse than (6w3, 6w3).

Lemma 12 (♣). Let C be a non-monotone clause in a reduced formula after Step 3. If there is a positive literal y ∈ C, then y is contained in a 3+-clause.

Lemma 13 (♣). Let F be a reduced formula after Step 3 and xD be a non-monotone clause in F containing a positive literal x. Then it holds that ∆ = µ(F)-µ(R(Fx=1)) ≥ 6w3.

Lemma 14 (♣). Let F be a reduced formula after Step 3 and xC ′ be a 3+-clause in F containing a negative literal x. It holds that ∆ = µ(F) - µ(R(Fx=0&C′=0)) ≥ 6w3.

Let C = xD be a non-monotone clause containing positive literal x and xC ′ be the clause containing x. In this step, we will branch with (1) x = 1; (2) x = 0 and C ′ = 0. Equipped with Lemmas 13 and 14, we can show the branching vector is not worse than (6w3, 6w3). In the first branch, we can reduce the measure by at least 6w3 by Lemma 13. In the second branch, we have |C ′ | ≥ 2 by Lemma 12 and then we can also reduce the measure by at least 6w3 by Lemma 14.

Step 5: Making the Formula 3-CNF

Now, the formula is monotone. In this step, we are going to deal with N-monotone clauses of length at least 4 and some N-monotone clauses of length 3.

Step 5.1: If there is an N-monotone clause C = v1v2 · · · vk with k ≥ 4, then branch with (1) v1 = · · · = v⌈k/2⌉ = 0; (2) v⌈k/2⌉+1 = · · · = vk = 0. This branch is correct because all the literals in C are (1, 2)-literals and we only need to let one of them be 1 and all others 0. We show that the branching vector is not worse that (6w3, 6w3). The proof is based on the following property.

Lemma 15 (♣). Let C be an N-monotone 4+-clause in a formula F after Step 4, and C ′ = v1 · · · vr be any subset of C of r ≥ 2 literals. We have ∆ = µ(F)-µ(R(FC′=0)) ≥ 6w3.

Based on Lemma 15, we know that Step 5.1 can always generate a branching vector not worse that (6w3, 6w3). Since Step 5.1 deals with N-monotone 4+-clauses, next we assume that each N-monotone clause in F is a 2-clause or 3-clause.

Lemma 16 (♣). Let C be an N-monotone 3-clause in a reduced formula F after Step 5.1. For any two negative literals y and z in C, it holds that |var(N(y,F) ∪N(z,F))| ≥ 4.

Step 5.2: Assume there is an N-monotone 3-clause xyz such that |C1| + |C2| ≥ 3 for the two clauses xC1 and xC2 containing x. In this step, we select a literal x such that |C1|+ |C2| is maximized, and branch with (1) x = 1; (2) x = 0 and y = z = 1.

Lemma 17. The branching vector generated by Step 5.2 is not worse than (5w3, 7w3).

Proof. Let ∆1 = µ(F) - µ(R(Fx=1)), ∆0 = µ(F) - µ(R(Fx=0&y=z=1)), and Nyz = N(y, F) ∪ N(z, F).

Case 1: |C1|+|C2| ≥ 4. In the branch x = 1, all variables in C1 and C2 are reduced. Together with x, we can reduce at least 5 variables. In the branch x = 0 and y = z = 1, all variables in var(Nyz) are reduced. By Lemma 16, we know that |var(Nyz)| ≥ 4. Additionally, Lemma 5 guarantees that var(Nyz) ∩ x, y, z = ∅. In this branch, we reduce at least |{x, y, z}| + |var(Nyz)| ≥ 7 variables in total. Thus, we can branch with (5w3, 7w3) at least.

Case 2: |C1| + |C2| = 3. W.l.o.g., we assume C1 = a and C2 = bc. We show that the branching vector is not worse than (4w3, 9w3), which is better than (5w3, 7w3). In the branch x = 1, at least 4 variables a, b, c, and x are reduced.

In the branch x = 0 and y = z = 1, we can further assign a = 1. Let aD be the other one clause containing literal a. Then D will also be reduced after we assign a = 1. To sum up, we can reduce variables in {x, y, z, a} ∪ var(Nyz) ∪ var(D). We have {x, y, z}∩var(D) = ∅ and a /∈ Nyz since R-Rule 13 is not applicable. Note that |var(Nyz)| ≥ 4, and {x, y, z} ∩ var(Nyz) = ∅ by Lemma 5. We can reduce at least |{x, y, z, a} ∪ var(Nyz) ∪ var(D)| = |{x, y, z, a}| + |var(Nyz)|+|var(D)\var(Nyz)| ≥ 9 variables if |var(D)\ var(Nyz)| ≥ 1 or |var(Nyz)| ≥ 5, and thus ∆0 ≥ 9w3. Next, we show that we can still reduce 9 variables at least if |var(Nyz)| = 4 and var(D) ⊆ var(Nyz).

Let yE1, yE2, zE3, and zE4 be the four clauses containing literal y or z. According to the choice of x, we know that |E1| + |E2| ≤ |C1| + |C2| = 3 and so |E1| = 1 or |E2| = 1. Similarly, |E3| = 1 or |E4| = 1. W.l.o.g., we assume that |E1| = |E3| = 1. It holds that var(E1) ̸= var(E3) and var(E1E3)∩var(E2E4) = ∅ otherwise R-Rule 13 would be applicable. Since |var(E1E2E3E4)| = |var(Nyz)| = 4, we have |var(E2E4)| = |var(E1E2E3E4)|-|var(E1E3)| = 2. If |E2|, |E4| ≥ 2, then |var(E2E4)| ≥ 3 by Lemma 5, which is a contradiction. So we can assume, w.l.o.g., that |E2| = 1 and 1 ≤ |E4| ≤ 2. If |E2| = 1 and |E4| = 2, then we have var(E2) ∩ var(E4) = ∅, otherwise R-Rule 13 is applicable. However, this implies a contradiction that |var(E2E4)| = |E2| + |E4| ≥ 3. Thus, we have |E2| = |E4| = 1. Let u be a literal in D. We know that u becomes pure after assigning x = 0 and y = z = 1 since that D and Nyz only contain positive literals, and u appears in both of them. So we can further assign u = 1 in this branch. Assume that the clause containing literal u is uvw, variables v and w are also reduced by u = 1. Since |Ei| = 1 for 1 ≤ i ≤ 4, we can apply R-Rule 13 if {v, w} ⊆ var(Nyz). So we have |{v, w} \ var(Nyz)| ≥ 1. Clearly, {v, w} ∩ {x, y, z, a} = ∅. As a result, we can reduce at least |{x, y, z, a} ∪ var(Nyz) ∪ {v, w}| = |{x, y, z, a}| + |var(Nyz)| + |{v, w} \ var(Nyz)| ≥ 9 variables, and so we have ∆1 ≥ 9w3 in this case. This completes the proof.

Lemma 18 (♣). After Step 5, all clauses have a length ≤ 3.

Lemma 18 implies that the formula after Step 5 is a 3-CNF.

Step 6: Fast Solving the Remaining Part

Next, we call a fast 3-SAT algorithm by Beigel and Eppstein to solve our problem directly.

Lemma 19 ([Beigel and Eppstein, 2005]). 3-SAT can be solved in time O∗ (1.3645t ) and polynomial space, where t is the number of 3-clauses.

Lemma 20. Step 6 can be solved in O∗ ((1.1092 1 w3 )µ(F) ) time and polynomial space.

Proof. Let m2 be the number of N-monotone 2-clauses, m3 be the number of N-monotone 3-clauses, and m3 be the number of P-monotone 3-clauses in the formula. Note that the number of 3-clauses in F is m3 +m3. Since the formula is monotone now and all negative literals appear once, we know that the number of variables is n = 2m2 + 3m3.

For an N-monotone 3-clause in F, say xyz, all clauses containing literal x/y/z are 2-clauses after Step 5.2. So, we can know that for a P-monotone 3-clause, say abc, all clauses containing literal a/b/c are 2-clauses. After Step 3, for an N-monotone 2-clause xy in F, there are two P-monotone 2-clauses and two P-monotone 3-clauses containing x or y. Thus, we can know that m3 = 2m2/3, and so we have

Then, by calling Beigel and Eppstein's algorithm, we can solve the problem in time O∗ (1.3645 n3 ) ⊆ O∗ (1.1092n ). Finally, since the formula is 3-regular, we have µ(F) = w3n and O∗ (1.1092n ) ⊆ O∗ ((1.1092 1 w3 )µ(F) ).

5 The Final Results

Now we present our main results. The algorithm will first apply the reduction rules to get a reduced formula and then apply the six branching steps in order. The worst branching vectors for each branching step are summarized in Table 2. Note that these worst branching vectors are not related to the value of the tunable parameter λ as long as 0 ≤ λ ≤ 2.

By setting λ = 2 and w3 = 1, we have µ(F) ≤ (d - 2)n and wi = i - 2 for i ≥ 3. The biggest branching factor for the first five steps is 1.1238, which is corresponding to the branching vector (5w3, 7w3) in Steps 2.3, 3, and 5.2. Since w3 = 1, Step 6 can be solved in time O∗ (1.1092µ(F) ). Thus, the whole instance can be solved in time O∗ (1.1238(d-2)n ).

Theorem 1. SAT without 1-variables can be solved in O∗ (1.1238(d-2)n ) time and polynomial space.

By setting λ = 0 and w3 = 1.87884, we have µ(F) ≤ dn, w4 = 3.75768, and wi = i for i ≥ 5. The biggest branching vector for the first five steps is 1.0641, and the bottlenecks are Steps 2.2, 2.3, 3, and 5.2. Under this setting, Step 6 can be solved in time O∗ (1.0568µ(F) ), and the whole instance can be solved in time O∗ (1.0641dn ). Since L = dn, we get that:

Theorem 2. SAT can be solved in O∗ (1.0641dn ) time (resp., O∗ (1.0641L) time) and polynomial space.

6 Conclusion

In this paper, we study the running-time bounds for SAT with the average occurrence of variables bounded by d. The results for d = 3 and 4, which were frequently used in other algorithms, have not been improved for a long time. One reason why it is hard to improve is that several cases will lead to the same bottleneck. In this paper, by using new reduction and branching techniques, we successfully avoid all the previous bottlenecks.

Another interesting technique is that we set a tunable parameter λ in our variable weights. By setting different values to the tunable parameter, we get different running-time bounds for the same algorithm with the same analysis framework. When the tunable parameter λ is smaller, more improvements for small d may propagate to that for large d. When λ reaches the upper bound 2, we get the best results for d = 3 and 4. When λ = 0, the running-time bound for d ≥ 5 becomes better. This analysis technique may be able to apply to more problems.

Acknowledgements

The work is supported by the National Natural Science Foundation of China, under grant 61972070, and the Natural Science Foundation of Sichuan Province of China, under grant 2023NSFSC0059.