Изменения

|definition = <b>2-SAT <tex>\mathrm 2SAT</tex></b> (2-satisfiability) выполнимость функции — задача распределения аргументов в булевой [[КНФ|КНФ]] функции, записанной в виде [[Специальные_формы_КНФ|2-КНФ (КНФ Крома)]], таким образом, чтобы результат данной функции был равен <tex> 1 </tex>.

== Примеры решения 2-SAT 2SAT ==

</tex>. Построим ориентированный граф со следующими множествами вершинам и ребер:множество вершин <tex> V = \{a, b, c\}, </tex>множество ребер <tex> E = \{(\overline a, b), (\overline b, a), (\overline a, c), (\overline c, a), (b, c), (\overline c, \overline b), (\overline a, \overline b), (a, b)\}</tex>.

Построим граф и рассмотрим Рассмотрим в графе следующие пути:

* <tex> \overline a \to b \to c </tex>.

Т.к. <tex> \overline a \to a </tex>, то <tex> a = 1, \overline a = 0 </tex>.

Т.к. <tex> a \to c </tex> и <tex> a = 1 </tex>, то <tex> c = 1, \overline c = 0 </tex>.

Значения <tex> b </tex> может быть любым, т.к. все вершины, из которых можно добраться в <tex> b </tex> имеют значение ноль.

<b> Ответ: </b> <tex> a = 1, b = 0, c = 1 </tex> или <tex> a = 1, b = 1, c = 1 </tex>.

Построим ориентированный граф со следующими множествами вершинам и ребер:множество вершин <tex> V = \{a, b, c\}, </tex>множество ребер <tex> E = \{(a, c), (\overline c, \overline a), (c, \overline a), (a, \overline c), (\overline a, b), (\overline b, a), (b, a), (\overline b, \overline a)\}</tex>. Заметим следующий путь: <tex> a \to c \to \overline a \to b \to a </tex>. Отсюда следует, что <tex> a \to \overline a \to a </tex>. Следовательно по ранее доказанной теореме, у данной функции решений нет.

Отсюда следует, что <texb> a \to \overline a \to a Ответ: </texb>Решений нет.

== Использование 2-SAT Примечания ==

*[http://e-maxx.ru/algo/2_sat MAXimal :: algo :: Задача 2-SAT 2SAT (2-CNF) ]