Explore Courses Blog Tutorials Interview Questions
0 votes
in AI and Deep Learning by (50.2k points)

I'm having trouble understanding the DPLL algorithm for checking the satisfiability of a sentence in propositional logic.
enter image description here

This algorithm is taken from the book Artificial Intelligence A modern approach. I'm finding it really confusing with those many function recursions. In particular, what does the EXTEND() function do, and what's the purpose behind the recursive calls to DPLL() ?

1 Answer

0 votes
by (108k points)

DPLL algorithm is basically a combination of three concepts:

  • Backtracking

  • Unit propagation

  • Pure literal rule


Answering your first question, the function call EXTEND(P, true, model) will return a new partial model in which P has true value. 

And for your second question, the DPLL is essentially a backtracking algorithm, and that is the main idea behind the recursive calls.

The algorithm is building a solution while trying assignments, you have a partial solution that might prove successful or not-successful as you go on.

The basic idea of the algorithm is:

  1. "Guess" a variable

  2. Find all unit clauses created from the last assignment and assign the needed value

  3. Iteratively retry step 2 until there is no change (found transitive closure)

  4. If the current assignment cannot yield true for all clauses - fold back from recursion and retry a different assignment

  5. If it can - "guess" another variable (recursively invoke and return to 1)

For a better understanding of the DPLL algorithm, refer the following link:

Browse Categories