Equisatisfiable Propositional Formula

logic

Definition

Equisatisfiable Propositional Formula

Two propositional formulas (or sets of formulas) are equisatisfiable if one is satisfiable exactly when the other is.

More precisely, $F$ and $G$ are equisatisfiable whenever

$$F\text{ is satisfiable }⟺G\text{ is satisfiable}.$$

This is weaker than logical equivalence: equisatisfiable formulas need not have the same models, nor even the same variables.

Relation to Equivalence

Weaker than equivalence

Logical equivalence implies equisatisfiability, but not conversely.

Equisatisfiability is the right notion when one only cares whether a formula has at least one model, for example during CNF transformation or naming.

Examples

Naming introduces a new variable

Let

$$F=p\leftrightarrow q.$$

Introduce a new atom $n$ and define

$$F_1=n\leftrightarrow q,F_2=p\leftrightarrow n.$$

The set $\{F_1,F_2\}$ is equisatisfiable with $F$, but not logically equivalent to it. An interpretation with $p=1,q=0,n=1$ satisfies $\{F_1,F_2\}$ yet does not satisfy $F$.

Thus equisatisfiability preserves only the existence of a model, not the exact set of satisfying assignments.