0
$\begingroup$

I am confused about the precise definition of the DPLL algorithm. Various sources tend to define DPLL differently:

  1. In pages 110-114 of the book Handbook of Satisfiability(Editors: Biere, A., Heule, M., Van Maaren, H., Walsh, T. Feb 2009. Volume 185 of Frontiers in Artificial Intelligence and Applications) it defines it as backtracking + unit propagation.

Also can be accessed from: http://reasoning.cs.ucla.edu/fetch.php?id=97&type=pdf (pages 106-110).

  1. In wikipedia: https://en.wikipedia.org/wiki/DPLL_algorithm#:~:text=In%20logic%20and%20computer%20science,solving%20the%20CNF%2DSAT%20problem. it defines it as backtracking + unit propagation + pure literal elimination.

  2. And in original 1962 paper: https://archive.org/details/machineprogramfo00davi/page/n5/mode/2up it mentions 3 rules: one-literal clause rule(unit propagation), affirmitive-negative rule(pure literal elimination) and rule for eliminating atomic formulas(creating resolvents).

Therefore, I am looking for a clear and strict definition of DPLL algorithm. Maybe it should be considered as purely backtracking algorithm and unit propagation and pure literal elimination as its extensions? Or maybe unit propagation is essential part of the algorithm and pure literal elimination is considered to be extention..?

$\endgroup$
1
$\begingroup$

What you are finding is that there are multiple versions of DPLL, all of which might have the name DPLL attached to them, even though they are a little different in some specifics. If you need to distinguish between them, then I suggest you introduce your own terminology. I don't think it really matters which one you call the "one true DPLL algorithm". If you have to pick one, you could use the specification in the original paper, but I suspect it's probably best to understand "DPLL" as referring to a family of closely related algorithms that are very similar to each other but not identical.

"backtracking + unit propagation" is not a definition of an algorithm; it is at best a high-level summary.

$\endgroup$
1
$\begingroup$

I have only one thing to add to D.W.'s answer which is worth considering. This is Wikipedia's pseudocode for DPLL:

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 Φ do
        Φ ← unit-propagate(l, Φ);
    for every literal l that occurs pure in Φ do
        Φ ← pure-literal-assign(l, Φ);
    l ← choose-literal(Φ);
    return DPLL(Φ ∧ {l}) or DPLL(Φ ∧ {not(l)});

Now consider what would happen if choose-literal always chose a pure literal if were it available:

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 Φ do
        Φ ← unit-propagate(l, Φ);
    l ← choose-literal(Φ);
    if l is a pure literal then
        return DPLL(Φ ∧ {l});
    else
        return DPLL(Φ ∧ {l}) or DPLL(Φ ∧ {not(l)});

Are they really different algorithms?

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.