I'm trying to understand DPLL algorithm for solving SAT problem. And here it is:Algorithm DPLL  Input: A set of clauses .  Output: A Truth Value.function DPLL()   if  is a consistent set of literals       then return true;   if  contains an empty clause       then return false;   for every unit clause l in         unit-propagate(l, );   for every literal l that occurs pure in         pure-literal-assign(l, );   l  choose-literal();   return DPLL(  l) or DPLL(  not(l));At first, I don't clearly understand how unit-propagate(l, ), pure-literal-assign(l, ) and choose-literal() work. I'll try to guess on particular examples. Correct me please if I do something wrong. For the first one unit-propagate(a, (0 v -a)  (a v b)  (b v d)  (f v g) v ...) we will have ((0 v -0)  (0 or 1)  (1 v d)  (f v g)  ... = (f v g) v ...,having a = 0, b = 1.For second procedurepure-literal-assign(a, (a v b v c)  (d v -b v a)  (-d v b))result is (b v c)  (d v -b)  (-d v b),assigning a = 1.And finally choose-literal() just returns some random (in common case) unassigned literal for further computations.Now, I don't understand why algorithm has such strange conditions for finishing? Why does it work?Thanks!
Understanding DPLL algorithm
algorithms;logic;satisfiability;sat solvers
It works because the three cases you mention will remove every non-pure variable after some number of steps, but it is crucial that you also consider the recursive step, namely $\mbox{dpll}(\phi \land l) \lor \mbox{dpll}(\phi \land \neg l)$.After a recursive step, you are guaranteed to have at least one unit clause, so the unit clause will be set to its value and hence all the variable will in the end be assigned a value.I think your misunderstanding must arise from the recursive calls.  Observe that if you have any formula $\phi = ((a \lor b \lor c) \land \cdots)$, then $\mbox{choose-literal}(\phi)$ will return some unassigned variable, say $a$.  The recursive call will then be with $\phi \land a$ which will be $(a \lor b \lor c) \land \cdots) \land (a)$.  And then $\mbox{unit-literal}(\phi)$ will return $a$ and set it to true.  The other recursive call is equivalent, but with $\phi \land (\neg a)$ so $\mbox{unit-literal}(\phi)$ will still return $a$ and set $a$ to false.