Хорн-выполнимость

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

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

Выполнимость Хорна на самом деле является одной из самых «сложных» или «наиболее выразительных» задач, которая, как известно, вычислима за полиномиальное время в том смысле, что это P -полная задача. ^[1]

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

Алгоритм

Проблема выполнимости по Хорну разрешима за линейное время . ^[4] Проблема определения истинности количественных формул Хорна также может быть решена за полиномиальное время. ^[5]Алгоритм с полиномиальным временем для выполнимости Хорна является рекурсивным :

Первое условие завершения — это формула, в которой все существующие в данный момент предложения содержат отрицательные литералы. В этом случае всем переменным в предложениях может быть присвоено значение false.
Второе условие завершения — пустое предложение. В этом случае формула не имеет решений.
В остальных случаях формула содержит предложение с положительной единицей. $l$ , поэтому мы выполняем единичное распространение : литерал $l$ установлено значение true, все предложения, содержащие $l$ удалены, и все пункты, содержащие $\neg l$ удалите этот литерал. Результатом является новая формула Хорна, повторяем еще раз.

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

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

Примеры

Тривиальный случай

В формуле Хорна

(\neg а \lor \neg б \lor c) \land

(\neg б \lor \neg c \lor d) \land

(\neg ж \lor \neg а \lor б) \land

(\neg е \lor \neg c \lor а) \land

(\neg е \lor ж) \land

(\neg d \lor е) \land

(\neg b \lor \neg c)

,

каждое предложение имеет отрицательный литерал. Следовательно, установка каждой переменной значения false удовлетворяет всем условиям и, следовательно, является решением.

Разрешимый случай

В формуле Хорна

(\neg а \lor \neg б \lor c) \land

(\neg б \lor \neg c \lor ж) \land

(\neg ж \lor б) \land

(\neg е \lor \neg c \lor а) \land

(ж) \land

(\neg d \lor е) \land

(\neg b \lor \neg c)

,

одно предложение заставляет f быть правдой. Установка f в true и упрощение дает

(\neg а \lor \neg б \lor c) \land

(б) \land

(\neg е \lor \neg c \lor а) \land

(\neg d \lor е) \land

(\neg b \lor \neg c)

.

Теперь b должно быть правдой. Упрощение дает

(\neg а \lor c) \land

(\neg е \lor \neg c \lor а) \land

(\neg d \lor е) \land

(\neg c)

.

Теперь это тривиальный случай, поэтому всем остальным переменным можно присвоить значение false. Таким образом, удовлетворяющее задание

а = ложь

,

б = правда

,

с = ложь

,

д = ложь

,

е = ложь

,

е = правда

.

Неразрешимый случай

В формуле Хорна

(\neg а \lor \neg б \lor c) \land

(\neg б \lor \neg c \lor ж) \land

(\neg ж \lor б) \land

(\neg е \lor \neg c \lor а) \land

(ж) \land

(\neg d \lor е) \land

(\neg b)

,

одно предложение заставляет f быть правдой. Последующее упрощение дает

(\neg а \lor \neg б \lor c) \land

(б) \land

(\neg е \lor \neg c \lor а) \land

(\neg d \lor е) \land

(\neg b)

.

Теперь b должно быть правдой. Упрощение дает

(\neg а \lor c) \land

(\neg е \lor \neg c \lor а) \land

(\neg d \lor е) \land

()

.

Мы получили пустое предложение, следовательно, формула невыполнима.

Обобщение

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

Спутниковый спутник с двумя рупорами

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

См. также

Ссылки

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

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

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

[CookNguyen2010-1] Стивен Кук; Фуонг Нгуен (2010). Логические основы сложности доказательства . Издательство Кембриджского университета. п. 224. ИСБН 978-0-521-51729-4 . ( авторский черновой вариант 2008 года , см. стр.213е)

[2] Райнер Хэнле (2001). «Продвинутая многозначная логика». В Дов М. Габбай, Франц Гюнтер (ред.). Справочник по философской логике . Том. 2 (2-е изд.). Спрингер. п. 373. ИСБН 978-0-7923-7126-7 .

[FittingOrlowska2003-3] Райнер Хэнле (2003). «Сложность многозначной логики». В Мелвине Фиттинге, Еве Орловской (ред.). За пределами двух: теория и приложения многозначной логики . Спрингер. ISBN 978-3-7908-1541-2 .

[4] Даулинг, Уильям Ф.; Галье, Жан Х. (1984), «Алгоритмы линейного времени для проверки выполнимости пропозициональных формул Хорна», Journal of Logic Programming , 1 (3): 267–284, doi : 10.1016/0743-1066(84)90014- 1 , МР 0770156

[buningkarpinski-5] Бунинг, Гонконг; Карпински, Марек; Флогель, А. (1995). «Разрешение для количественных логических формул» . Информация и вычисления . 117 (1). Эльзевир: 12–18. дои : 10.1006/inco.1995.1025 .

[6] Льюис, Гарри Р. (1978). «Переименование набора предложений в набор Хорна» . Журнал АКМ . 25 (1): 134–135. дои : 10.1145/322047.322059 . МР 0468315 . .

[7] Аспвалл, Бенгт (1980). «Распознавание замаскированных случаев NR (1) проблемы выполнимости». Журнал алгоритмов . 1 (1): 97–103. дои : 10.1016/0196-6774(80)90007-3 . МР 0578079 .

[8] Эбрар, Жан-Жак (1994). «Линейный алгоритм переименования набора предложений в набор Хорна». Теоретическая информатика . 124 (2): 343–350. дои : 10.1016/0304-3975(94)90015-9 . МР 1260003 . .

[9] Чандру, Виджая; Коллетт Р. Куллард ; Питер Л. Хаммер; Мигель Монтаньес; Сяорун Сунь (2005). «О переименовываемых функциях Хорна и обобщенных функциях Хорна». Анналы математики и искусственного интеллекта . 1 (1–4): 33–47. дои : 10.1007/BF01531069 .

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]