Splitting Algorithm

logic

Definition

Splitting Algorithm

The splitting algorithm is a recursive decision procedure for the satisfiability of a propositional formula.

Starting from a formula $A$, one chooses a distinguished subformula or atom and forms simpler branch formulas by replacing selected occurrences according to a chosen replacement policy. The resulting branch formulas are then analysed recursively.

Different replacement policies yield different variants of splitting. The recursive execution of the algorithm forms a splitting tree.

The most common variant is equivalent replacement on an atom $p$. In that case one branches on the assumptions $p=\top$ and $p=\perp$, obtaining formulas such as $A_p^{\top }$ and $A_p^{\perp }$.

Replacement Policies

To describe local replacements, write $A[B_1]$ for a formula $A$ with a distinguished occurrence of a subformula $B_1$. If that occurrence is replaced by $B_2$, we write the resulting formula as $A[B_2]$.

Equivalent Replacement

Equivalent replacement

Let $I$ be an interpretation. If $I\models B_1\leftrightarrow B_2$ then $A[B_1]$ and $A[B_2]$ have the same truth value under $I$.

In particular:

• if $I(p)=1$, then $A$ and $A_p^{\top }$ have the same truth value under $I$;
• if $I(p)=0$, then $A$ and $A_p^{\perp }$ have the same truth value under $I$.

This is the replacement policy used in the basic splitting algorithm.

Monotonic Replacement

Monotonic replacement

Define $A_{p,+}^{\top }$ as the formula obtained from $A$ by replacing every positive occurrence of $p$ by $\top$ and leaving every negative occurrence unchanged.

Let $I$ be an interpretation. If

$$I\models B_1\to B_2$$

and the chosen occurrence of $B_1$ in $A[B_1]$ has positive polarity, then

$$I\models A[B_1]\to A[B_2].$$

Since

$$\models p\to \top ,$$

repeated monotonic replacement of positive occurrences gives

$$\models A\to A_{p,+}^{\top }.$$

Thus monotonic replacement is one-sided: it preserves implication, not equivalence.

Monotonic Replacement

Let $A,B_1,B_2$ be formulas, $I$ be an interpretation, and

$$I\models B_1\to B_2$$

• If $\mathrm{pol}(A,\pi )=1$, then $I\models A[B_1{]}_{\pi }\to A[B_2{]}_{\pi }$.

• Likewise, if $\mathrm{pol}(A,\pi )=-1$, then $I\models A[B_2{]}_{\pi }\to A[B_1{]}_{\pi }$.

where $\mathrm{pol}(A,\pi )$ denotes the polarity at position in $A$.

Splitting Step

Splitting over atoms

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

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

This theorem uses equivalent replacement. Monotonic replacement alone is not enough to justify the bidirectional splitting equivalence.

Procedure

Recursive procedure

To decide whether a formula $A$ is satisfiable in the basic equivalent-replacement version:

1. Simplify $A$ as far as possible after substituting truth values.
2. If the resulting formula is $\top$, return satisfiable.
3. If the resulting formula is $\perp$, return unsatisfiable.
4. Otherwise choose an atom $p$ occurring in $A$.
5. Construct $A_p^{\top }$ and $A_p^{\perp }$.
6. Recursively test both formulas.
7. Return satisfiable if at least one recursive call returns satisfiable.

In pseudocode:

function SPLIT(A)
    simplify A
    if A = ⊤ then
        return satisfiable
    if A = ⊥ then
        return unsatisfiable

    choose an atom p in A
    return SPLIT(A_p^⊤) or SPLIT(A_p^⊥)

Properties

Correctness

The basic splitting algorithm is sound and complete for propositional satisfiability, because equivalent replacement preserves satisfiability exactly.

Termination

Every recursive call fixes the truth value of at least one further atom. Hence, for a formula with $n$ atoms, the recursion depth is at most $n$.

Complexity

In the worst case, the algorithm explores both branches for each of $n$ atoms, so it may inspect up to $2^n$ cases. It is therefore a brute-force tree-like search algorithm, although simplification may prune branches early.

Relation to Other Methods

Related procedures

The recursive execution of the algorithm can be represented as a splitting tree.

Compared with truth tables, splitting only explores assignments that arise from the chosen recursive branches.

Polarity becomes relevant for monotonic replacement: there one replaces only positive occurrences and obtains a one-sided consequence of the original formula.

The DPLL algorithm refines the basic splitting idea by adding simplification rules such as unit propagation.

Example

Equivalent vs. monotonic replacement

Let

$$A=(p\vee q)\wedge (\neg p\vee r).$$

We compare the two replacement policies for the atom $p$.

First, use equivalent replacement. We replace every occurrence of $p$.

For $p=\top$:

$$\begin{array}{rl}{A}_p^{\top }& =(\top \vee q)\wedge (\neg \top \vee r)\\ & =\top \wedge (\perp \vee r)\\ & =r\end{array}$$

For $p=\perp$:

$$\begin{array}{rl}{A}_p^{\perp }& =(\perp \vee q)\wedge (\neg \perp \vee r)\\ & =q\wedge (\top \vee r)\\ & =q\end{array}$$

Hence

$$A\text{ is satisfiable }⟺r\text{ is satisfiable or }q\text{ is satisfiable}.$$

This is the branching step used in the basic splitting algorithm.

Now consider monotonic replacement. The occurrence of $p$ in $(p\vee q)$ is positive, while the occurrence of $p$ in $(\neg p\vee r)$ is negative.

Therefore only the positive occurrence may be replaced by $\top$:

$$\begin{array}{rl}{A}_{p,+}^{\top }& =(\top \vee q)\wedge (\neg p\vee r)\\ & =\top \wedge (\neg p\vee r)\\ & =\neg p\vee r\end{array}$$

So monotonic replacement yields

$$A\to A_{p,+}^{\top },$$

but not an equivalence.

Indeed, if $p=\perp$, $q=\top$, and $r=\perp$, then

$$A=\top \text{but}r=\perp .$$

So replacing the negative occurrence as well would be too strong.

Thus:

• equivalent replacement replaces all occurrences and yields the splitting equivalence;
• monotonic replacement replaces only positive occurrences and yields a one-sided consequence.