Equisatisfiability
Encyclopedia
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. Two equisatisfiable formulae may have different models
, provided they both have some or both have none. 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
. The Davis-Putnam algorithm removes, at each step, a variable from a formula, generating a formula that is equisatisfiable with the original one.
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.
Logic
In philosophy, Logic is the formal systematic study of the principles of valid inference and correct reasoning. Logic is used in most intellectual activities, but is studied primarily in the disciplines of philosophy, mathematics, semantics, and computer science...
, 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. Two equisatisfiable formulae may have different models
Model theory
In mathematics, model theory is the study of mathematical structures using tools from mathematical logic....
, provided they both have some or both have none. As a result, equisatisfiability is different from logical equivalence
Logical equivalence
In logic, statements p and q are logically equivalent if they have the same logical content.Syntactically, p and q are equivalent if each can be proved from the other...
, 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
Conjunctive normal form
In Boolean logic, a formula is in conjunctive normal form if it is a conjunction of clauses, where a clause is a disjunction of literals.As a normal form, it is useful in automated theorem proving...
. The Davis-Putnam algorithm removes, at each step, a variable from a formula, generating a formula that is equisatisfiable with the original one.
Examples
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.