КНФ

Конъюнкти́вная норма́льная фо́рма (КНФ) в булевой логике — нормальная форма, в которой булева формула имеет вид конъюнкции нескольких дизъюнктов.

Например, следующие формулы записаны в КНФ:

$A \and B$

$A\!$

$(A \or B) \and \neg A$

$(A \or B \or \neg C) \and (\neg D \or E \or F) \and (C \or D) \and B$

Конъюнктивная нормальная форма удобна для автоматического доказательства теорем.

Приведение булевой формулы к КНФ

Любая булева формула может быть приведена к КНФ. Впрочем, при этом размер булевой формулы может возрасти экспоненциально. Так, например, 2ⁿ дизъюнктов потребуется, чтобы записать следующую формулу:

$(X_1 \and Y_1) \or (X_2 \and Y_2) \or \dots \or (X_n \and Y_n)$

Формальная грамматика, описывающая КНФ

Следующая формальная грамматика описывает все формулы, приведенные к КНФ:

<КНФ> → <дизъюнкт>

<КНФ> → <КНФ> ∧ <дизъюнкт>

<дизъюнкт> → <литерал>

<дизъюнкт> → (<дизъюнкт> ∨ <литерал>)

<литерал> → <терм>

<литерал> → ¬<терм>

где <терм> обозначает произвольную булеву переменную.

Задача выполнимости формулы в КНФ

В теории вычислительной сложности важную роль играет задача выполнимости булевых формул в конъюнктивной нормальной форме. Эта задача NP-полна, и она сводится к задаче 3-SAT, которая в свою очередь сводится ко многим другим NP-полным задачам.

См. также

• Дизъюнктивная нормальная форма
• k-конъюнктивная нормальная форма