Function unit(F[l]) 1. If there exists a clause ll1 l2  ... ln in F,
then remove the clause ll1 l2  ... ln and the literals l1, l2,…, ln from F.

2. If there exists a clausel l'1 l'2  ... l'k in F, 
removel fromll
'1 l'2  ... l'k.

3. For 1≤ i ≤
n do unit(F[li]).

4. Return F.

Park J.D.. 2002. MAP complexity results and approximation methods. In *18th UAI*, 388-396.

Sang T., Beame P., and Kautz H.A.. 2005. Performing Bayesian inference by weighted model counting. In *20th AAAI*, 475482.

Porschen S.. 2005. On some weighted satisfiability and graph problems. In 31s *SOFSEM*, 278-287. Porschen S.. 2006. Counting all solutions of minimum weight exact satisfiability. In *6th CIAC*, 50-59.

Valiant G.. 1979. The complexity of computing the permanent. Theoretical Comput. Sci. 8(2): 189–201.