$$\begin{array}{r l}{F_{1}}&{{}F_{2}}\\ {\ }&{{}}&{{}}\end{array}$$
$$F^{\prime}$$
The same holds for  The number of clauses of formulas F1 F2 produced by splitting F is
equal to the number of all clauses of F minus the number of clauses of F which contain the

3. In this case, each variable occurs in each clause positively, negatively or not at all

(3)

Proof is given in Appendix A.

The assumption of is commonly adopted in probabilistic analysis of algorithms

literal l respectively.

Lemma 2 Each of formulas F1, F2 produced by splitting F contains m  clauses with probability m k k(1  m k.

Since each of F1 F2 contains at most n variables, the following recurrence inequality
$$\begin{array}{l l l l}{{\mathrm{S}}}&{{}}&{{}}&{{F_{1}}}&{{F_{2}}}\\ {{T}}&{{m\,,\,n}}&{{}}&{{}}\end{array}\qquad\qquad\qquad\begin{array}{l l l l}{{n-1}}&{{}}&{{}}&{{}}\\ {{}}&{{}}&{{}}&{{}}\end{array}$$
for T m; n holds. T m; n  8 : cmn+ Pm k =1 m k k(1  m kT m  k; n  1)+ Pm k =0 m k k(1  m kT m  k; n  1) n; m  (2) n or m The rst term cmn is the time needed for one iteration of CDP. The second and third terms are the expected times needed for computing the number of models of F1 and F2 respectively. Since the literal l appears in F it is impossible that the number of clauses in which l occurs is 0, and so, the summation of the second term starts at 1. The literal may not appear at all in F (if l is pure). Consequently, the summation of the third term begins at 0. The right-hand side of (2) overestimates T m; n since, rst, the number of variables of F1 F2 is at most n  1, and, second, function CDP may stop when F contains an empty clause, even before m or n becomes 0. To estimate T m; n), we show, rst, that for 3, T m; n O m2n), and, second, that for any p T m; n O mdn where d 1 log2 (1p ) e: 3.2 The Average Running Time for Following Goldberg (1979), we start with the analysis of the average running time for

$$F^{\prime}$$

with the same probability (1 3). So, recurrence (2) takes the form

T m; n  8 : cmn+ 2 3 m T m; n  1)+ Pm k =1 m k )( 1 3 k 2 3 m k T m  k; n  1) m; n  n or m Theorem 1 For 1 3 , T m; n O m2n :

3.3 The Average Running Time for Any p handling CNF or DNF formulas (Franco & Paull, 1983; Goldberg, 1979; Goldberg et al.,
