Изменения
Нет описания правки
====Определения====
* ''Литералом'' является переменная или отрицание переменной. Например, <tex>x</tex> или <tex>\neg y</tex>.
* ''Дизъюнктом'' называется логическое '''ИЛИ''' одного или нескольких литералов. Например, <tex>x \vee \neg y \vee z</tex>
* Говорят, что формула записана в ''конъюнктивной нормальной форме'' (CNFКНФ), если представляет собой логическое '''И''' дизъюнктов.=== Определение ===<tex>CNFSAT = \{\phi \| в КНФ, \phi \in SAT\} </tex> — задача о выполнимости булевой формулы в форме КНФ.== Теорема ==<tex> CNFSAT \in NPC. </tex>== Доказательство ==
