I am confused about the precise definition of the DPLL algorithm. Various sources tend to define DPLL differently:
- 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).
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.
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..?