Первый рассматриваемый здесь алгоритм часто называют алгоритмом Дэвиса-Патнем в честь авторов оригинальной статьи, в которой он был опубликован, Мартина Дэвиса и Хилари Патнем [336]. Затем этот алгоритм фактически стал одной из версий, описанных Дэвисом, Логеманом и Лавлендом [335], поэтому мы будем называть его DPLL по первым буквам фамилий всех четырех авторов. Алгоритм DPLL принимает на входе некоторое высказывание в конъюнктивной нормальной форме — высказывание, представленное как множество выражений. Как и алгоритмы Backtracking-Search и TT-Entails?, он фактически выполняет рекурсивный перебор в глубину всех возможных моделей. Но в этом алгоритме реализованы три описанных ниже усовершенствования, и этим он отличается от простой схемы, применяемой в алгоритме TT-Entails?.

• Раннее завершение. Алгоритм обнаруживает, должно ли данное высказывание быть истинным или ложным, даже с помощью частично завершенной модели. Выражение является истинным, если истинен любой его литерал, даже притом что для других литералов еще не определены истинностные значения; поэтому об истинности всего высказывания в целом можно судить еще до того, как модель будет составлена полностью. Например, высказывание является истинным, если истинен литерал А, независимо от значений литералов В и С. Аналогичным образом, высказывание является ложным, если ложно любое его выражение, а это происходит, если каждый литерал этого выражения является ложным. Опять-таки, такая ситуация может возникнуть задолго до того, как модель будет полностью составлена. Раннее завершение позволяет обойтись без исследования целых поддеревьев в пространстве поиска.

•    Эвристика чистого символа. Чистым символом называется символ, который всегда появляется с одним и тем же "знаком" во всех выражениях. Например, в трех выражениях символ А является чистым, поскольку он появляется только в виде положительных литералов, чистым можно также считать символ в, который появляется только в виде отрицательных литералов, а символ С считается нечистым. Можно легко показать, что если некоторое высказывание имеет модель, то это — модель с чистыми символами, значения которым присвоены так, чтобы их литералы приняли значение true, поскольку при таком условии ни одно выражение не может стать ложным. Следует отметить, что при определении чистоты символа алгоритм может игнорировать выражения, в отношении которых уже известно, что они истинны в модели, составленной до сих пор. Например, если модель содержит присваивание в= false, то выражение уже является истинным, а символ С становится чистым, поскольку присутствует только в выражении

•    Эвристика единичного выражения. Единичное выражение было определено ранее как выражение только с одним литералом. В контексте алгоритма DPLL оно также относится к выражениям, в которых в данной модели всем литералам, кроме одного, уже было присвоено значение false. Например, если модель содержит присваивание в= false, то выражение становится единичным выражением, поскольку оно эквивалентно выражению, или просто. Очевидно, для того, чтобы это выражение приняло истинное значение, литералу С должно быть присвоено значение false. Эвристика единичного выражения предусматривает присваивание значений всем таким символам до того, как происходит переход к обработке оставшейся части высказывания. Одним из важных следствий из этой эвристики является то, что любая попытка доказать (путем опровержения) истинность литерала, который уже находится в базе знаний, немедленно приводит к успеху (упр. 7.16). Следует также отметить, что присваивание значения одному единичному выражению может привести к созданию еще одного единичного выражения; например, после присваивания символу С значения false единичным становится выражение, что влечет за собой присваивание истинного значения символу л. Такое "каскадное" распространение форсированных присваиваний называется распространением единичных выражений. Оно напоминает процесс прямого логического вывода с применением хорновских выражений, а в действительности, если рассматриваемое высказывание в конъюнктивной нормальной форме содержит только хорновские выражения, то алгоритм DPLL по сути сводится к алгоритму прямого логического вывода.