有限布尔公式上的搜索
DPLL处理的对象是有限命题公式的合取范式，即若干子句的合取，每个子句又是文字的析取；文字是变量或其否定。它要回答是否存在一个真假赋值，使全部子句同时成立。名称结合了戴维斯、普特南、洛格曼和洛夫兰的姓氏；1962年的回溯程序承接了此前的研究，但不能与1960年的变量消去路线直接等同。
算法不必一开始就填写所有变量，而是维护部分赋值。某子句已有真文字，便已满足；若所有文字都假，便出现冲突；剩下未定文字的子句还可能由后续赋值满足。分支实际上把尚未解决的问题拆为某变量取真和取假两个互斥、合起来穷尽的情况。
先传播，再作决定
单元传播处理当前只剩一个未定文字、其余文字均为假的子句。要满足该子句，唯一剩余文字必须为真，因此这个赋值不是猜测。新赋值又可能使别的子句变成单元子句，传播应持续到没有新的强制赋值，或者发现冲突。
传播停下不等于已经解答问题。若仍有未满足子句，算法选择未定变量作分支决定；若冲突出现，则撤销本分支的决定及其引出的赋值，尝试相反方向。经典表述也可加入纯文字规则，但仅靠这些简化规则不能解决任意命题公式。
一个产生冲突的分支
考虑四个子句：p∨q、¬p∨r、¬p∨¬r、¬q∨s。先决定p为真，第二个子句便强制r为真，第三个却强制r为假，因而该分支不可能满足原公式。冲突只排除了p为真的情况，并没有证明整个公式不可满足。
回溯后改取p为假。第一个子句随即要求q为真，第四个再要求s为真；含¬p的两个子句都已满足。于是p假、q真、s真，加上任意r值，构成满足赋值。这个例子区分了决定、传播和冲突，也说明不能把一次失败当成全局否定。
与消去法及学习算法的区别
早期戴维斯—普特南方法用归结生成子句以消去变量；DPLL的主干则是保存赋值轨迹、分支和回溯。现代CDCL求解器在这一框架上分析冲突，保留原公式所蕴含的学习子句，并可跳过与冲突无关的决策层。这些能力不是最简DPLL已经包含的全部步骤。
有限变量保证完整回溯搜索能够终止，穷尽所有失败分支才可判定不可满足。不过搜索树在最坏情况下仍可非常大。变量选择、传播实现和输入结构会影响实践速度；工程上的成功不能改写为对任意可满足性实例的多项式时间保证。