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.
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.