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

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

Обзор

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

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

Процедура примерно состоит из трех частей:

• поместите формулу в Prenex формировать и исключать кванторы
• генерировать все пропозициональные основания один за другим
• проверьте, является ли каждый экземпляр выполнимым

Последняя часть, вероятно, самая новаторская и работает следующим образом (см. Рисунок):

• для каждой переменной в формуле
  • для каждого пункта ${\displaystyle c}$ содержащий переменную и каждое предложение ${\displaystyle n}$ содержащее отрицание переменной
    • разрешить c и п и добавляем резольвенту в формулу
  • удалить все исходные предложения, содержащие переменную или ее отрицание

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

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

Смотрите также

• Гербирование

использованная литература

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