number of the common literals when counting the models of the \#XSAT problem. Thus, from the above we know if a XSAT 
formula F can be simplified by the common variables principle, then any two clauses in F don't have more than two literals in common. And once there are two clauses having more than two literals in common, this means that Var(C) Var(F')≠and at least one common variable appears in another clause. Then we can branch on maximal degree of the common variables, which allows us to eliminate as many variables as possible.

Next we describe how to solve the \#XSAT problem using the resolution principles which inspired by (Byskov et al. 2005).

Actually, the resolution principle is a well-known technique for removing variables occurring both positive and negative and efficiently solving SAT problem. However, it is a pity that the technique can't be applied in solving \#SAT for sometimes it eliminates a few variables which leads to the wrong result. Although \#XSAT is also a counting problem, but the technique is suitable to solve \#XSAT on account of the nature of the XSAT problem. Since the complexity of each node in the branching tree is strictly greatly than its son, we just use the resolution principle for (1, 1+)-literals and (2, 2)-literals so that the resolution never increase the complexity. Now suppose that an exact SAT formula F contains a (1, 1+)-literal or a (2, 2)-
literal, then we obtain the following principles.

Resolution Principle 1. Let F = (xC)(xC1)(xC2) … (xCk)F', where x is a literal, C1 , C2, and Ck are sub-clauses in F. Then, M(F)=M(F'') 
where F''=(CC1)(CC2) … (CCk)F'
Resolution Principle 2. Let *F=(x*C1)( xC2)(xC3)(xC4)F', where x is a literal, C1 , C2, C3, and C4 are sub-clauses in F. Then, M(F)=M(F'') where F''=(C1 C3)
(C1 C4)(C2 C3)(C2 C4)F'
 By performing the resolution principles, if the reduced formula F contains a variable occurring both unnegated and negated, the literal consisting of the variable must be a (2+, 3+)-literal. According to the two resolution principles, we can obtain the follows. Theorem 1. Given a formula F, if F only contains (1, 0)-literals, (2, 0)-literals, (3, 0)-literals, and it has a clause xy, then x and y can be both removed. 

(6)
(7)