Complementary Branching for #SAT: Bounded-Degree Bounds and Faster #3-SAT

1 Introduction

The Boolean Satisfiability problem (SAT), the first problem shown to be NP-complete [Cook, 1971], is at the heart of many artificial intelligence tasks and applications. Its counting variant, the Propositional Model Counting problem (#SAT) is the problem of determining the number of satisfying assignments of a given formula. It was introduced and shown to be #P-complete by Valiant [Valiant, 1979]. Exact and approximate model counting are the backbone in probabilistic inference and graphical models [Chavira and Darwiche, 2008], probabilistic databases and probabilistic logic programming [Belle, 2017], knowledge compilation and exact inference [Darwiche and Marquis, 2002], planning and reasoning [Speck et al., 2025], cryptographic security analysis [Beck et al., 2020], and neuro-symbolic reasoning [Manhaeve et al., 2021]. The wide range of applications has led to the creation of dedicated model counting competitions [Fichte et al., 2021; Fichte and Hecher, 2025].

Not surprisingly, the design of fast algorithms for satisfiability problems has been a major research topic in the past decades. For Boolean formulas in conjunctive normal form (CNF), the three main satisfiability problems are decision SAT, its optimization extension Max-SAT, and the counting variant #SAT. A na¨ıve algorithm for each of the problems runs in time O∗ (2n ) by explicitly evaluating all possible 2n variable assignments. Under the Strong Exponential Time Hypothesis [Calabro et al., 2009], general SAT cannot be solved in time O(cn ) for some constant c < 2. Thus, the focus has been on structural parameters of the underlying CNF instances, for which sub-2n algorithms can be designed.

Two natural parameters are the clause width k (maximum number of literals per clause) and the clause density δ = m/n (ratio of clauses to variables). For decision SAT, many algorithms have been designed that run significantly faster than 2n for fixed k [Paturi et al., 1997; Dantsin et al., 2002]. Density-parameterized bounds can be obtained via a technique called width reduction [Schuler, 2005] to k-SAT algorithms. [Calabro et al., 2006] established a duality between the width and density parameters for decision SAT and showed that SAT with density δ reduces to k-SAT for k = O(log δ).

This is not the case for Max-SAT and #SAT. It is an open question if Max-k-SAT can be solved in less than 2n steps for fixed k but there are many algorithms for general CNF instances that run in time O∗ (2n(1- 1 f(δ) ) ) for some monotonically growing function f. On the contrary, #k-SAT is trivially solvable in time O∗ (cnk ), for ck < 2, but the values ck are too large for width reduction to work, and almost no #SAT algorithms have been specifically designed for sparse instances. This is perhaps surprising given the practical importance of sparse formulas as evident in model counting competitions [Fichte et al., 2021; Fichte and Hecher, 2025].

Our Contribution. We present complementary branching, a branching approach for model counting based on the complement counting equality #(F ∧ G) = #F - #(F ∧ ¬G). By negating a CNF subformula we obtain a DNF, which can then be naturally branched on. This allows branching on subformulas rather than individual variables, and proves particularly effective when variables of low degree appear in long clauses as we can assign many variables at once.

As a main application of complementary branching, we design a novel #SAT algorithm for CNF formulas of bounded variable degree ∆ and no restriction on clause width. The algorithm runs in time O∗ (2(1- 1 3D )n ) for D = max(∆, 3) and can be extended to solving #SAT for formulas with density δ = m/n in time O∗ (2(1- 1 cδ )n ) for some constant c > 0.

As a second application, we extend complementary branching to a variation of clause learning. By applying it to several tight cases in the analysis from [Kutzkov, 2007], we improve the upper bound for #3-SAT from O∗ (1.6423n ) to O∗ (1.637n ). While incremental, this is the first improvement to the bound in nearly two decades.

2 Notation and Definitions

A Boolean variable (or simply variable) can take the value 1 (True) or 0 (False). For a variable x, the positive literal is x and the negative literal is ¯x. The sign of a literal is denoted by sign(·), with sign(x) = 1 and sign(¯x) = 0.

A clause is a disjunction (OR) of literals. A CNF formula (Conjunctive Normal Form) is a conjunction (AND) of clauses, while a DNF formula (Disjunctive Normal Form) is a disjunction of conjunctions of literals.

The negation of a Boolean formula F is denoted by ¬F. Note that, in general, the negation of a CNF formula is a DNF formula, and vice versa.

For a formula F, we denote by var(F) the set of variables in F . Let n = |var(F )| be the number of variables and m the number of clauses. The density of F is defined as

For a clause C, var(C) denotes the set of variables that occur in C.

An assignment for a variable set V is a mapping σ : V → {0, 1}. A literal x is satisfied by σ if σ(x) = 1, and ¯x is satisfied if σ(x) = 0. A clause is satisfied if at least one of its literals is satisfied. An assignment σ is a model of a formula F if it satisfies all clauses in F, which we denote by σ |= F.

For a variable x ∈ var(F ), we write F [x = 1] and F [x = 0] for the formulas obtained from F by setting x to 1 and 0, respectively. We also define

Fa = {C ∈ F : a ∈ var(C)} and F-a = {C ∈ F : a /∈ var(C)}, i.e., Fa is the subformula of F consisting of the clauses that contain a, and F-a is the subformula consisting of the clauses that do not contain a.

Definition 1 (#SAT). Given a Boolean formula F, the #SAT problem asks for the number of satisfying assignments of F, that is

Definition 2 (#k-SAT). For an integer k ≥ 2, the #k-SAT problem is the restriction of #SAT to formulas in k-CNF, i.e., CNF formulas where each clause has at most k literals.

In the weighted variant, each literal is assigned a positive weight, the weight of an assignment is the product of its literal weights and the weighted model count of a formula is the sum of the weights of all satisfying assignments, see [Peng et al., 2025]. For ease of presentation, we will consider the unweighted version but all our results extend to weighted model counting.

The degree of a variable v is the number of clauses containing v, and by dk(v) we denote the number of clauses of length k containing v.

Branching Algorithms. Branching algorithms solve combinatorial problems by recursively decomposing them into subproblems. At each step, the algorithm uses some criterion to divide the current formula into subformulas, the so-called branches, then recursively solves the resulting subproblems and aggregates their solutions.

Definition 3 (Branching Vector). Let T(n) be the running time of a branching algorithm on an instance of size n. If a branching operation creates k subproblems of sizes n - t1, n - t2, . . . , n - tk respectively, then (t1, t2, . . . , tk) is called the branching vector of this operation.

Definition 4 (Branching Number). The branching number τ(t1, t2, . . . , tk) of a branching vector (t1, t2, . . . , tk) is the unique positive root of the equation

The branching number determines the exponential factor in the running time such that if the largest branching number among all branching operations is τ, then the algorithm runs in time O∗ (τ n ).

Throughout the paper, log denotes the base-2 logarithm. We use O∗ notation to suppress polynomial factors, i.e., O∗ (f(n)) = O(f(n) · poly(n)).

3 Complementary Branching

As a warm-up, we illustrate complementary branching in its simplest form and design a clause branching #SAT algorithm that runs in time O∗ (2m) and can be seen as a simplification of the inclusion-exclusion technique [Lozinskii, 1992].

Let F be a CNF formula and let C be a clause such that F = G ∧ C. Using the basic identity

we obtain

Thus, we can always select a clause C and branch as "remove C" vs. "falsify C", the recursion base being that an empty formula over n unassigned variables has 2n models.

We can extend the above idea such that we obtain strong branchings with respect to n in certain cases. Consider F = F-a ∧(a∨b∨c) where a appears only in this clause. Branching on a gives #(F-a) for a=1 and #(F-a∧(b∨c)) for a=0. Observe that #(F-a) = #(F-a∧(b∨c))+#(F-a∧¯b∧¯ c), so #(F ) = 2 ·#(F-a)-#(F-a ∧¯b∧¯ c). Thus, we need to compute #(F-a) and #(F-a ∧ ¯b ∧ ¯ c), which yields a branching number τ(1, 3).

The next two lemmas formally present the concept of complementary counting, and how it can be used to design a new branching technique that we call DNF branching.

Lemma 1 (Complementary counting). Let F be a Boolean formula and a ∈ var(F). Then

Proof. Partition by the value of a:

For any Boolean formulas G,H ⊆ F, it holds #SAT(G) = #SAT(G∧H) +#SAT(G∧ ¬H). Setting G = F-a and H = Fa[a = 0] yields

and similarly

Summing both equalities proves the lemma.

Note that a /∈ var(F-a), and if F is over n variables then F-a is over n - 1 variables. If all clauses of F-a are satisfied, then #SAT(F-a) = 2n-1 . Similarly, if all clauses are satisfied in Fa[a = 1], then #SAT(¬Fa[a = 1]) = 0.

Lemma 2 (DNF branching). Let F be in CNF and H = C1∧ · · · ∧ Ct be a conjunction of clauses. Then

Proof. We show that

and that the formulae in the disjunction are pairwise exclusive. Any assignment κ satisfying F ∧ ¬H satisfies at least one ¬Ci, therefore κ must also satisfy at least one of the formulas in the disjunction. Also, since ¬H is satisfied there exists a unique smallest index i such that κ(¬Ci) = 1 and κ(C1) = 1, . . . , κ(Ci-1) = 1. Further, it holds that κ satisfies exactly the i-th formula as for all subsequent formulae we have κ(Ci) = 0, and thus κ(F ∧C1 ∧· · ·∧Ci ∧. . . ¬Cj) = 0 for j > i. Therefore the formulae in the disjunction are mutually exclusive, no model is counted twice and the model count of F ∧ ¬H equals the sum on the right-hand side.

Example. Consider a formula F in CNF such that the only clauses in F containing the variable a are (¯a ∨ l1 ∨ l2 ∨ l3), (¯a ∨ l4 ∨ l5 ∨ l6), and (a ∨ r1 ∨ r2 ∨ r3). Branching on a yields the two subformulas F-a ∧ (r1 ∨ r2 ∨ r3) and F-a ∧ (l1 ∨ l2 ∨ l3) ∧ (l4 ∨ l5 ∨ l6).

By complementary counting and using that ¬(l) = (¯l) for unit clauses we obtain:

For the other branch, let C1 = (l1 ∨ l2 ∨ l3) and C2 = (l4 ∨ l5 ∨ l6). Then

Applying the DNF branching lemma to ¬(C1 ∧ C2) gives

which is equivalent to

In the above example we obtain a branching number of τ(1, 4, 4, 4) ≈ 1.6581 by computing #SAT(F-a) and assigning the variables in the unit clauses in the other three branches. Branching in a similar way on variables of low degree appearing in longer clauses will be the key ingredient to designing a fast algorithm for instances with low density.

It should be noted that the proofs of Lemma 1 and Lemma 2 use only that we partition assignments into disjoint subsets and add their respective counts. Evaluating the weights of literals (including negated ones) does not affect the asymptotic complexity of the algorithm. Hence both lemmas naturally extend to weighted model counting.

4 An Algorithm for Sparse #SAT

Properties of Branching Numbers. The following two lemmas provide bounds on branching numbers that appear in our algorithms. The proofs are provided in the appendix.

Lemma 3. Let τk denote the branching number of the vector (1, 2, . . . , k), k ≥ 3. Then

Lemma 4. Let d ≥ 3 and k ≥ log(2d). For the branching vector (1, k+1, . . . , k+1) with d copies of k+1, the branching number τ satisfies

4.1 An Algorithm for Instances of Bounded Degree

In Algorithm 1 we present #BoundedSAT, an algorithm for counting the number of satisfying assignments for Boolean CNF formulas of bounded degree ∆. The key insight is that if all variables have degree at most ∆ then we can always obtain a branching number τ∆ < 2.

If there is a clause of length at most k, we branch on it (short clause branching). This yields the branching vector (1, 2, . . . , k) whose branching number is strictly less than 2 for every fixed k. If no short clause exists then we can apply complementary counting by branching on a variable a of bounded degree at most ∆ which appears only in clauses of length at least k + 1. By choosing an appropriate k = k(∆) we obtain

and expand each negated term with DNF branching. Since all clauses have length at least k + 1 in this case, each DNF branch fixes at least k additional literals. This leads to a branching vector of the form (1, k + 1, . . . , k + 1) with d k-branches, which has branching number < 2 for suitable choices of k = k(∆) and d = d(∆).

Theorem 1. The number of satisfying assignments of a CNF formula over n variables of maximum variable degree ∆ can be determined in time O∗ (2(1- 1 3D )n ) where D = max(∆, 3).

Algorithm 1 #BoundedSAT

Input: CNF formula F over n remaining variables, clause length k

Output: #SAT(F)

• 1: if F contains an empty clause then
• 2: return 0
• 3: end if
• 4: if F has no clauses then
• 5: return 2n
• 6: end if
• 7: if F contains a DNF term from complementary counting then
• 8: Branch as described in Lemma 2
• 9: end if
• 10: if there exists a clause C with |C| ≤ k then
• 11: Apply short clause branching on C, obtaining subinstances F1, . . . , F|C|
• 12: return ∑|C| i=1 #BoundedSAT(Fi, n - i, k) 13: else ▷ complementary counting
• 14: Select a variable a of minimum degree
• 15: return 2 · #BoundedSAT(F-a, n-1, k)-
• 16: #BoundedSAT(F-a ∧ ¬Fa[a = 1], n - 1, k)-
• 17: #BoundedSAT(F-a ∧ ¬Fa[a = 0], n - 1, k)

18: end if

Proof. The algorithm recursively solves the problem using backtracking and uses polynomial space in the input size. We show that for a suitable choice of the clause length parameter k, #BoundedSAT solves the #SAT problem in the given time. Let k = log(2D) where D = max(∆, 3). We consider two cases.

Case 1: If there exists a clause C with |C| ≤ k, then according to Lemma 3, clause branching yields a branching number τ = 21- 1 4 ln 2·D < 21- 1 3D .

Case 2: Otherwise, all clauses have length at least k+1 = log(2D) + 1. Select a variable a of degree at most ∆ ≤ D. All clauses containing a have length at least k + 1, so by complementary counting and DNF branching we obtain a (1, k + 1, . . . , k + 1)-branching with at most D branches. Since D ≥ 3 and k = log(2D), Lemma 4 applies and gives a branching number of 21- 1 2D .

In both cases the branching number is at most 21- 1 3D .

4.2 Extending to Constant Clause Density

We extend the algorithm for maximum degree to handle formulas of low clause density δ as follows. While there exists a variable v of degree at least 4d, for d = max(δ, 3), we branch on v. Otherwise, the formula has maximum degree at most 4d and we apply #BoundedSAT.

The intuition for the complexity analysis of the above approach is as follows. If we branch on balanced variables that appear as at least 2d positive and at least 2d negative literals, we can bound the size of tree to 2ℓ such that ℓ ≤ n/2, and thus the total running time to O∗ (2ℓ+(1- 1 12d )(n-ℓ) ) = O∗ (2(1- 1 24d )n ). But if we branch only on pure variables of degree more than 4d, we decrease the number of clauses in only one of the branches. Therefore, we introduce a new complexity measure that tracks progress in both variables and clauses.

Theorem 2. Let F be a CNF formula over n variables and m clauses with clause density δ = m/n ≥ 1. There exists a constant c > 0 such that the number of satisfying assignments of F can be determined in time O∗ (2(1- 1 cδ )n ) and polynomial space.

Proof. Define

Branching on a variable of degree > 4d reduces µ by at least 1 in one child (we assign one variable) and by at least 2 in the other (we assign one variable and the deletion of > 4d clauses adds at least one additional unit). Thus, a high-degree branching step gives a binary split in which µ decreases by at least 1 in one branch and at least 2 in the other. With δ = m/n ≤ d we have

Let S be the number of units of progress until we reach a leaf where all degrees are ≤ 4d. Clearly, an upper bound is S ≤ ⌈µ(F)⌉ ≤ 5 4 n.

Distinguish between left (assigning a variable) and right branchings (assigning a variable and removing > 4d clauses). This gives us a (1,2)-splitting with respect to µ. Let P be a root to leaf path on which S units of progress have been made. Let t be the number of assigned variables on P, and ℓ and r be the number of left and right branchings on P. Observe that t = ℓ + r and S = ℓ + 2r. Hence, t = S - r, and the number of leafs with t assigned variables and r right branches is (tr) = (S-r r ). Let q = 2(1- 1 12d ) . At each branch we run #BoundedSAT on n - t = n - (S - r) variables. Thus, we can bound the total running time T(n) to

Let us write U(S) = ∑⌊S⌋ r=0 (S-r r )qr . Then we have T(n) = qn-S U(S).

Using Pascal's rule (S-r r ) = (S-1-r r ) + (S-1-r r-1 ) and a change of summation index, with some simple algebra we obtain that U is a Fibonacci-type recurrence:

For such a sequence, the characteristic equation is x2 - x - q = 0 and it has roots λ± := 1±√1+4q 2 , see, e.g., [Graham et al., 1989, Chap. 5.4]). Overall, we obtain

We have 1 < q < 2, hence 1 < λ+ < 2 and -1 < λ- < 0. Therefore for S ≥ 1,

Define ρ(q) := λ+ q = 1+√1+4q 2q . Thus, for the total running time we obtain

for some constant C > 0, and we have T(n) = O((qρ(q) 54 )n ). In the appendix we show that for q = 21- 1 12d we have qρ(q)5/4 ≤ 21-1/(73d) , thus the theorem holds for c = 73.

In addition, we should note that we pessimistically model every high-degree split by the minimal (1,2) progress in µ for branching only on pure variables of high degree. The presented proof technique extends to more balanced branching of the form (1 + i/4, 1 + (4 - i)/4) where 1 ≤ i ≤ 3 clauses are eliminated in one branch and 4 - i in the other.

4.3 Discussion

The classes of #SAT instances for which sub-2n algorithms are known are not many: fixed-width #k-SAT, very sparse formulas with m < n [Lozinskii, 1992], and polynomial time algorithms for bounded treewidth CNFs [Bacchus et al., 2003; Samer and Szeider, 2010]. Schuler's widthreduction [Schuler, 2005] applies to #SAT, but the best #kSAT bounds come from branching on a clause of length k. The lower bound on the branching number in Lemma 3 shows that width reduction cannot yield a sub-2n bound.

We are aware of only one algorithm designed for sparse #SAT, and it has a better running time than O∗ (2n ) only for very sparse instances with δ ≤ 2.25 [Laakkonen et al., 2024]. We find this rather surprising given the long history of (polynomial or exponential space) exact deterministic algorithms for sparse instances for SAT [Arvind and Schuler, 2003; Dantsin and Wolpert, 2005; Wahlstr¨om, 2005; Calabro et al., 2006; Peng and Xiao, 2023] and Max-SAT [Dantsin and Wolpert, 2006; Kulikov and Kutzkov, 2007; Scott and Sorkin, 2007; Golovnev and Kutzkov, 2014; Chen and Santhanam, 2015; Sakai et al., 2017].

It should be noted that the Max-SAT algorithm by [Chen and Santhanam, 2015] applies to general sparse CNF formulas and can be adapted to #SAT to yield a running time O∗ (2(1- 1 cδ )n ) with c = 800. The algorithm is essentially the classic DPLL splitting algorithm that greedily selects highdegree variables to branch on until only unit clauses remain. Using shrinkage analysis [Santhanam, 2010], one bounds the running time to O∗ (2(1- 1 cδ )n ). Note that the greedy approach is similar to our constant density algorithm but there are some important differences. First, we use as a base case our bounded-degree algorithm that exploits specific #SAT properties, and obtain much smaller constant for c. Of course, these constants capture worst cases that are very unlikely to occur in real instances but the gap highlights the contribution of our strong bounded-degree bound. Second, the Chen-Santhanam proof is based on a global probabilistic argument and offers structural insights about sparse CNF formulas but no direct guidance for the design of new #SAT algorithms. In contrast, our DNF branching and explicit complexity measure combining variables and clauses can be naturally translated into novel branching heuristics.

5 An Improved Upper Bound for #3-SAT

Complementary branching can be also used to improve the upper bound for #3-SAT. We build on the algorithm by [Kutzkov, 2007] which combines a reduction from sparse instances to #2-SAT and a careful branching case analysis for denser formulas. We extend complementary branching to a clause learning technique that enables the creation of new 2clauses and strengthen the tight cases in this case analysis.

Solving sparse #3-SAT instances. The algorithm of [Kutzkov, 2007] for instances of average degree at most 5, let us call it #3-SAT-SPARSE, branches on variables of high degree in 3-clauses and then solves the resulting #2-SAT instances. Substituting the current best #2-SAT upper bound of O∗ (1.2377n ) [Wahlstr¨om, 2008] into the analysis of #3-SAT-SPARSE yields the following lemma.

Lemma 5. A #3-SAT instance over n variables with density less than or equal to 5/3 can be solved in O∗ (1.637n ).

5.1 The ComplexityMeasure

For formulas with density > 5/3, we use the complexity measure from [Kutzkov, 2007]: µ(F) = n-λ(F2), where λ(F2) is a positive weight for the subformula of F consisting of 2clauses. The set of all 2-clauses is divided into three subsets: S (for single), T (for two) and R (for rest). S is built from arbitrary 2-clauses in F2, so that no variable in the S-clauses occurs more than once, T may contain at most two 2-clauses and the rest are in R. The S-clauses and T -clauses are weighted with ε > 0. The R-clauses are not weighted. For ε < 1 it holds λ(F2) = (|S|+|T |)ε ≤ (n/2+2)ε < n/2+2, thus the complexity µ(F ) = 0 implies there are no more than constant number of unassigned variables in the formula.

5.2 Complementary Clause Learning

Lemma 6. Let F be a CNF formula and let a be a variable that occurs only positively in F . Write F = F-a ∧Fa, where Fa is the conjunction of all clauses containing a, and let H be any CNF formula equivalent to ¬Fa[a = 0]. Then

Hence

Apply complementary counting (Lemma 1) to the instance F-a with constraint G:

By assumption H is a CNF equivalent to ¬G, so

Substituting into the expression for #SAT(F) yields

Algorithm 2 #3-SAT-General

Observe that the above lemma implies that for a pure literal a we mimic branching in the standard way on a. However, we "learn" the CNF H from ¬Fa[a = 0] and instead of F [a = 1] we consider F-a ∧ H which is particularly useful if a has a low degree. For example, let Fa = (a ∨ b) ∧ (a ∨ x1 ∨ x2). Then H = (¯b∨¯x1)∧(¯b∨¯x2), and by adding the two 2-clauses we decrease the complexity µ(F [a = 1]) by 2ε.

5.3 The Algorithm

In Algorithm 2 we present the #3-SAT algorithm which considers different cases depending on the maximum degree of the formula and the cardinality of the 2-clauses sets S and T . Fk denotes the subformula of F consisting of k-clauses.

Case 0. The number of added 2-clauses is at least six. We analyze only the worst case when all six 2-clauses are added in one branch. It is easy to verify that the more symmetric the complexity decrease in both branches, the smaller the branching number. The analysis for the other cases can be immediately concluded from this one. If variable b occurs 3 ≤ k ≤ 5 times in the added 2-clauses then we branch on b and the recursion is computed to τ (1, 2 + (6 - k)ε, k + 2). For k = 6 we obtain six 2-clauses that all share the same variable b. If b is not a pure literal, then immediately branching on b would yield a branching number of at least τ (1, 3, 7) < 1.52. Otherwise, the literal b is dominated by the literal a, or vice versa, such that by assigning a = 1, respectively b = 1, there are no more appearances of b, respectively a. Thus, the branching is at least τ(1, 2) < 1.62.

Therefore we conclude that no variable occurs more than twice in the added six 2-clauses. First of all we observe that each four of the considered 2-clauses will fit in S and T as there always exist two variable-disjoint 2-clauses which can be set in S. If we have the 2-clauses (l1 ∨ l2), (¯l1 ∨ l3) we easily obtain τ(1, 3 + 3ε, 3 + 3ε). Let's now consider the case we have 2-clauses (l1 ∨ l2), (l1 ∨ l3). If l2 or l3 does not occur in another of the six 2-clauses or l2 and l3 are in the same 2-clause we branch on l1. As per [Kutzkov, 2007], such variables of degree two are called suitable variables. The corresponding recursion equation is computed to τ (1, 2+4ε, 4+3ε). If there exists no suitable variable and not all the six 2-clauses fit in S and T , we conclude a "deadlock" situation, i.e. six variables forming six 2-clauses so that each variable occurs twice: e.g. (l1 ∨ l2), (l3 ∨ l4), (l1 ∨ l3), (l2 ∨ l5), (l4 ∨ l6), (l5 ∨ l6). In this configuration we distinguish two subcases. If some variable, say l1, appears only in its two 2-clauses (l1 ∨ l2) and (l1 ∨ l3) and nowhere else in the formula, then by Lemma 6 we can apply complementary counting to the l1-branch and obtain an additional 2-clause of the form (¯l2 ∨ ¯l3) in the l1 = 1 branch. Branching subsequently on l2 in the l1 = 1 branch yields a branching number stronger than τ (2, 3, 3) < 1.53. Otherwise every li has an additional occurrence outside these six 2-clauses, and branching on such a variable immediately yields a recursion of at least τ (1 - 2ε, 3 - 3ε).

If none of the above applies, all six 2-clauses can be added to S ∪T and weighted with ε. Thus, we compute the branching number to τ (1, 1 + 6ε).

Case 1. The goal in this case is to show that we have a worstcase recursion of τ(1-ε, 2+2ε). Let (a∨b) be a 2-clause in F2. If one of a, b (say a) occurs only in this clause, we branch on the other variable and obtain a symmetric (2 - ε, 2 - ε)- branching. If a has degree 2 in F, then besides (a ∨ b) it appears in a single additional clause, say (a ∨ ℓ1 ∨ ℓ2). By Lemma 6 we can apply complementary counting in the a = 1 branch and add 2-clauses (¯b ∨ ¯ ℓ1) and (¯b ∨ ¯ ℓ2). This yields a branching number of at least τ(1, 2) < 1.62.

If both a and b have degree 3, we branch a and in the a = 1 branch we can use complementary counting on the two 3clauses containing b. Let these be (b ∨ l1 ∨ l2), (b ∨ l3 ∨ l4). In the general case, branching on b and applying Lemma 6, results in a branching number of τ(1 + 2ε, 1 + 4ε), thus an overall branching of τ(2 + ε, 2 + 3ε, 2 + ε). If we cannot add four 2-clauses, then we have a specific structure such as a shared variable among the li variables or 2-clauses in S in which at least two of the li's appear. In all these cases we can either assign one more variable or have a subsequent strong branching assigning 2 variables in each branch.

Finally, if at least one of a, b has degree at least 4, then branching on that variable creates three new 2-clauses in one branch. If we cannot add the three 2-clauses to S ∪ T , then we can have a subsequent (1,3)-branching. We then obtain a branching number at least τ(1-ε, 3, 5-2ε). Otherwise, the branching number is the desired τ (1 - ε, 2 + 2ε).

Case 2. The case when a literal and its negation both occur in F2 has an obvious bound of τ(2 - 3ε, 2 - 3ε) since the setting of a variable deletes at most two 2-clauses and one of the 2-clauses is shared by the assigned variables. Otherwise we have a literal which occurs twice; w.l.o.g. consider the 2-clauses (a ∨ b) and (a ∨ c). If a appears in an additional clause (either a 2-clause or a 3-clause), then branching on a yields a recursion of at least τ(1 - 2ε, 3 - 3ε), since in one branch we delete two weighted 2-clauses and in the other we gain (at least) an extra weighted 2-clause from the additional occurrence. If a appears only in (a∨b) and (a∨c), we apply Lemma 6 with G = b ∧ c to replace the a = 0 branch with the complementary instance F-a ∧ (¯b ∨ ¯ c). This guarantees in the complementary branch there is a newly learned weighted 2-clause, so the recursion is bounded by τ (1 - ε, 3 - 4ε). Case 3. The recursion equation τ(1 - 3ε, 4 - 5ε) is trivial since we delete all T -clauses.

Theorem 3. The #3-SAT problem on formulas over n variables can be solved in time O∗ (1.637n ).

Proof. For instances of density at most 5/3, Lemma 5 gives a running time of O∗ (1.637n ). It therefore suffices to consider formulas of density > 5/3 and analyze the algorithm #3SATGeneral using the complexity measure µ(F ) = n - λ(F2).

The case analysis above shows that for every recursive call the measure µ decreases according to one of the following branching vectors:

• Case 0 (no 2-clauses) yields τ(1, 2+3ε, 5), τ(1, 2+2ε, 6), τ(1, 2+ε, 7), τ(1, 3+3ε, 3+3ε), τ(1, 2+4ε, 4+3ε), and τ (1, 1+6ε).
• Case 1 (F2 ⊆ S, T = ∅) yields (2-ε, 2-ε), τ(2+ε, 2+ 3ε, 2 + ε), τ (1-ε, 2+2ε) and τ (1 - ε, 3, 5 - 2ε).
• Case 2 (a literal of degree two in F2) yields τ(2-3ε, 2-3ε), τ(1-2ε, 3-3ε) and τ(1-ε, 3-4ε).
• Case 3 (a variable of degree three in S ∪ T ) yields τ (1-3ε, 4-5ε).

Fix ε = 0.1545. The numerical evaluation of the branching numbers listed above shows that the maximum is at most 1.6343, and the tight cases are τ(1, 2+4ε, 4+3ε), τ(1, 1+6ε), and τ(1-2ε, 3-3ε). Therefore, the total running time of Algorithm 2 on formulas of density > 5/3 is bounded by O∗ (1.6343n ). Combining this with #3-SATSPARSE from Lemma 5 gives an overall running time of O∗ (1.637n ) for #3-SAT.

5.4 Discussion

There is a long history of exact deterministic algorithms for #2-SAT and #3-SAT, with running times analyzed with respect to the number of variables or the number of clauses [Zhang, 1996; Dahll¨of et al., 2005; F¨urer and Kasiviswanathan, 2007; Kutzkov, 2007; Wahlstr¨om, 2008; Zhou et al., 2010; Peng et al., 2025]. When parameterized by the number of clauses, the best known bounds are O∗ (1.1082m) for #2-SAT and O∗ (1.4423m) for #3-SAT.

Note that an improved upper bound for #2-SAT with respect to the number of variables would improve the bound O∗ (1.637n ) for sparse #3-SAT instances and thus yield a better overall bound for #3-SAT.

Randomized algorithms can achieve an eε -approximation of the model count with stronger exponential bases than our deterministic bound, but incur an additional ε-2 factor in running time [Thurley, 2012; Schmitt and Wanka, 2013].

6 Conclusions and Future Directions

We introduced complementary branching, a novel branching paradigm for model counting that naturally complements the classical DPLL branching. Using this technique, we designed new algorithms for sparse #SAT instances and obtained a new record running time for #3-SAT. These results demonstrate that complementary branching is a powerful and versatile tool for designing faster exact algorithms for model counting.

While our results are theoretical, a major research direction is to leverage the introduced complementary branching techniques in modern #SAT solvers. We analyzed 200 MC2025 benchmark instances [Fichte and Hecher, 2025] for weighted and unweighted model counting benefits. Below is a summary of our findings, details can be found in the appendix:

• Complementary clause branching as described in Section 3. In about 8% of the instances less than 1% of the clauses contribute to more than 10% of the overall clause length. In 11% of the instances there are clauses with hundreds of variables and removing such long clauses early on might yield structural benefits.
• DNF branching as described in Lemma 2. We observe that 15 instances in the two tracks will directly benefit from DNF branching. We search for variables of degree at most 5 that appear only in clauses of length at least 4, and compute the branching numbers for these variables using DNF branching, see Lemma 2. Table ?? shows a list of instances that have ≥ 1% of such variables, achieving average branching numbers τ ≈ 1.38. Notably, the largest test instances benefit the most.
• Clause learning as described in Lemma 6. Pure variables are abundant among the test instances, and in many instances there is a significant number of pure variables of low degree. We computed that for 20 out of 200 instances more than 10% of the variables are pure with degree below the median clause length, allowing us to create many new short clauses. These new clauses can thus further shrink the search space and guide #SAT solvers.

Of course, the above is just a first glimpse into the potential benefits of complementary branching, and one needs to study how the technique can be combined with other methods. In particular, DNF branching and clause learning are likely to be more beneficial at deeper levels of the branching tree where even more low-degree variables emerge.