Equisatisfiability Explained
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 neither is.[1] The truth values of two equisatisfiable formulae may nevertheless disagree for a particular assignment of variables. As a result, equisatisfiability differs from logical equivalence, since two equivalent formulae always have the same models, whereas equisatisfiable ones need only share satisfiability status. More formally, the equisatisfiability meta formula
is true if either the two subformulae are both satisfiable or if they both are not:
[2] f \equiv (\operatorname{Sat}(\phi)\land\operatorname{Sat}(\psi))\lor(lnot\operatorname{Sat}(\phi)\landlnot\operatorname{Sat}(\psi)) \equiv \operatorname{Sat}(\phi)\leftrightarrow\operatorname{Sat}(\psi)
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.
Examples
A translation from propositional logic into propositional logic in which every binary disjunction
is replaced by
(a\veen)\wedge(\negn\veeb)
, where
is a
fresh variable (one for each replaced disjunction) is a transformation in which satisfiability is preserved: the original and resulting formulae are equisatisfiable. These two formulae are not equivalent: the first formula has the model in which
is true while
and
are false (the model's truth value for
being irrelevant to the truth value of the formula), but this is not a model of the second formula, in which
has to be true when
is false.
References
- Book: Markus Krötzsch. Description Logic Rules. 11 October 2010. IOS Press. 978-1-61499-342-1.
- Book: Bradley . Aaron R. . Manna . Zohar . The Calculus of Computation: Decision Procedures with Applications to Verification . Springer . Berlin Heidelberg New York . 2007 . 24 . 978-3-540-74112-1.
