# Tseitin's Encoding

Definition: Formulas and are equisatisfiable iff is satisfiable iff is satisfiable.

Note: If a formula is satifiable, it is equisatisfiable with formula 'true'. If a formula is unsatisfiable, it is equisatisfiable with the formula 'false'.

Claim: each formula can be transformed in polynomial time into a new formula such that is satisfiable iff is satisfiable.

Procedure:

The use of last rule can be minimized by using negation-normal form–applying De Morgan's laws to push negation to leaves of the formula syntax tree.

Then transform each of the equivalences into a conjunction of clauses:

Note: if is in negation-normal form, then we can replace some of these equivalences with implications.