- КНФ
-
Конъюнкти́вная норма́льная фо́рма (КНФ) в булевой логике — нормальная форма, в которой булева формула имеет вид конъюнкции нескольких дизъюнктов.
Например, следующие формулы записаны в КНФ:
Конъюнктивная нормальная форма удобна для автоматического доказательства теорем.
Содержание
Приведение булевой формулы к КНФ
Любая булева формула может быть приведена к КНФ. Впрочем, при этом размер булевой формулы может возрасти экспоненциально. Так, например, 2n дизъюнктов потребуется, чтобы записать следующую формулу:
Формальная грамматика, описывающая КНФ
Следующая формальная грамматика описывает все формулы, приведенные к КНФ:
- <КНФ> → <дизъюнкт>
- <КНФ> → <КНФ> ∧ <дизъюнкт>
- <дизъюнкт> → <литерал>
- <дизъюнкт> → (<дизъюнкт> ∨ <литерал>)
- <литерал> → <терм>
- <литерал> → ¬<терм>
где <терм> обозначает произвольную булеву переменную.
Задача выполнимости формулы в КНФ
В теории вычислительной сложности важную роль играет задача выполнимости булевых формул в конъюнктивной нормальной форме. Эта задача NP-полна, и она сводится к задаче 3-SAT, которая в свою очередь сводится ко многим другим NP-полным задачам.
См. также
Wikimedia Foundation. 2010.