This is pseudo-code version of Knuth's algorithm C from 7.1.1.

For each proposition P, set LAST(p) <- Lambda, TRUTH(p) <- 0;
s <- 0;
For each clause c, 
  set CONCLUSION(c) <- v, COUNT(c) <- k;
  if k = 0 and TRUTH(v) = 0 set TRUTH(v) <- 1, S[s] <- v, s <- s+1
For each 1 <= j <= k
  create hypothesis record h;
  CLAUSE(h) <- c, PREV(h) <- LAST(u[j]), LAST(u[j]) <- h

while s neq 0 do
   s <- s-1, p <- S[s], h <- LAST(p);
   while h neq Lambda do
      c <- CLAUSE(h), COUNT(c) <- COUNT(c)-1;
      if COUNT(c) = 0
         p <- CONCLUSION(c);
         if TRUTH(p) = 0
           then TRUTH(p) <- 1, S[s] <- p; s <- s+1;
      h <- PREV(h)