Изменения

== Рассмотрим функцию, записанную в виде 2-SAT Выполнимость ==КНФ (КНФ Крома).

Рассмотрим функцию, записанную в виде 2-КНФ (КНФ Крома). <br> {{Определение|definition =2-SAT выполнимость данной функции - — эта задача распределения аргументов таким образом, чтобы результат данной функции был равен 1.}}

Рассмотрим любой дизъюнкт функции: (<tex> a || \vee b) </tex> <br>Несложно заметить, что это равнозначно записи !<tex>(\overline a => \to b и !\wedge b =\to \overline a) </tex> a <br>

Построим ориентированный граф, где вершинами будут аргументы и их отрицание, а ребрами будут ребра вида: !<tex>\overline a =\to b </tex> b и !<tex> b =\to \overline a </tex> a для каждого дизъюнкта функции (<tex> a || \vee b) </tex> <br>

Для того, чтобы данная задача 2-SAT имела решение, необходимо и достаточно, чтобы для любой переменной <tex> x </tex> из вершины <tex> x </tex> нельзя достичь !<tex> \overline x </tex> и из вершины !<tex> \overline x </tex> нельзя достичь <tex> x </tex> одновременно. <tex>(!\overline x => \to x && \wedge x => !\to \overline x) </tex>

Докажем, что не может быть такого, чтобы для любой переменной <tex> x </tex> из вершины <tex> x </tex> можно достичь !<tex> \overline x </tex> и из вершины !<tex> \overline x </tex> можно достичь <tex> x </tex> одновременно. <tex>(!\overline x => \to x && \wedge x => !\to \overline x) </tex> <br>Тогда чтобы из !<tex> \overline x </tex> достичь <tex> x </tex> <tex> (!\overline x =\to x </tex> x) x было верным), <tex> x </tex> должен быть равен 1. С другой стороны для того, чтобы из <tex> x </tex> достичь !<tex> \overline x </tex> <tex> (!\overline x \to x =</tex> x) было верным), <tex> x </tex> должен быть равен 0. Отсюда следует противоречие. <br> <br>

Пусть для любой переменной <tex> x </tex> из вершины <tex> x </tex> нельзя достичь !<tex> \overline x </tex> и из вершины !<tex> \overline x </tex> нельзя достичь <tex> x </tex> одновременно. <br>

Пусть из !<tex> \overline x </tex> можно достичь <tex> x</tex>, но из вершины <tex> x </tex> нельзя достичь !<tex> \overline x</tex>. Докажем, что из <tex> x </tex> не достижимо такой <tex> y</tex>, что из <tex> y </tex> достижимо !<tex> \overline y</tex>. (т.е. <tex> x => \to y => !\to \overline y. (x = 1, y = 0))</tex>. <br>Если из <tex> x =\to y </tex> y, то (!<tex> \overline x || \vee y)</tex>, отсюда следует (!<tex> \overline y =\to \overline x </tex> !x). Тогда <tex> x => \to y => !\to \overline y =\to \overline x </tex> !x. Следовательно <tex> x =\to \overline x </tex> !x. Противоречие.

== Ссылки См. также == *[http://neerc.ifmo.ru/wiki/index.php?title=КНФ - КНФ]*[http://neerc.ifmo.ru/wiki/index.php?title=Специальные_формы_КНФ - Специальные формы КНФ. КНФ в форме Крона (2-КНФ)]== Источники информации ==