Naming

logic propositional-logic

Definition

Naming

Let be a non-trivial subformula of a propositional formula . Introduce a new propositional variable that does not occur in . Add the defining equivalence

and replace the chosen occurrence of in by .

The resulting set of formulas is equisatisfiable with on the original variables, but not logically equivalent to .

Preservation of Satisfiability

Preservation of Satisfiability

Let be a set of formulas and a formula. Let be an atom not occurring in and not occurring in .

Then is satisfiable if and only if is satisfiable.

In other words, naming an existing subformula by a new variable does not change whether the original set of formulas has a model.

Examples

Avoiding exponential blow-up

Let

A direct CNF transformation of this nested equivalence expands each into two clauses, and the distributive steps multiply the clauses at each level. The resulting CNF is exponential in the nesting depth.

To avoid this, we introduce a fresh variable for the innermost non-atomic subformula.

Step 1 — Choose a subformula.
Select

as the subformula to name. This is the innermost non-trivial equivalence.

Step 2 — Introduce a fresh variable.
Let be a new atom not occurring in . Add the definition

Step 3 — Replace in the original formula.
Substitute for the occurrence of in :

The set has the same models as when restricted to the original variables .

Not equivalent

The set is not logically equivalent to the original formula , because is an extra variable. An interpretation that assigns a value to inconsistent with can satisfy without satisfying . Equivalence holds only after restricting to the original variables.

Step 4 — Transform each piece separately.
Each of and is now much smaller than the fully expanded CNF of . We can transform each independently and then conjoin the results. The total size is linear in the number of connectives, rather than exponential.