В формальной логике выполнимость по Хорну , или HORNSAT , — это проблема решения, является ли данный набор пропозициональных предложений Хорна выполнимым или нет. Предложения Хорна и Хорна названы в честь Альфреда Хорна .
Предложение Хорна — это предложение , содержащее не более одного положительного литерала , называемого заголовком предложения, и любого количества отрицательных литералов, образующих тело предложения. Формула Хорна — это пропозициональная формула, образованная соединением предложений Хорна.
Выполнимость Хорна на самом деле является одной из самых «сложных» или «наиболее выразительных» задач, которая, как известно, вычислима за полиномиальное время в том смысле, что это P -полная задача. [1]
Проблему выполнимости Хорна можно также задать для пропозициональных многозначных логик . Алгоритмы обычно не линейны, но некоторые являются полиномиальными; обзор см. в Hähnle (2001 или 2003). [2] [3]
Алгоритм
Проблема выполнимости по Хорну разрешима за линейное время . [4]
Проблема определения истинности количественных формул Хорна также может быть решена за полиномиальное время. [5]
Алгоритм с полиномиальным временем для определения выполнимости Хорна является рекурсивным :
- Первое условие завершения — это формула, в которой все существующие в данный момент предложения содержат отрицательные литералы. В этом случае всем переменным, присутствующим в предложениях, можно присвоить значение false.
- Второе условие завершения — пустое предложение. В этом случае формула не имеет решений.
- В других случаях формула содержит положительное предложение единицы , поэтому мы выполняем распространение единицы : литералу присваивается значение true, все содержащие его предложения удаляются, а из всех предложений, содержащих этот литерал, удаляется. Результатом является новая формула Хорна, повторяем еще раз.
Этот алгоритм также позволяет определить истинность выполнимых формул Хорна: всем переменным, содержащимся в единичном предложении, присваиваются значения, удовлетворяющие этому единичному предложению; все остальные литералы имеют значение false. Результирующее присваивание представляет собой минимальную модель формулы Хорна, то есть присваивание, имеющее минимальный набор переменных, которым присвоено значение true, где сравнение выполняется с использованием включения множества.
Используя линейный алгоритм для единичного распространения, алгоритм линеен по размеру формулы.
Примеры
Тривиальный случай
В формуле Хорна
- (¬ а ∨ ¬ б ∨ c ) ∧
- (¬ б ∨ ¬ c ∨ d ) ∧
- (¬ ж ∨ ¬ а ∨ б ) ∧
- (¬ е ∨ ¬ c ∨ а ) ∧
- (¬ е ∨ ж ) ∧
- (¬ d ∨ е ) ∧
- (¬ б ∨ ¬ c ) ,
каждое предложение имеет отрицательный литерал. Следовательно, установка каждой переменной значения false удовлетворяет всем условиям и, следовательно, является решением.
Разрешимый случай
В формуле Хорна
- (¬ а ∨ ¬ б ∨ c ) ∧
- (¬ б ∨ ¬ c ∨ ж ) ∧
- (¬ ж ∨ б ) ∧
- (¬ е ∨ ¬ c ∨ а ) ∧
- ( ж ) ∧
- (¬ d ∨ е ) ∧
- (¬ б ∨ ¬ c ) ,
одно предложение заставляет f быть правдой. Установка f в true и упрощение дает
- (¬ а ∨ ¬ б ∨ c ) ∧
- ( б ) ∧
- (¬ е ∨ ¬ c ∨ а ) ∧
- (¬ d ∨ е ) ∧
- (¬ б ∨ ¬ c ) .
Теперь b должно быть правдой. Упрощение дает
- (¬ а ∨ c ) ∧
- (¬ е ∨ ¬ c ∨ а ) ∧
- (¬ d ∨ е ) ∧
- (¬ в ) .
Теперь это тривиальный случай, поэтому всем остальным переменным можно присвоить значение false. Таким образом, удовлетворяющее задание
- а = ложь ,
- б = правда ,
- с = ложь ,
- д = ложь ,
- е = ложь ,
- е = правда .
Неразрешимый случай
В формуле Хорна
- (¬ а ∨ ¬ б ∨ c ) ∧
- (¬ б ∨ ¬ c ∨ ж ) ∧
- (¬ ж ∨ б ) ∧
- (¬ е ∨ ¬ c ∨ а ) ∧
- ( ж ) ∧
- (¬ d ∨ е ) ∧
- (¬ б ) ,
одно предложение заставляет f быть правдой. Последующее упрощение дает
- (¬ а ∨ ¬ б ∨ c ) ∧
- ( б ) ∧
- (¬ е ∨ ¬ c ∨ а ) ∧
- (¬ d ∨ е ) ∧
- (¬ б ) .
Теперь b должно быть правдой. Упрощение дает
- (¬ а ∨ c ) ∧
- (¬ е ∨ ¬ c ∨ а ) ∧
- (¬ d ∨ е ) ∧
- () .
Мы получили пустое предложение, следовательно, формула невыполнима.
Обобщение
Обобщением класса формул Хорна являются формулы переименовываемого Хорна, которые представляют собой набор формул, которые можно поместить в форму Хорна путем замены некоторых переменных их соответствующим отрицанием. Проверку существования такой замены можно производить за линейное время; следовательно, выполнимость таких формул находится в 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.
