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
leaf. On input
:
- simplify
; - if
, answer satisfiable; - if
, answer unsatisfiable; - otherwise choose an atom
occurring in and answer satisfiable iff the algorithm answers satisfiable for or for . It is sound and complete by the splitting equivalence and terminates because every recursive call removes one atom.