CNF против Horn Выполнимость

Я знаю, что легче доказать, что формула рога выполнима. Мой вопрос: почему с рупорной формулой проще, чем с обычным CNF?


person noctua    schedule 16.03.2015    source источник


Ответы (1)


Наличие или отсутствие выполнимости Хорна можно показать в линейном времени. Вот хороший введение с некоторыми примерами. Решение можно найти с помощью распространения единиц без возврата.

Псевдокод из Калифорнийского университета в Беркли лекций< /а>:

введите здесь описание изображения

Выполнимость для общих выражений CNF является классической проблемой NP-complete. Алгоритмы с полиномиальным временем не известны для выполнимости CNF (за исключением случаев, когда P=NP).

person Axel Kemper    schedule 18.03.2015