Splitting Algorithm (Propositional Logic)

Definition

Splitting Algorithm (Propositional Logic)

The splitting algorithm is the recursive decision procedure for satisfiability that searches the splitting tree of a formula for a $\top$ leaf.

On input $A$:

1. simplify $A$;
2. if $A=\top$, answer satisfiable;
3. if $A=\perp$, answer unsatisfiable;
4. otherwise choose an atom $p$ occurring in $A$ and answer satisfiable iff the algorithm answers satisfiable for $A_p^{\top }$ or for $A_p^{\perp }$.

It is sound and complete by the splitting equivalence and terminates because every recursive call removes one atom.