2SAT — различия между версиями

Материал из Викиконспекты
Перейти к: навигация, поиск
(Применение 2-SAT задач: Добавлен пример применения 2-SAT)
(Временно убран пример. Исправлено вступление, алгоритм решения)
Строка 1: Строка 1:
Рассмотрим функцию, записанную в виде 2-КНФ (КНФ Крома).
 
 
Решим задачу 2-SAT выполнимости данной функции.
 
 
{{Задача
 
{{Задача
|definition = 2-SAT (2-satisfiability) выполнимость данной функции — задача распределения аргументов таким образом, чтобы результат данной функции был равен <tex> 1 </tex>.
+
|definition = <b>2-SAT </b> (2-satisfiability) выполнимость функции — задача распределения аргументов в булевой [[КНФ|КНФ]] функции, записанной в виде [[Специальные_формы_КНФ|2-КНФ (КНФ Крома)]], таким образом, чтобы результат данной функции был равен <tex> 1 </tex>.
 
}}
 
}}
  
== Алгоритм Решения ==
+
== Алгоритм решения ==
  
  
Строка 12: Строка 9:
 
Несложно заметить, что это равнозначно записи <tex>(\overline a \to b \wedge b \to \overline a) </tex>.
 
Несложно заметить, что это равнозначно записи <tex>(\overline a \to b \wedge b \to \overline a) </tex>.
  
Построим ориентированный граф, где вершинами будут аргументы и их отрицание, а ребрами будут ребра вида: <tex>\overline a \to b </tex> и <tex> b \to \overline a </tex> для каждого дизъюнкта функции <tex> a \vee b </tex>.
+
Построим [[Основные_определения_теории_графов|ориентированный граф]], где вершинами будут аргументы и их отрицание, а ребрами будут ребра вида: <tex>\overline a \to b </tex> и <tex> b \to \overline a </tex> для каждого дизъюнкта функции <tex> a \vee b </tex>.
  
 
{{Теорема
 
{{Теорема
Строка 18: Строка 15:
 
Для того, чтобы данная задача 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>.
 
Для того, чтобы данная задача 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=
 
|proof=
*Докажем достаточность: Пусть 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>. Тогда чтобы из <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. Отсюда следует противоречие.
+
<tex>(\Rightarrow)</tex>Докажем достаточность: Пусть 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>. Тогда чтобы из <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. Отсюда следует противоречие.
  
*Докажем необходимость: Пусть для любой переменной <tex> x </tex> из вершины <tex> x </tex> нельзя достичь <tex> \overline x </tex> и из вершины <tex> \overline x </tex> нельзя достичь <tex> x </tex> одновременно. Докажем, что этого достаточно, чтобы 2-SAT имело решение. Пусть из <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>. Противоречие.
+
<tex>(\Leftarrow)</tex>Докажем необходимость: Пусть для любой переменной <tex> x </tex> из вершины <tex> x </tex> нельзя достичь <tex> \overline x </tex> и из вершины <tex> \overline x </tex> нельзя достичь <tex> x </tex> одновременно. Докажем, что этого достаточно, чтобы 2-SAT имело решение. Пусть из <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>. Противоречие.
 
}}
 
}}
  
 
Теперь мы можем собрать весь алгоритм воедино:
 
Теперь мы можем собрать весь алгоритм воедино:
  
*Построим граф импликаций.
+
#Построим граф импликаций.  
*Найдём в этом графе компоненты сильной связности за время <tex>O(N + M)</tex>, пусть <tex>comp[v]</tex> — это номер компоненты сильной связности, которой принадлежит вершина <tex>v</tex>.
+
#[http://e-maxx.ru/algo/strong_connected_components Найдём в этом графе компоненты сильной связности за время <tex>O(N + M)</tex>]
*Проверим, что для каждой переменной <tex>x</tex> вершины <tex>x</tex> и <tex>\overline x</tex> лежат в разных компонентах, т.е. <tex>comp[x] \ne comp[\overline x]</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.
+
#Если <tex>comp[x] > comp[\overline x]</tex>, то переменной x выбираем значение true, иначе - false.
 
 
== Применение 2-SAT задач ==
 
 
 
Предположим, что семь комиков согласились во время трехдневного фестиваля дать концерты в двух из пяти отелей. При этом у каждого из них один из дней занят другой работой, поэтому вот как выглядят возможные варианты их выступлений в отелях Лас-Вегаса:
 
 
 
*Tomlin может выступить в отелях Aladdin и Caesars в дни 1 и 2;
 
*Unwin может выступить в отелях Bellagio и Excalibur в дни 1 и 2;
 
*Vegas может выступить в отелях Desert и Excalibur в дни 2 и 3;
 
*Williams может выступить в отелях Aladdin и Desert в дни 1 и 3;
 
*Xie может выступить в отелях Caesars и Excalibur в дни 1 и 3;
 
*Yankovic может выступить в отелях Bellagio и Desert в дни 2 и 3;
 
*Zany может выступить в отелях Bellagio и Caesars в дни 1 и 2.
 
 
 
Можно ли составить расписание так, чтобы не возникало никаких конфликтов?
 
Для решения этой задачи можно ввести семь булевых переменных <tex>{t, u, v, w, x, у, z}, </tex> где <tex>t</tex> например, означает выступление Tomlin в Aladdin в первый день и в Caesars во второй, в то время как <tex> \overline t </tex> означает, что дни соответствуют отелям в обратном порядке: выступление в Aladdin — во второй день, а в Caesars — в первый. Тогда мы можем записать ограничения, означающие, что никакие два комедианта не выступают в одном отеле в один и тот же день, следующим образом.
 
 
 
Тогда мы можем записать ограничения, означающие, что никакие два комедианта не выступают в одном отеле в один и тот же день, следующим образом. (В квадратных скобках указаны первая буква отеля и день, в который двое участников не могут выступать одновременно).
 
 
 
{| class="wikitable" style="width:10cm" border=1
 
|<tex>\overline {(t \wedge w)} {[}A1{]} </tex>
 
||<tex>\overline {(y \wedge \overline z)} {[}B2{]} </tex>
 
||<tex>\overline {(t \wedge z)} {[}C2{]} </tex>
 
||<tex>\overline {(w \wedge y)} {[}D3{]} </tex>
 
|-
 
|<tex>\overline {(u \wedge z)} {[}B1{]} </tex>
 
||<tex>\overline {(\overline t \wedge x)} {[}C1{]} </tex>
 
||<tex>\overline {(v \wedge \overline y)} {[}D2{]} </tex>
 
||<tex>\overline {(\overline u \wedge \overline x)} {[}E1{]} </tex>
 
|-
 
|<tex>\overline {(\overline u \wedge y)} [B2] </tex>
 
||<tex>\overline {(\overline t \wedge \overline z)} [C1] </tex>
 
||<tex>\overline {(\overline v \wedge w)} [D3] </tex>
 
||<tex>\overline {(u \wedge \overline v)} [E2] </tex>
 
|-
 
|<tex>\overline {(\overline u \wedge \overline z)} [B2] </tex>
 
||<tex>\overline {(x \wedge \overline z)} [C1] </tex>
 
||<tex>\overline {(\overline v \wedge y)} [D3] </tex>
 
||<tex>\overline {(v \wedge x)} [E3] </tex>
 
|}
 
 
 
Каждое из этих ограничений, конечно же, представляет собой дизъюнкт Крома, которые мы должны выполнить
 
 
 
<tex>
 
(\overline t \vee \overline w)
 
\wedge (\overline u \vee \overline z)
 
\wedge (u \vee \overline y)
 
\wedge (u \vee z)
 
\wedge (\overline y \vee z)
 
\wedge (t \vee \overline x)
 
\wedge (t \vee z)
 
\wedge (\overline x \vee z)
 
\wedge
 
</tex>
 
 
 
<tex>
 
(\overline t \vee \overline z)
 
\wedge (\overline v \vee y)
 
\wedge (v \vee \overline w)
 
\wedge (v \vee \overline y)
 
\wedge (\overline w \vee \overline y)
 
\wedge (u \vee x)
 
\wedge (\overline u \vee v)
 
\wedge (\overline v \vee \overline x)
 
</tex>
 
 
 
Кроме того, дизъюнкты Крома могут быть записаны в виде импликаций:
 
 
 
<tex>
 
(t \to \overline w)
 
\wedge (u \to \overline z)
 
\wedge (\overline u \to \overline y)
 
\wedge (\overline u \to z)
 
\wedge (y \to z)
 
\wedge (\overline t \to \overline x)
 
\wedge (\overline t \to z)
 
\wedge (x \to z)
 
\wedge
 
</tex>
 
 
 
<tex>
 
(t \to \overline z)
 
\wedge (v \to y)
 
\wedge (\overline v \to \overline w)
 
\wedge (\overline v \to \overline y)
 
\wedge (w \to \overline y)
 
\wedge (\overline u \to x)
 
\wedge (u \to v)
 
\wedge (v \to \overline x)
 
</tex>
 
 
 
И каждая такая импликация может также быть представлена в альтернативном, "контрапозитивном" виде:
 
 
 
<tex>
 
(w \to \overline t)
 
\wedge (z \to \overline u)
 
\wedge (\overline y \to \overline u)
 
\wedge (\overline z \to u)
 
\wedge (z \to y)
 
\wedge (\overline x \to \overline t)
 
\wedge (\overline z \to t)
 
\wedge (z \to x)
 
\wedge
 
</tex>
 
<tex>
 
(z \to \overline t)
 
\wedge (y \to v)
 
\wedge (\overline w \to \overline v)
 
\wedge (\overline y \to \overline v)
 
\wedge (y \to \overline w)
 
\wedge (\overline u \to x)
 
\wedge (v \to u)
 
\wedge (x \to \overline v)
 
</tex>
 
 
 
При решение данной задачи можно найти следующий цикл:
 
 
 
<tex>
 
u
 
\to \overline z
 
\to \overline y
 
\to \overline v
 
\to \overline u
 
\to z
 
\to \overline t
 
\to \overline x
 
\to \overline u
 
</tex>
 
 
 
Этот цикл говорит о том, что <tex> v </tex> и <tex> \overline v </tex> должны иметь одно и то же значение; так что нет никакой возможности удовлетворить все условия. Если расписание должно быть составлено любой ценой, организаторам фестиваля придется провести переговоры и пересмотреть соглашение по крайней мере с одним из семи комедиантов.
 
  
Организаторы могут, например, попытаться временно вывести за рамки картины <tex> v </tex>. Тогда пять из шестнадцати ограничений исчезнут, и останутся только 22 из импликаций.
+
Компоненты сильной связности найдем за <tex>O(N + M)</tex>, затем проверим каждую из <tex>N</tex> переменных за <tex>O(N)</tex>. Следовательно асимптотика <tex>O(N + M)</tex>
Такое решение будет иметь циклы наподобие <tex> z \to \overline u \to x \to z </tex> или <tex> t \to \overline z \to t </tex>.  
 
Можно заметить что значение <tex> tuwxyz = 110000 </tex> выполняют каждый дизъюнкт. Эти значения дают нам расписание, которое выполняет шесть из семи исходных условий, начиная с выступления (Tomlin, Unwin, Zany, Williams, Xie) в первый день в (Aladdin, Bellagio, Caesars, Desert, Excalibur).
 
  
 
== См. также ==
 
== См. также ==
  
*[[КНФ | КНФ]]
 
*[[Специальные_формы_КНФ | Специальные формы КНФ. КНФ в форме Крона (2-КНФ)]]
 
*[[Основные_определения_теории_графов#.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-КНФ]]
 
*[[3CNFSAT | NP-полнота задачи о выполнимости булевой формулы в форме 3-КНФ]]
*[http://e-maxx.ru/algo/strong_connected_components MAXimal :: algo :: Поиск компонент сильной связности за O(N + M)]
 
  
 
== Источники информации ==
 
== Источники информации ==
  
 
*[http://e-maxx.ru/algo/2_sat MAXimal :: algo :: Задача 2-SAT (2-CNF) ]
 
*[http://e-maxx.ru/algo/2_sat MAXimal :: algo :: Задача 2-SAT (2-CNF) ]
*[https://en.wikipedia.org/wiki/2-satisfiability 2-satisfiability - Википедия]
+
*[https://en.wikipedia.org/wiki/2-satisfiability 2-satisfiability Википедия]
  
 
[[Категория: Дискретная математика и алгоритмы]]
 
[[Категория: Дискретная математика и алгоритмы]]
  
 
[[Категория: Булевы функции ]]
 
[[Категория: Булевы функции ]]

Версия 13:33, 10 декабря 2015

Задача:
2-SAT (2-satisfiability) выполнимость функции — задача распределения аргументов в булевой КНФ функции, записанной в виде 2-КНФ (КНФ Крома), таким образом, чтобы результат данной функции был равен [math] 1 [/math].


Алгоритм решения

Рассмотрим любой дизъюнкт функции: [math] a \vee b [/math]. Несложно заметить, что это равнозначно записи [math](\overline a \to b \wedge b \to \overline a) [/math].

Построим ориентированный граф, где вершинами будут аргументы и их отрицание, а ребрами будут ребра вида: [math]\overline a \to b [/math] и [math] b \to \overline a [/math] для каждого дизъюнкта функции [math] a \vee b [/math].

Теорема:
Для того, чтобы данная задача 2-SAT имела решение, необходимо и достаточно, чтобы для любой переменной [math] x [/math] из вершины [math] x [/math] нельзя достичь [math] \overline x [/math] и из вершины [math] \overline x [/math] нельзя достичь [math] x [/math] одновременно. [math](\overline x \to x \wedge x \to \overline x) [/math].
Доказательство:
[math]\triangleright[/math]

[math](\Rightarrow)[/math]Докажем достаточность: Пусть 2-SAT имеет решение. Докажем, что не может быть такого, чтобы для любой переменной [math] x [/math] из вершины [math] x [/math] можно достичь [math] \overline x [/math] и из вершины [math] \overline x [/math] можно достичь [math] x [/math] одновременно. [math](\overline x \to x \wedge x \to \overline x) [/math]. Тогда чтобы из [math] \overline x [/math] достичь [math] x [/math] [math] (\overline x \to x [/math] было верным), [math] x [/math] должен быть равен [math] 1 [/math]. С другой стороны для того, чтобы из [math] x [/math] достичь [math] \overline x [/math] [math] (\overline x \to x [/math] было верным), [math] x [/math] должен быть равен 0. Отсюда следует противоречие.

[math](\Leftarrow)[/math]Докажем необходимость: Пусть для любой переменной [math] x [/math] из вершины [math] x [/math] нельзя достичь [math] \overline x [/math] и из вершины [math] \overline x [/math] нельзя достичь [math] x [/math] одновременно. Докажем, что этого достаточно, чтобы 2-SAT имело решение. Пусть из [math] \overline x [/math] можно достичь [math] x [/math], но из вершины [math] x [/math] нельзя достичь [math] \overline x [/math]. Докажем, что из [math] x [/math] не достижимо такой [math] y [/math], что из [math] y [/math] достижимо [math] \overline y [/math]. (т.е. [math] x \to y \to \overline y (x = 1, y = 0)) [/math]. Если из [math] x \to y [/math], то [math] \overline x \vee y [/math], отсюда следует [math] \overline y \to \overline x [/math]. Тогда [math] x \to y \to \overline y \to \overline x [/math]. Следовательно [math] x \to \overline x [/math]. Противоречие.
[math]\triangleleft[/math]

Теперь мы можем собрать весь алгоритм воедино:

  1. Построим граф импликаций.
  2. Найдём в этом графе компоненты сильной связности за время [math]O(N + M)[/math]
  3. Пусть [math]comp[v][/math] — это номер компоненты сильной связности, которой принадлежит вершине [math]v[/math]. Проверим, что для каждой переменной [math]x[/math] вершины [math]x[/math] и [math]\overline x[/math] лежат в разных компонентах, т.е. [math]comp[x] \ne comp[\overline x][/math]. Если это условие не выполняется, то вернуть "решение не существует".
  4. Если [math]comp[x] \gt comp[\overline x][/math], то переменной x выбираем значение true, иначе - false.

Компоненты сильной связности найдем за [math]O(N + M)[/math], затем проверим каждую из [math]N[/math] переменных за [math]O(N)[/math]. Следовательно асимптотика [math]O(N + M)[/math]

См. также

Источники информации