title: DPLL algorithm definition
body: <p>I am having some problems understanding the DPLL algorithm and I was wondering if anyone could explain it to me because I think my understanding is incorrect.</p>
  
  <p>The way I understand it is, I take some set of literals and if some every clause is true the model is true but if some clause is false then the model is false.</p>
  
  <p>I recursively check the model by looking for a unit clause, if there is one I set the value for that unit clause to make it true, then update the model. Removing all clauses that are now true and remove all literals which are now false.</p>
  
  <p>When there are no unit clauses left, I chose any other literal and assign values for that literal which make it true and make it false, then again remove all clauses which are now true and all literals which are now false.</p>