Русская Википедия:Конъюнктивная нормальная форма
Конъюнкти́вная норма́льная фо́рма (КНФ) в булевой логике — нормальная форма, в которой булева формула имеет вид конъюнкции дизъюнкций литералов. Конъюнктивная нормальная форма удобна для автоматического доказательства теорем. Любая булева формула может быть приведена к КНФ.[1] Для этого можно использовать: закон двойного отрицания, закон де Моргана, дистрибутивность.
Примеры и контрпримеры
Формулы в КНФ:
- <math>\neg A \wedge (B \vee C),</math>
- <math>(A \vee B) \wedge (\neg B \vee C \vee \neg D) \wedge (D \vee \neg E),</math>
- <math>A \wedge B.</math>
Формулы не в КНФ:
- <math>\neg (B \vee C),</math>
- <math>(A \wedge B) \vee C,</math>
- <math>A \wedge (B \vee (D \wedge E)).</math>
Но эти 3 формулы не в КНФ эквивалентны следующим формулам в КНФ:
- <math>\neg B \wedge \neg C,</math>
- <math>(A \vee C) \wedge (B \vee C),</math>
- <math>A \wedge (B \vee D) \wedge (B \vee E).</math>
Построение КНФ
Алгоритм построения КНФ
1) Избавиться от всех логических операций, содержащихся в формуле, заменив их основными: конъюнкцией, дизъюнкцией, отрицанием. Это можно сделать, используя равносильные формулы:
- <math>A \rightarrow B = \neg A \vee B,</math>
- <math>A \leftrightarrow B = (\neg A \vee B) \wedge (A \vee \neg B).</math>
2) Заменить знак отрицания, относящийся ко всему выражению, знаками отрицания, относящимися к отдельным переменным высказываниям на основании формул:
- <math>\neg (A \vee B) = \neg A \wedge \neg B,</math>
- <math>\neg (A \wedge B) = \neg A \vee \neg B.</math>
3) Избавиться от знаков двойного отрицания.
4) Применить, если нужно, к операциям конъюнкции и дизъюнкции свойства дистрибутивности и формулы поглощения.
Пример построения КНФ
Приведем к КНФ формулу
- <math> F = ( X \rightarrow Y ) \wedge (( \neg Y \rightarrow Z ) \rightarrow \neg X ).</math>
Преобразуем формулу <math>F</math> к формуле, не содержащей <math>\rightarrow</math>:
- <math> F = ( \neg X \vee Y ) \wedge ( \neg ( \neg Y \rightarrow Z ) \vee \neg X ) = ( \neg X \vee Y ) \wedge ( \neg ( \neg \neg Y \vee Z ) \vee \neg X ).</math>
В полученной формуле перенесем отрицание к переменным и сократим двойные отрицания:
- <math> F = ( \neg X \vee Y) \wedge ((\neg Y \wedge \neg Z) \vee \neg X).</math>
По закону дистрибутивности получим КНФ:
- <math>F = (\neg X \vee Y) \wedge (\neg X \vee \neg Y) \wedge (\neg X \vee \neg Z).</math>
k-конъюнктивная нормальная форма
k-конъюнктивной нормальной формой называют конъюнктивную нормальную форму, в которой каждая дизъюнкция содержит ровно k литералов.
Например, следующая формула записана в 2-КНФ:
- <math>(A \lor B) \land (\neg B \lor C) \land (B \lor \neg C).</math>
A≡((x→y)→!x)→(x→(y&x));
Переход от КНФ к СКНФ
Если в простой дизъюнкции не хватает какой-то переменной (например, z), то добавляем в неё выражение :<math>Z \wedge \neg Z = 0</math> (это не меняет самой дизъюнкции), после чего раскрываем скобки с использованием распределительного закона:
- <math>(X \vee Y) \wedge (X \vee \neg Y \vee \neg Z) = (X \vee Y \vee (Z \wedge \neg Z)) \wedge (X \vee \neg Y \vee \neg Z) = (X \vee Y \vee Z) \wedge (X \vee Y \vee \neg Z) \wedge (X \vee \neg Y \vee \neg Z).</math>
Таким образом, из КНФ получена СКНФ.
Формальная грамматика, описывающая КНФ
Следующая формальная грамматика описывает все формулы, приведенные к КНФ:
- <КНФ> → <дизъюнкт>
- <КНФ> → <КНФ> ∧ <дизъюнкт>
- <дизъюнкт> → <литерал>;
- <дизъюнкт> → (<дизъюнкт> ∨ <литерал>)
- <литерал> → <терм>
- <литерал> → ¬<терм>
где <терм> обозначает произвольную булеву переменную.
Задача выполнимости формулы в КНФ
В теории вычислительной сложности важную роль играет задача выполнимости булевых формул в конъюнктивной нормальной форме. Согласно теореме Кука, эта задача NP-полна, и она сводится к задаче о выполнимости формул в 3-КНФ, которая сводится и к которой в свою очередь сводятся другие NP-полные задачи.
Задача о выполнимости 2-КНФ формул может быть решена за линейное время.
Особенности обозначений
Следует отметить, что для удобства восприятия в качестве обозначения конъюнкции и дизъюнкции часто используют символы арифметического умножения и сложения, при этом символ умножения часто опускается. В этом случае формулы булевой алгебры выглядят как алгебраические полиномы, что более привычно для глаза, однако иногда может привести к недоразумениям.
Например, следующие записи эквивалентны:
- <math>(A \vee B) \wedge (\neg B \vee C \vee \neg D) \wedge (D \vee \neg E);</math>
- <math>(A \vee B) \wedge (\overline{B} \vee C \vee \overline{D}) \wedge (D \vee \overline{E});</math>
- <math>(A \vee B) \cdot (\overline{B} \vee C \vee \overline{D}) \cdot (D \vee \overline{E});</math>
- <math>(A \vee B)(\overline{B} \vee C \vee \overline{D})(D \vee \overline{E});</math>
- <math>(A + B)(\overline{B} + C + \overline{D})(D + \overline{E}).</math>
По этой причине КНФ в русскоязычной литературе иногда называют «произведением сумм», что является калькой с английского термина «product of sums».
См. также
- Дизъюнктивная нормальная форма
- Совершенная дизъюнктивная нормальная форма
- Совершенная конъюнктивная нормальная форма
- Конъюнктивный одночлен
- Дизъюнктивный одночлен
Примечания
Литература
- Ю.И. Галушкина, А.Н. Марьямов: Конспект лекций по дискретной математике - 2-е изд., испр. - М.: Айрис-пресс, 2008. - 176 с. - (Высшее образование)
Ссылки
- ↑ Ошибка цитирования Неверный тег
<ref>
; для сносокnf
не указан текст