1632
правки
Изменения
2SAT
,rollbackEdits.php mass rollback
}}
== Алгоритм решения ==
Рассмотрим любой дизъюнкт функции: <tex> a \vee b </tex>.
Несложно заметить, что это равнозначно записи <tex>(\overline a \to b \wedge \overline b \to a) </tex>.
{{Теорема
|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>Докажем необходимость: Пусть 2-SAT <tex>\mathrm {2SAT}</tex> имеет решение. <br>Докажем, что не может быть такого, чтобы для любой переменной <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> было верным), <tex> x </tex> должен быть равен <tex> 1</tex>. С другой стороны для того, чтобы из <tex> x </tex> достичь <tex> \overline x </tex> <tex> (\overline x \to \overline x </tex> было верным), <tex> x </tex> должен быть равен 0. Отсюда следует противоречие. <br> <br>
<tex>(\Leftarrow)</tex>Докажем достаточность: Пусть для любой переменной <tex> x </tex> из вершины <tex> x </tex> нельзя достичь <tex> \overline x </tex> и из вершины <tex> \overline x </tex> нельзя достичь <tex> x </tex> одновременно. <br>Докажем, что этого достаточно, чтобы 2-SAT <tex>\mathrm {2SAT}</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>, то <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>. Противоречие.
}}
Данная функция эквивалентна функции
<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>.
Значения <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>
(\overline a \vee c) \wedge
(\overline c \vee \overline a) \wedge
(a \vee b) \wedge
(\overline b \vee a)
</tex>
Данная функция эквивалентна функции
<tex>
a \to c \wedge
\overline c \to \overline a \wedge
c \to \overline a \wedge
a \to \overline c \wedge
\overline a \to b \wedge
\overline b \to a \wedge
b \to a \wedge
\overline b \to \overline a
</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>.
Заметим следующий путь: <tex> a \to c \to \overline a \to b \to a </tex>.
Отсюда следует, что <tex> a \to \overline a \to a </tex>.
Следовательно по ранее доказанной теореме, у данной функции решений нет.
<b> Ответ: </b> Решений нет.
== Использование 2SAT ==
Решение <tex>\mathrm {2SAT}</tex> может потребоваться в следующих задачах:
*латинские квадраты<ref> [https://ru.wikipedia.org/wiki/Латинский_квадрат Википедия — Латинские квадраты] </ref>,
*квазигруппы<ref>[https://ru.wikipedia.org/wiki/Квазигруппа_(социология) Википедия — Квазигруппы]</ref>,
*числа Рамсея<ref>[https://ru.wikipedia.org/wiki/Теорема_Рамсея#.D0.A7.D0.B8.D1.81.D0.BB.D0.B0_.D0.A0.D0.B0.D0.BC.D1.81.D0.B5.D1.8F Википедия — Числа Рамсея]</ref>,
*система Штейнера<ref>[https://ru.wikipedia.org/wiki/Система_Штейнера Википедия — Система Штейнера]</ref>,
*проектирование протоколов (пример: для сетевых коммуникаций),
*электронная коммерция (Электронные аукционы и автоматизированные брокеры,
*теории кодирования, криптографии,
*проектирование и тестирование лекарств (мед. препаратов).
== См. также ==
*[[3CNFSAT | NP-полнота задачи о выполнимости булевой формулы в форме 3-КНФ]]
== Примечания ==
<references/>
== Источники информации ==
*[http://e-maxx.ru/algo/2_sat MAXimal :: algo :: Задача 2-SAT 2SAT (2-CNF) ]*[https://en.wikipedia.org/wiki/2-satisfiability Википедия — 2-satisfiability - Википедия]
[[Категория: Дискретная математика и алгоритмы]]
[[Категория: Булевы функции ]]