Алгоритм Дэвиса – Патнэма

В логике и информатике алгоритм Дэвиса-Патнэма был разработан Мартином Дэвисом и Хилари Патнэмом для проверки достоверности логической формулы первого порядка с использованием процедуры принятия решения на основе разрешения для логики высказываний . Поскольку набор допустимых формул первого порядка рекурсивно перечислим, но не рекурсивен , общего алгоритма решения этой проблемы не существует. Следовательно, алгоритм Дэвиса – Патнэма завершается только на допустимых формулах. Сегодня термин «алгоритм Дэвиса-Патнэма» часто используется как синоним процедуры пропозиционального решения на основе разрешения ( процедура Дэвиса-Патнэма ), которая на самом деле является лишь одним из шагов исходного алгоритма.

Обзор

Два прогона процедуры Дэвиса-Патнэма на примерах пропозициональных оснований. *Сверху вниз, слева:* начиная с формулы $(a\lor b\lor c)\land (b\lor \lnot c\lor \lnot f)\land (\lnot b\lor e)$ , алгоритм разрешается на $b$ , а затем дальше $c$ . Поскольку дальнейшее разрешение невозможно, алгоритм останавливается; поскольку пустое предложение не может быть получено, результат является « *выполнимым* ». *Справа:* Решение данной формулы на $b$ , затем дальше $a$ , затем дальше $c$ дает пустое предложение; следовательно, алгоритм возвращает « *неудовлетворительно* ».

Процедура основана на теореме Эрбрана , которая подразумевает, что невыполнимая формула имеет невыполнимый основной экземпляр , и на том факте, что формула действительна тогда и только тогда, когда ее отрицание невыполнимо. В совокупности эти факты означают, что для доказательства истинности φ достаточно доказать, что основной пример ¬φ невыполним. Если φ недействителен, то поиск неудовлетворительного наземного экземпляра не прекращается.

Процедура проверки правильности формулы φ примерно состоит из этих трех частей:

поместите формулу ¬φ в предварительную форму и исключите кванторы
генерировать все экземпляры пропозициональной основы, один за другим
проверьте, выполним ли каждый экземпляр.
- Если какой-то экземпляр неудовлетворителен, верните, что φ действителен. В противном случае продолжайте проверку.

Последняя часть представляет собой решатель SAT, основанный на разрешении (как показано на иллюстрации), с активным использованием единичного распространения и чисто буквальным исключением (исключением предложений с переменными, которые встречаются в формуле только положительно или только отрицательно). ^{[ нужны разъяснения ]}

Algorithm DP SAT solver
    Input: A set of clauses Φ.
    Output: A Truth Value: true if Φ can be satisfied, false otherwise.

function DP-SAT(Φ)
   repeat
       // unit propagation:
       while Φ contains a unit clause {l} do
           for every clause c in Φ that contains l do
              Φ ← remove-from-formula(c, Φ);
           for every clause c in Φ that contains ¬l do
              Φ ← remove-from-formula(c, Φ);
              Φ ← add-to-formula(c \ {¬l}, Φ);
       // eliminate clauses not in normal form:
       for every clause c in Φ that contains both a literal l and its negation ¬l do
           Φ ← remove-from-formula(c, Φ);
       // pure literal elimination:
       while there is a literal l all of which occurrences in Φ have the same polarity do
           for every clause c in Φ that contains l do
              Φ ← remove-from-formula(c, Φ);
       // stopping conditions:
       if Φ is empty then
           return true;
       if Φ contains an empty clause then
           return false;
       // Davis-Putnam procedure:
       pick a literal l that occurs with both polarities in Φ
       for every clause c in Φ containing l and every clause n in Φ containing its negation ¬l do
           // resolve c with n:
           r ← (c \ {l}) ∪ (n \ {¬l});
           Φ ← add-to-formula(r, Φ);
       for every clause c that contains l or ¬l do
           Φ ← remove-from-formula(c, Φ);

« ←» означает присвоение . Например, « самый большой ← элемент » означает, что значение самого большого изменяется на значение элемента .
« return » завершает алгоритм и выводит следующее значение.

На каждом этапе решателя SAT генерируемая промежуточная формула эквивалентна , но, возможно, не эквивалентна исходной формуле. Шаг разрешения приводит к экспоненциальному увеличению размера формулы в худшем случае.

Алгоритм Дэвиса-Патнэма-Логеманна-Лавленда представляет собой усовершенствованный в 1962 году шаг пропозициональной выполнимости процедуры Дэвиса-Патнэма, который в худшем случае требует только линейного объема памяти. Он избегает разрешения правила разделения : алгоритма обратного отслеживания, который выбирает литерал l , а затем рекурсивно проверяет, выполнима ли упрощенная формула с l, которому присвоено истинное значение, или упрощенная формула с l, которому присвоено ложное значение. Он по-прежнему составляет основу для сегодняшних (по состоянию на 2015 год) наиболее эффективных комплексных решателей SAT .

См. также

Гербрандизация

Ссылки

Дэвис, Мартин; Патнэм, Хилари (1960). «Вычислительная процедура для количественной теории» . Журнал АКМ . 7 (3): 201–215. дои : 10.1145/321033.321034 .
Дэвис, Мартин; Логеманн, Джордж; Лавленд, Дональд (1962). «Машинная программа для доказательства теорем» . Коммуникации АКМ . 5 (7): 394–397. дои : 10.1145/368273.368557 . hdl : 2027/mdp.39015095248095 .
Р. Дектер; И. Риш. «Направленное решение: пересмотр процедуры Дэвиса-Патнэма». В Дж. Дойле, Э. Сандеволле и П. Торассо (ред.). Принципы представления знаний и рассуждения: Учеб. Четвертой Международной конференции (КР'94) . Кауфманн. стр. 134–145.
Джон Харрисон (2009). Справочник по практической логике и автоматизированным рассуждениям . Издательство Кембриджского университета. стр. 79–90 . ISBN 978-0-521-89957-4 .