
## Algorithm #Xsat

We propose a main algorithm \#XSAT (Figure 5) which makes use of another algorithm \#XSAT3 when(F)3. Both of the algorithms are based on the DPLL and take the reduced XSAT formula F as the input. The basic idea of the two algorithms is to choose a variable and recursively count the number of satisfying assignments where the variable is *true* and the variable is false. At first, we present the framework of our algorithm \#XSAT3 for solving \#XSAT when (F)3 in Figure 4. Note that in the algorithm MC(F) is a function that solves the \#XSAT by exhaustive search. As we all know, if a \#XSAT instance is solved by exhaustive search, it will spend a lot of time. However, when the number of clauses that the formula F contains is so few, it may run in polynomial time. Therefore, we use the function MC(F) only when the number of clauses isn't above 4, which can guarantee the exhaustive search runs in polynomial time. In addition, since the operation on each node is the function(F, ) running in polynomial time, we analyze the algorithms \#XSAT3 and \#XSAT using the measure described above in the following theorems.

Theorem 3. Algorithm \#XSAT3 runs in O(1.1995n) time, where n is the number of the variables.

Proof. Let us analyze the algorithm case by case.

Case 1, 2, and 3: These cases run in O(1).

Case 4: This case doesn't increase the time needed.

Case 5: Suppose the two clauses are of the forms (xyC) and (xyC'). We know that at least the literal x appears in another clause based on Theorem 2.The running time T(n) of the algorithm satisfies the recursive relation

## T(N)=T(N- C - C'+C C' -1)+T(N-2-I) (8)

where i is an integer and C C'is the set of literals occurring in both sub-clauses. When (xy)=*true*, the literals in Cand C' are removed. When x=*false* and y=*false*, the two literals are also removed. Furthermore, onceC=2 one literal is removed by function *Reduce* (line 2), i.e., i=1. And the same situation is encountered whenC' =2. Here, since each clause has at least two variables that do not occur in the other by Theorem 2, C 2,C' 2, andC C' min (C -2,C' -2). Moreover, ifC C' 1, x and y both occur in another clauses based on Theorem 2. When (xy)=*true, y* is substituted byx and this makes x a (1, 1+)-literals, which we can remove by resolution principle 1. Therefore, it is easy to see that the worst case 