24
правки
Изменения
2SAT
,Добавлено применение 2-SAT. Добавлены новые ссылки
Построим ориентированный граф, где вершинами будут аргументы и их отрицание, а ребрами будут ребра вида: <tex>\overline a \to b </tex> и <tex> b \to \overline a </tex> для каждого дизъюнкта функции <tex> a \vee b </tex> <br>
{{Теорема
|statement=
Для того, чтобы данная задача 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>
|proof== Доказательство ==
Пусть 2-SAT имеет решение. <br>
Докажем, что не может быть такого, чтобы для любой переменной <tex> x </tex> из вершины <tex> x </tex> можно достичь <tex> \overline x </tex> и из вершины <tex> \overline x </tex> можно достичь <tex> x </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>. <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>. Противоречие.
}}
== Применение 2-SAT задач ==
Алгоритм для решения 2-SAT может быть применим во всех задачах, где есть набор величин, каждая из которых может принимать 2 возможных значения, и есть связи между этими величинами:
* Расположение текстовых меток на карте или диаграмме. Имеется в виду нахождение такого расположения меток, при котором никакие две не пересекаются. Стоит заметить, что в общем случае, когда каждая метка может занимать множество различных позиций, мы получаем задачу general satisfiability, которая является NP-полной. Однако, если ограничиться только двумя возможными позициями, то полученная задача будет задачей 2-SAT.
* Расположение рёбер при рисовании графа. Аналогично предыдущему пункту, если ограничиться только двумя возможными способами провести ребро, то мы придём к 2-SAT.
* Составление расписания игр. Имеется в виду такая система, когда каждая команда должна сыграть с каждой по одному разу, а требуется распределить игры по типу домашняя-выездная, с некоторыми наложенными ограничениями.
== См. также ==
*[http://neerc.ifmo.ru/wiki/index.php?title=КНФ - КНФ]
*[http://neerc.ifmo.ru/wiki/index.php?title=Специальные_формы_КНФ - Специальные формы КНФ. КНФ в форме Крона (2-КНФ)]
*[http://neerc.ifmo.ru/wiki/index.php?title=Основные_определения_теории_графов#.D0.9E.D1.80.D0.B8.D0.B5.D0.BD.D1.82.D0.B8.D1.80.D0.BE.D0.B2.D0.B0.D0.BD.D0.BD.D1.8B.D0.B5_.D0.B3.D1.80.D0.B0.D1.84.D1.8B - Ориентированные графы]
*[http://neerc.ifmo.ru/wiki/index.php?title=3CNFSAT - NP-полнота задачи о выполнимости булевой формулы в форме 3-КНФ]
== Источники информации ==
*[http://e-maxx.ru/algo/2_sat MAXimal :: algo :: Задача 2-SAT (2-CNF) ]
