This lecture is about DPLL. A DPLL is an algorithm to establish whether a CNF is satisfiable, based on resolution. It originates from a paper appeared in 1962 by Davis, Logemann and Loveland. Here we see an early version of this paper. Well, then you think the letters are DLL, what's the P coming from? Well, paper was based on an earlier paper by Davis and Putnam, that was this paper and that justifies the P in DPLL. DPLL is still this algorithm, this idea of an algorithm to establish satisfiability or unsatisfiability of propositional formula, is still the basis of current SAT/SMT solvers. What's the idea? The idea is first we apply unit resolution as long as possible and if you cannot proceed by unit resolution only or trivial observations, then choose a variable p and introduce case analysis on p and "Not p". So one case is, add p to the formula and continue by it and the other case is add "Not p" to the formula and continue by that and then you can go on recursively. Here, apply unit resolution as long as possible means, as long as a clause occurs consisting of a single literal l, called a unit clause, then we may remove "Not l" from all clauses containing "Not l". Essentially, this is the unit resolution. But we also remove all clauses containing l since they are redundant if we have the clause l. In the algorithm, we denote this by unit resolution. The algorithm looks as follows. DPLL applied on X starts by, first apply unit resolution on X and put the result on X. It can be the case that X is empty. If everything has been removed by this unit resolution where we remove clauses containing l, then it can be the case that, well, then we are finished and then we have a satisfying assignment as we will see in a minute then the algorithm returns satisfiable. If we derive the empty clause, then this case has been proven to be unsatisfiable and in the remaining case, we should continue by starting the case analysis and that means we choose variable p occurring in X which exist since X is not empty and then we recursively apply the same algorithm on the formula X we have now to which we add p and also X to which we add the unit clause, "Not p". Termination of this algorithm always holds since in every recursive call, the number of variable decreases, strictly decreases. Why is that? Well, if we add the unit clause, p, and we do unit resolution on p, after this unit resolution, p doesn't occur anymore. So, at least one variable is completely removed by this unit resolution. If satisfiable is returned by the algorithm, then you can see that all involved unit clauses yield a satisfying assignment. So then we have proved that a formula is satisfiable. In the remaining case, we can consider the algorithm as finding a big case analysis and if never satisfiable is returned, then it's a big case analysis ending at every case in the empty clause being a contradiction. So we can say, we have split up the whole formula in several cases. Every case yields a contradiction and that has approved that our formula is unsatisfiable. So, DPLL is a complete method to establish satisfiability. Let's consider an example. Here we have a CNF consisting of nine clauses and we want to establish whether this formula is satisfiable or not. We see that no unit resolution is possible since none of the nine clauses is a unit clause. So we have to choose a variable and do a case analysis on this variable. Let's choose variable p. That means first we add p, but if we add p as an extra clause, we can do unit resolution. The two red clauses contain "Not p", so there we can do unit resolution and we may remove "Not p" from these two clauses yielding to new unit clauses, "Not s" and "Not r". But now, we may do a unit resolution on these new clauses, "Not s" and "Not r". If we do so, we can apply then on the two red clauses if we see the clause q or s unit resolution with "Not s" yields the new unit clause, q. If we consider the clause r or t, unit resolution with "Not r" yields the new unit clause, t and we can continue. Now we have q and t. If we look at the red clause "Not q" or "Not t", and we have our clause q, we can derive the new clause "Not t". But now we see we have t and "Not t" which yields a contradiction. It can be seen as a unit resolution step, but in any case, we derived the empty clause. So, this ends this first case in which we added p. In the remaining case, we have to add "Not p". Well, if we add "Not p", we can do unit resolution on the two red clauses p or r and p or s yielding two new unit clauses, r and s. Again, using r and using s, we can derive two new unit clauses q and t. Using q and to the clause, "Not q or "Not t", we can derive a new unit clause, "Not t". Now we have both the unit clause t and "Not t" yielding the empty clause. So also, in the second case, we have bottom, we have derived a contradiction. So in both cases, we a found contradiction showing that this formula is unsatisfiable. In this simple example, we only have two cases typically in more complicated examples. This goes on recursively several times and we can have thousands of cases to consider. Let's consider a next example consisting of only eight clauses. In fact, it's the same example as before, only the last clause has been removed. Again we see that in the starting CNF, there is no unit clause so we should start by case analysis and again, let's choose p as the variable on which we do case analysis. Well, the case for p, adding p is exactly the same, yields a contradiction s in the example which you saw. But in the next case, we have "Not p". We add "Not p" to this formula and then we can do unit resolution yielding r and s as two new unit clauses based on the two red clauses, p or r and p or s. If we continue, we have the clause s and we have the clause "Not s" or t, unit resolution yields t. Once we have t, we have the clause "Not q" or "Not t", we can derive the clause "Not q". How to continue? We see we have added "Not p", we have derived r, we have derived s, we have derived t, and we have derived "Not q". So, for every letter, we have either the variable itself or its negation in the list and if we do the unit resolution, where we remove everything as indicated, nothing remains. So here we are in the situation where nothing remains. Now we can see that indeed, "Not p", "Not q", r, s, and, t yields a satisfying assignment which is easily checked. But, it's also easily checked that in a general setting, this holds as soon as we find satisfiable then the corresponding values yield a satisfying assignment. Concluding, we can state that this algorithm DPLL is a complete method for satisfiability, based on unit resolution and case analysis. The efficiency of this algorithm strongly depends on the choice of the variable. If no unit resolution is possible anymore, we have to choose a variable and typically if we apply this on the big formula, there is a lot of choice and some choice will lead to much more efficient computation than others. In fact, current SAT solvers follow this scheme combined with good heuristics for variable choice and several optimizations. Thank you.
