Equisatisfiability

From Wikipedia, the free encyclopedia
Jump to navigation Jump to search

In 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. Equisatisfiable formulae may disagree, however, for a particular choice of variables. As a result, equisatisfiability is different from logical equivalence, as two equivalent formulae always have the same models.

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 involving this concept are Skolemization and some translations into conjunctive normal form.

Examples[edit]

A translation from propositional logic into propositional logic in which every binary disjunction is replaced by , where is a new variable (one for each replaced disjunction) is a transformation in which satisfiability is preserved: the original and resulting formulae are equisatisfiable. Note that these two formulae are not equivalent: the first formula has the model in which is true while and are false, and this is not a model of the second formula, in which has to be true in this case.