Изменения

Перейти к: навигация, поиск

2SAT

1179 байт добавлено, 20:53, 3 декабря 2015
Добавлен алгоритм. Заменено "Определение" на "Задачу"
Рассмотрим функцию, записанную в виде 2-КНФ (КНФ Крома).
Решим задачу 2-SAT выполнимости данной функции.{{ОпределениеЗадача|definition =2-SAT выполнимость данной функции — эта задача распределения аргументов таким образом, чтобы результат данной функции был равен <tex> 1</tex>.
}}
 
== Алгоритм Решения ==
Рассмотрим любой дизъюнкт функции: <tex> a \vee b </tex> <br>.Несложно заметить, что это равнозначно записи <tex>(\overline a \to b \wedge b \to \overline a) </tex> <br>.
Построим ориентированный граф, где вершинами будут аргументы и их отрицание, а ребрами будут ребра вида: <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 \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 x </tex> было верным), <tex> x </tex> должен быть равен 0. Отсюда следует противоречие. <br> <br>
*Пусть для любой переменной <tex> x </tex> из вершины <tex> x </tex> нельзя достичь <tex> \overline x </tex> и из вершины <tex> \overline x </tex> нельзя достичь <tex> x </tex> одновременно. <br>Докажем, что этого достаточно, чтобы 2-SAT имело решение. <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>O(N + 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>. Если это условие не выполняется, то вернуть "решение не существует".
*Если <tex>comp[x] > comp[\overline x]</tex>, то переменной x выбираем значение true, иначе - false.
== Применение 2-SAT задач ==
*[[Основные_определения_теории_графов#.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 | Ориентированные графы]]
*[[3CNFSAT | NP-полнота задачи о выполнимости булевой формулы в форме 3-КНФ]]
*[http://e-maxx.ru/algo/strong_connected_components MAXimal :: algo :: Поиск компонент сильной связности за O(N + M)]
== Источники информации ==
24
правки

Навигация