In mathematical logic (a subtopic within the field of formal logic), two formulae are equisatisfiable if the first formula is satisfiable whenever the second is and vice versa; in other words, either both formulae are satisfiable or both are not.
[1] Equisatisfiable formulae may disagree, however, for a particular choice of variables.
Equisatisfiability is generally used in the context of translating formulae, so that one can define a translation to be correct if the original and resulting formulae are equisatisfiable.
Examples of translations that preserve equisatisfiability are Skolemization and some translations into conjunctive normal form such as the Tseytin transformation.
is a new variable (one for each replaced disjunction) is a transformation in which satisfiability is preserved: the original and resulting formulae are equisatisfiable.
are false (the model's truth value for