uni/sysver/3-sat/3-sat.md

Tseitin transformation

Let $F$ be a formula in $\text{conjunctive normal form}$ (CNF), i.e., a conjunction of clauses

$$ \bigwedge\limits_i^{C} \bigvee\limits_j^{Si} \ell{i,j},\ \text{where}\ \ell_{i,j} \in { P, \neg P \mid P \text{ is an atom} } $$ {#eq:clauses}

Note that every clause $C_i$ with $m$ literals can be seen as a "nested" disjunction, i.e.,

$$ Ci = (\ell{i,1} \lor (\ell{i,2} \lor (\text{...} \lor (\ell{i,m-1} \lor \ell_{i,m}) $$ {#eq:nested}

Explain how you can use Tseitin's transformation to convert any arbitrary formula in CNF into an equi-satisfiable formula in CNF whose clauses have at most 3 literals.

solution

A clause in the formula is with no loss of generality described by

$$ Ci = (\ell{i,1} \lor \ell{i,2} \lor (\ell{i,3} \lor (\ell{i,4} \lor (F))),\ F = \bigvee{j}^A \ell_{i,j},\ A = {S_i} \setminus {1,2,3,4} $$ {#eq:general-formula}

We can introduce a new symbol for a satisfiability-equivalent formula

$$ (\ell{i,1} \lor \ell{i,2} \lor O_1) \land (O1 \Leftrightarrow (\ell{i,3} \lor (\ell_{i,4} \lor (F))) $$ {#eq:equivalent-formula}

and apply the corresponding Tseitin Encoding

$$ \begin{aligned} (\ell{i,1} \lor \ell{i,2} \lor O1)\land (\neg \ell{i,3} \lor O1) &\land \overbrace{(\neg(\ell{i,4} \lor F) \lor O1)}^{C{i,const}} \ &\land \underbrace{(\neg O1 \lor \ell{i,3} \lor (\ell{i,4} \lor (F)))}_{C_i,recursive} \end{aligned} $$ {#eq:tseitin}

Doing so yields two components for which we have to show that they contain at most 3 literals. The first of which represents a constant blow-up of conjuncts

$$ \begin{aligned} C{i,const} &= \neg (\ell{i,4} \lor F) \lor O1 \ &= (\neg \ell{i,4} \land \neg F) \lor O1 \ &= (\neg \ell{i,4} \lor O_1) \land (\neg F \lor O1) \ &= (\neg \ell{i,4} \lor O_1) \land (\neg (\bigveej^A \ell{i,j} ) \lor O1) \ &= (\neg \ell{i,4} \lor O_1) \land ((\bigwedgej^A \neg \ell{i,j} ) \lor O1) \ &= (\neg \ell{i,4} \lor O_1) \land (\bigwedgej^A \neg \ell{i,j} \lor O_1) \ \end{aligned} $$ {#eq:conjuncts}

Note that [@eq:conjuncts] makes entensive use of the distributivity of conjuncts and disjuncts to expand $C_{i,const}$ into sub-clauses that are short enough.

The other remaining clause is $C_{i,recursive}$, for which it remains to be shown that the formula is a disjunction with at most 3 literals. This term is the original expression $Ci$ without the disjuncts $\ell{i,1}$ and $\ell_{i,2}$. The expansion described in [@eq:equivalent-formula] and [@eq:tseitin] can thus be applied again until all clauses have been reduced to form an equi-satisfiable formula in CNF whose clauses have at most 3 literals.