def DPLL(S: Set[Clause]) : $\BB$ =
  val S1 = subsumption(UnitProp(S))
  if $\emptyset$ $\in$ S1 then false // unsat
  else if S1 has only unit clauses then true // S1 gives satisfying assignment
  else
     // instead of doing general resolution, make more unit literals, recurse
     val L = a literal from a clause of S1 where {L} $\notin$ S1
     DPLL(S1 $\cup$ {{L}}) || DPLL(S1 $\cup$ {{$\overline L$}})
 
def UnitProp(S: Set[Clause]): Set[Clause] = // Unit Propagation (BCP)
  if C $\in$ S, unit U $\in S$, $\bar U \in C$, C - {$\bar U$} $\notin$ S
  then UnitProp((S - {C}) $\cup$ {C - {$\bar U$}}) else S

def subsumption(S: Set[Clause]): Set[Clause] =
  if C1,C2 $\in$ S such that C1 $\subseteq$ C2 
  then subsumption(S - {C2})  else S