Splitting (Propositional Logic)

Definition

Splitting (Propositional Logic)

Splitting is a recursive decision method for the satisfiability of a propositional formula: instead of evaluating a formula directly, it reduces the problem to simpler subproblems by branching on an atom.

For a formula $A$ and an atom $p$ occurring in $A$, let $A_p^{\top }$ and $A_p^{\perp }$ be the formulas obtained by replacing every occurrence of $p$ by the constant $\top$ (verum) or $\perp$ (falsum), respectively.

Each branch removes $p$, so repeating the step recursively builds a binary splitting tree whose leaves are constant formulas.

Lemma

Splitting over Atoms

Let $p$ be an atom, $A$ a formula, and $I$ an interpretation. Then

$$I\models p⟹I\models A\leftrightarrow A_p^{\top },I/\models p⟹I\models A\leftrightarrow A_p^{\perp }.$$

Under $I$, replacing $p$ by the constant it takes leaves the truth value of $A$ unchanged.

Proof

$I\models p$

Suppose $I\models p$. Then $p$ and $\top$ have the same truth value under $I$, so $I\models p\leftrightarrow \top$. Applying equivalent replacement with $B_1=p$ and $B_2=\top$ replaces every occurrence of $p$ in $A$ by $\top$ and yields $I\models A\leftrightarrow A_p^{\top }$.

$I/\models p$

Suppose $I/\models p$. Then $p$ and $\perp$ have the same truth value under $I$, so $I\models p\leftrightarrow \perp$. Applying equivalent replacement with $B_1=p$ and $B_2=\perp$ yields $I\models A\leftrightarrow A_p^{\perp }$.

Theorem

Splitting

Let $A$ be a formula and $p$ an atom. Then

$$A\text{ is satisfiable}⟺A_p^{\top }\text{ is satisfiable or }{A}_p^{\perp }\text{ is satisfiable}.$$

Proof

$\Rightarrow$

If $I$ satisfies $A$, then $I$ satisfies $p$ or not. If $I\models p$, the lemma gives $I\models A\leftrightarrow A_p^{\top }$, hence $I\models A_p^{\top }$; if $I/\models p$, it gives $I\models A\leftrightarrow A_p^{\perp }$. In either case the matching branch formula is satisfiable.

$\Leftarrow$

Assume $A_p^{\top }$ is satisfiable: some $I\models A_p^{\top }$. Since $p$ does not occur in $A_p^{\top }$, extend $I$ to $I^{\prime }$ with $I^{\prime }(p)=\text{true}$; the value of $A_p^{\top }$ is unchanged, so $I^{\prime }\models A_p^{\top }$. Because $I^{\prime }\models p$, the lemma yields $I^{\prime }\models A\leftrightarrow A_p^{\top }$, hence $I^{\prime }\models A$. Symmetrically, a satisfying interpretation of $A_p^{\perp }$ extends with $I^{\prime }(p)=\text{false}$.