1
правка
Изменения
2SAT
,→Первый пример
Построим [[Основные_определения_теории_графов|ориентированный граф]], где вершинами будут аргументы и их отрицание, а ребрами будут ребра вида: <tex>\overline a \to b </tex> и <tex> \overline b \to a </tex> для каждого дизъюнкта функции <tex> a \vee b </tex>. {{ОпределениеТеорема|definition statement=2-SAT выполнимость данной функции — эта Для того, чтобы данная задача распределения аргументов таким образом<tex>\mathrm {2SAT}</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>.|proof=<tex>(\Rightarrow)</tex>Докажем достаточность: Пусть <tex>\mathrm {2SAT}</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>. Тогда чтобы из <tex> \overline x </tex> достичь <tex> x </tex> <tex> (\overline x \to x </tex> было верным), <tex> x </tex> должен быть равен <tex> 1 </tex>. С другой стороны для того, чтобы результат данной функции был из <tex> x </tex> достичь <tex> \overline x </tex> <tex> (x \to \overline x </tex> было верным), <tex> x </tex> должен быть равен 0. Отсюда следует противоречие. <tex>(\Leftarrow)</tex>Докажем необходимость: Пусть для любой переменной <tex> x </tex> из вершины <tex> x </tex> нельзя достичь <tex> \overline x </tex> и из вершины <tex> \overline x </tex> нельзя достичь <tex> x </tex> одновременно. Докажем, что этого достаточно, чтобы <tex>\mathrm {2SAT}</tex> имело решение. Пусть из <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>. Если из <tex> x \to y </tex>, то <tex> \overline x \vee y </tex>, отсюда следует <tex> \overline y \to \overline x </tex>. Тогда <tex> x \to y \to \overline y \to \overline x </tex>. Следовательно <tex> x \to \overline x </tex>. Противоречие.
}}
Теперь мы можем собрать весь алгоритм воедино:
#Построим граф импликаций.
#<i>Найдём в этом графе [[Отношение_связности,_компоненты_связности#Сильная связность | компоненты сильной связности]] за время <tex>O(N + M)</tex></i>, где <tex> N </tex> — количество вершин в графе (удвоенное количество переменных), а <tex> M </tex> — количество ребер графа (удвоенное количество дизъюнктов).
#Пусть <tex>comp[v]</tex> — это номер компоненты сильной связности, которой принадлежит вершине <tex>v</tex>. Проверим, что для каждой переменной <tex>x</tex> вершины <tex>x</tex> и <tex>\overline x</tex> лежат в разных компонентах, т.е. <tex>comp[x] \ne comp[\overline x]</tex>. Если это условие не выполняется, то вернуть <i>решение не существует</i>.
#Если <tex>comp[x] > comp[\overline x]</tex>, то переменной <tex>x</tex> выбираем значение <tex> \mathtt {true}</tex>, иначе — <tex> \mathtt {false}</tex>.
Компоненты сильной связности найдем за <tex>O(N + M)</tex>, затем проверим каждую из <tex>N</tex> переменных за <tex>O(N)</tex>. Следовательно асимптотика <tex>O(N + M)</tex>.
== Примеры решения 2SAT ==
=== Первый пример ===
Рассмотрим следующую функцию: <tex> (a \vee b) \wedge
(a \vee c) \wedge
(\overline b \vee c) \wedge
(\overline b \vee a) </tex>
Данная функция эквивалентна функции
<tex>
\overline a \to b \wedge
\overline b \to a \wedge
\overline a \to c \wedge
\overline c \to a \wedge
b \to c \wedge
\overline c \to \overline b \wedge
\overline a \to \overline b \wedge
a \to b
</tex>.
Построим ориентированный граф со следующими множествами вершинам и ребер:
множество вершин <tex> V = \{a, b, c, \overline a, \overline b, \overline 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), (b, a)\}</tex>.
Рассмотрим в графе следующие пути:
* <tex> \overline a \to b \to a </tex>
* <tex> \overline a \to \overline b \to a </tex>
* <tex> \overline c \to a </tex>
* <tex> a \to c </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>.
<b> Ответ: </b> <tex> a = 1, b = 0, c = 1 </tex> или <tex> a = 1, b = 1, c = 1 </tex>.
Построим ориентированный граф со следующими множествами вершинам и ребер:
множество вершин V = <tex>\{a, b, c, \overline a, \overline b, \overline 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>.
== См. также ==
*[http://neerc.ifmo.ru/wiki/index.php?title=КНФ - КНФ]*[http://neerc.ifmo.ru/wiki/index.php?title=Специальные_формы_КНФ 3CNFSAT | NP- Специальные формы КНФ. КНФ полнота задачи о выполнимости булевой формулы в форме Крона (23-КНФ)]] == Примечания ==<references/>
== Источники информации ==
*[http://e-maxx.ru/algo/2_sat MAXimal :: algo :: Задача 2-SAT 2SAT (2-CNF) ]*[https://en.wikipedia.org/wiki/2-satisfiability Википедия — 2-satisfiability] [[Категория: Дискретная математика и алгоритмы]] [[Категория: Булевы функции ]]
