Get possible solution with DPLL algorithm

Question

I was implementing the following DPLL algorithm in Prolog:

DPLL implementation

The implementation tells me if there is a solution for the given CNF, but is it also possible with DPLL algorithm to get one or all possible solutions?

Answer 1

Yes, you just need to keep track of how you got to the empty clause set.

In fact, in Prolog this is straightforward: add a list of literals as an argument to the function. When you make the first call, use an empty list, and then add $L$ to this list of literals whenever $\{ L \} \in F$ applies.

So, roughly, create a function DP(F,Ls) with:

DPLL([],[]).

DPLL(F,_):- element([],F), fail.

DPLL(F',[L|Ls]):- element([L],F),reduce(F,L,F').

DPLL([[L]|F],[L|Ls]):- element(C,F), element(L,F).

DPLL([[L']|F],[L'|Ls]):- element(C,F), element(L,F),complement(L,L').

(note that this is very inefficient, as it ends up splitting on every literal and complement that occur in any of the clauses ... so, for example, if some literal $A$ occurs multiple times in the clauses, then it will split on $A$ that many times, whereas obviously once should suffice)