Naming

logic propositional-logic

Definition

Naming

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

$$n\leftrightarrow A$$

and replace the chosen occurrence of $A$ in $F$ by $n$.

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

Preservation of Satisfiability

Preservation of Satisfiability

Let $S$ be a set of formulas and $B$ a formula. Let $n$ be an atom not occurring in $S$ and not occurring in $B$.

Then $S$ is satisfiable if and only if $S\cup \{n\leftrightarrow B\}$ 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

$$F=p_1\leftrightarrow (p_2\leftrightarrow (p_3\leftrightarrow (p_4\leftrightarrow (p_5\leftrightarrow p_6))))$$

A direct CNF transformation of this nested equivalence expands each $\leftrightarrow$ 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

$$A=p_5\leftrightarrow p_6$$

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

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

$$n\leftrightarrow (p_5\leftrightarrow p_6).$$

Step 3 — Replace in the original formula.
Substitute $n$ for the occurrence of $p_5\leftrightarrow p_6$ in $F$:

$$\begin{array}{rl}{F}_1& =p_1\leftrightarrow (p_2\leftrightarrow (p_3\leftrightarrow (p_4\leftrightarrow n)))\\ F_2& =n\leftrightarrow (p_5\leftrightarrow p_6)\end{array}$$

The set $\{F_1,F_2\}$ has the same models as $F$ when restricted to the original variables $\{p_1,\dots ,p_6\}$.

Not equivalent $\{F_1,F_2\}$ is not logically equivalent to the original formula $F$, because $n$ is an extra variable. An interpretation that assigns a value to $n$ inconsistent with $p_5\leftrightarrow p_6$ can satisfy $\{F_1,F_2\}$ without satisfying $F$. Equivalence holds only after restricting to the original variables.

The set

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