Роговая выполнимость - Horn-satisfiability

В формальная логика, Роговая выполнимость, или же HORNSAT, - это проблема определения того, является ли данный набор пропозициональных Роговые оговорки удовлетворительно или нет. Хорн-выполнимость и предложения Хорна названы в честь Альфред Хорн.

Основные определения и терминология

Оговорка Хорна - это пункт максимум с одним положительным буквальный, называется голова предложения и любое количество отрицательных литералов, образующих тело статьи. Формула Хорна - это пропозициональная формула образована соединение Роговых статей.

Проблема выполнимости Горна решается в линейное время.^[1] Проблема определения истинности количественных формул Хорна также может быть решена за полиномиальное время.^[2]Полиномиальный алгоритм выполнимости Хорна основан на правиле единичное распространение: если формула содержит предложение, состоящее из одного литерала ${\displaystyle l}$ (единичное предложение), тогда все предложения, содержащие ${\displaystyle l}$ (кроме самого предложения unit) удаляются, и все предложения, содержащие ${\displaystyle \neg l}$ удалите этот литерал. Результатом второго правила может быть предложение unit, которое распространяется таким же образом. Если нет единичных предложений, формула может быть удовлетворена, просто установив все оставшиеся переменные отрицательными. Формула невыполнима, если это преобразование порождает пару противоположных единичных предложений ${\displaystyle l}$ и ${\displaystyle \neg l}$. Выполнимость Horn на самом деле является одной из «самых сложных» или «наиболее выразительных» проблем, которая, как известно, может быть вычислена за полиномиальное время в том смысле, что это п-полный проблема.^[3]

Этот алгоритм также позволяет определять присвоение истинности выполнимых формул Хорна: все переменные, содержащиеся в предложении единицы измерения, устанавливаются на значение, удовлетворяющее этому предложению единицы; все остальные литералы имеют значение false. Результирующее присваивание является минимальной моделью формулы Хорна, то есть присваиванием, имеющим минимальный набор переменных, которому присвоено значение true, где сравнение выполняется с использованием включения набора.

Используя линейный алгоритм для единичного распространения, алгоритм является линейным по размеру формулы.

Обобщением класса формул Хорна являются формулы переименовываемого Горна, которые представляют собой набор формул, которые могут быть преобразованы в форму Хорна, заменяя некоторые переменные их соответствующим отрицанием. Проверить наличие такой замены можно за линейное время; следовательно, выполнимость таких формул находится в P, поскольку ее можно решить, сначала выполнив эту замену, а затем проверив выполнимость полученной формулы Хорна.^[4][5][6][7] Выполнимость Horn и переименовываемая выполнимость Horn обеспечивают один из двух важных подклассов выполнимости, которые разрешимы за полиномиальное время; другой такой подкласс 2-выполнимость.

Проблема выполнимости Хорна также может быть задана пропозициональной многозначная логика. Алгоритмы обычно не являются линейными, но некоторые из них полиномиальны; см. обзор у Hähnle (2001 или 2003).^[8][9]

Dual-Horn SAT

Двойной вариант Horn SAT: Dual-Horn SAT, в котором каждое предложение имеет не более одного отрицательного литерала. Отрицание всех переменных преобразует экземпляр Dual-Horn SAT в Horn SAT. В 1951 году Хорном было доказано, что двухканальный SAT п.

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

• Распространение единицы
• Проблема логической выполнимости
• 2-выполнимость

Рекомендации

1. Доулинг, Уильям Ф .; Галье, Жан Х. (1984), «Линейные алгоритмы для проверки выполнимости пропозициональных формул Хорна», Журнал логического программирования, 1 (3): 267–284, Дои:10.1016/0743-1066(84)90014-1, МИСТЕР  0770156
2. Buning, H.K .; Карпинский, Марек; Флогель, А. (1995). «Разрешение для количественных булевых формул». Информация и вычисления. Эльзевир. 117 (1): 12–18. Дои:10.1006 / inco.1995.1025.
3. Стивен Кук; Фыонг Нгуен (2010). Логические основы сложности доказательства. Издательство Кембриджского университета. п. 224. ISBN  978-0-521-51729-4.
4. Льюис, Гарри Р. (1978). «Переименование набора предложений в набор Рогов». Журнал ACM. 25 (1): 134–135. Дои:10.1145/322047.322059. МИСТЕР  0468315..
5. Аспвалл, Бенгт (1980). «Распознавание замаскированных NR (1) примеров проблемы выполнимости». Журнал алгоритмов. 1 (1): 97–103. Дои:10.1016/0196-6774(80)90007-3. МИСТЕР  0578079.
6. Эбрар, Жан-Жак (1994). «Линейный алгоритм для переименования набора предложений в набор Горна». Теоретическая информатика. 124 (2): 343–350. Дои:10.1016/0304-3975(94)90015-9. МИСТЕР  1260003..
7. Чандру, Виджая; Коллетт Р. Куллар; Питер Л. Хаммер; Мигель Монтаньес; Сяожун Сунь (2005). «О переименовываемых и обобщенных функциях Горна». Анналы математики и искусственного интеллекта. 1 (1–4): 33–47. Дои:10.1007 / BF01531069.
8. Райнер Хенле (2001). «Продвинутая многозначная логика». В Дов М. Габбай, Франц Гюнтнер (ред.). Справочник по философской логике. 2 (2-е изд.). Springer. п. 373. ISBN  978-0-7923-7126-7.
9. Райнер Хенле (2003). «Сложность многозначной логики». В Мелвин Фиттинг, Ева Орловска (ред.). За пределами двух: теория и приложения многозначной логики. Springer. ISBN  978-3-7908-1541-2.

дальнейшее чтение

• Грэдель, Эрих; Колайтис, Phokion G .; Либкин, Леонид; Маартен, Маркс; Спенсер, Джоэл; Варди, Моше Ю.; Венема, Иде; Вайнштейн, Скотт (2007). Теория конечных моделей и ее приложения. Тексты по теоретической информатике. Серия EATCS. Берлин: Springer-Verlag. ISBN  978-3-540-00428-8. Zbl  1133.03001.