NP-полнота задачи о выполнимости булевой формулы в форме КНФ

Определения

• Литералом является переменная или отрицание переменной. Например, [math]x[/math] или [math]\neg y[/math].
• Дизъюнктом называется логическое ИЛИ одного или нескольких литералов. Например, [math]x \vee \neg y \vee z[/math]
• Говорят, что формула записана в конъюнктивной нормальной форме (КНФ), если представляет собой логическое И дизъюнктов.

Определение

[math]CNFSAT = \{\phi \ |\ \phi в КНФ, \phi \in SAT\} [/math] — задача о выполнимости булевой формулы в форме КНФ.

Теорема

[math] CNFSAT \in NPC. [/math]