Note that in this function, S is an integer value recording the length of the eliminating sub-clause thatappears in. We assume that P=1 when the literals indon't appear in R.

Algorithm \#XSAT3(F)
Case 1: F has an empty clause. Return 0. Case 2: F is empty. Return 0.

Case 3: m 4. Return MC (F).

Case 4: F contains disjoint components F1, F2, …, Fk.

Return \#XSAT3 (F1)\#XSAT3(F2) …\#XSAT3 (Fk). 

Case 5: F contains two clauses having at least two literals in common. Pick two maximal degree common variables x and y and return \#XSAT3 ((F, {x y})) + S\#XSAT3
((F, { x, y })). Case 6: If F contains a 3-clause x yz, where x isn't a singleton.

1. If there is a 4-clause x pq r none of which is singleton, then return \#XSAT3 ((F, 
{ x p })) + \#XSAT3 ((F, { q r })).

2. Otherwise, return S\#XSAT3 ((F, {x}))+ S
\#XSAT3 ((F, { x})).

Case 7:If F contains a 4-clause x yzp having no singletons, then return \#XSAT3 ((F, {x y})) +
\#XSAT3 ((*F, {z*p})).

Case 8: If F contains a 4-clause x yzp, where p is a singleton and z also occurs in other 4-clause, then return \#XSAT3 ((F, {x y})) + \#XSAT3 ((F, 
{zp})). Case 9: If F contains a 5-clause x yzpq having no singletons, then return \#XSAT3 ((*F, {x* y})) + \#XSAT3 ((F, {zp})) + S\#XSAT3 ((*F, {q*})).

Case 10: If F contains a 4-clause x yzp, where p is a singleton and x, y, and z all occur in clauses of length at least 6, then return S\#XSAT3 ((F, {x})) 
+ S\#XSAT3 ((F, {y}) + \#XSAT3 ((F, {zp})).

Case 11: If F contains a clause of length at least 6, pick a literal x that isn't a singleton in the clause and return S\#XSAT3((F, {x})) + S\#XSAT3 ((F, { x})).

Case 12: If F contains a 5-clause x yzpq, where q is a singleton, then return \#XSAT3 ((F, 
{x y})) + S\#XSAT3 ((F, {z})) + \#XSAT3 ((F, 
{pq})).

Figure 4: \#XSAT3 Algorithm