
## Reduction Principles

In this subsection, we concentrate on introducing the common literals principle and describing how to use the resolution principles in solving the \#XSAT problem. 

![0_image_0.png](0_image_0.png)

Figure 1: Function *unit(F[l*])

![0_image_1.png](0_image_1.png)

Before presenting the common variables principle, function *unit(F*[l]) in Figure 1 is addressed, which recursively executes the propagation. The function takes a formula F and a literal l being assigned *true* as input. The detailed process of the function is presented as follows. (1) Remove all clauses containing literal l from F; (2) delete all literals occurring with l from the other clauses; (3) delete all occurrences of the negation of literal l from F; (4) perform the process as far as possible.

Finally, the function returns a simplified formula. For ease in writing, the function *unit*(F[l]) is called F[l] for short in the following sections.

Now we begin to present the common variables principle. Supposing an exact SAT formula F contains at least two clauses having at least variables in common. Then we can calculate the models of F as follows:
Common Literals Principle. Let F=(CC1)(CC2) … (CCk)F', where C, C1 , C2,…, Ck are sub-clauses, and Var(C) Var(F')=. Then, M(F)=C M(F'' [x])+ M(F'' [x]) where F''=
(5)
(xC1)(xC2) … (xCk)F' and xC
This principle is referred to as removing superfluous common literals. For example, F=(xy z)(xy r)(s p). 

Then by executing the common literals principle, the formula can be reduced as F''= (x z)(x r)(s p). It seems reasonable that M(F)=M(F'') but this is not the case. In a model when x=*true*, y is *false*. However, we know that there is a model that x=*false* and y=*true*. This means that the reserved literal x represents both, and therefore, we should hold the 