Davis-Putnam (DPLL) procedure
Martin Davis, Hillary Putnam, George Logemann, and Donald Loveland (1962)

dp(in  ATOMS : set of propositional atoms;
       S : Set of propositional formulas in CNF)
  return: either a valuation on ATOMS satisfying S or NIL if none exists.

V : array[ATOMS];

{ for (A in ATOMS) do V[A] = UNBOUND;
  return dp1(ATOMS,S,V) }
end dp

dp1(ATOMS,S,V) {                             % call S,V by value 
   loop {       % Loop as long as there are easy cases to cherry pick 

%  BASE OF THE RECURSION: SUCCESS OR FAILURE 

    if (S is empty)    %  Success: All clauses are satisfied   
       { for (A in ATOMS)
           if (V[A] == UNBOUND) then assign V[A] either TRUE or FALSE;
         return(V);
       }

    else if (some clause in S is empty) %  Failure: Some clause 
          then return NIL;            %  is unsatisfiable under V 
  
%  EASY CASES: PURE LITERAL ELIMINATION AND FORCED ASSIGNMENT 
    else if (there exists a literal L in S  % Pure literal elimination 
               such that the negation of L does not appear in S)
          then { V = obviousAssign(L,V);
                 delete every clause containing L from S;
               }

    else if (there exists a clause C in S       %  Forced assignment 
                containing a single literal L)
           then { V = obviousAssign(L,V)
                  S = propagate(atom(L), S, V);
                }

    else exitloop;  %  No easy cases found 
  }   %  end loop 


%  HARD CASE: PICK SOME ATOM AND TRY EACH ASSIGNMENT IN TURN 
  pick atom A such that V[A] == UNBOUND;   %  Try one assignment 
  V[A] = TRUE;
  S1 = copy(S);
  S1 = propagate(A, S1, V);
  VNEW = dp1(ATOMS,S1,V);
  if (VNEW != NIL) then return(VNEW); % Found a satisfying valuation

%  If V[A] = TRUE didn't work, try V[A] = FALSE;
  V[A] = FALSE;
  S1 = propagate(A, S, V);
  return(dp1(ATOMS,S1,V)); % Either found a satisfying valuation or backtrack
} end dp1

% Propagate the effect of assigning atom A to be value V.
% Delete every clause where A appears with sign V
% Delete every literal where A appears with sign not V.
 
propagate(A,S,V) {
  for (each clause C in S)_ do
     if ((A in C and V[A]==TRUE) or (~A in C and V[A]==FALSE))
      then delete C from S
     else if (A in C and V[A]==FALSE) then delete A from C
     else if (~A in C and V[A]==TRUE) then delete ~A from C;
  return S;
}
end propagate.

% Given a literal L with atom A, make V[A] the sign indicated by L.

obviousAssign(L,V) {
  if (L is an atom A) then V[A] = TRUE;
  else if (L has the form ~A) then V[A] = FALSE;
}