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

Материал из Викиконспекты
Перейти к: навигация, поиск
м (Алгоритм Решения)
(Применение 2-SAT задач: Добавлен пример применения 2-SAT)
Строка 32: Строка 32:
 
== Применение 2-SAT задач ==
 
== Применение 2-SAT задач ==
  
Алгоритм для решения 2-SAT может быть применим во всех задачах, где есть набор величин, каждая из которых может принимать 2 возможных значения, и есть связи между этими величинами:
+
Предположим, что семь комиков согласились во время трехдневного фестиваля дать концерты в двух из пяти отелей. При этом у каждого из них один из дней занят другой работой, поэтому вот как выглядят возможные варианты их выступлений в отелях Лас-Вегаса:  
  
* Расположение текстовых меток на карте или диаграмме. Имеется в виду нахождение такого расположения меток, при котором никакие две не пересекаются. Стоит заметить, что в общем случае, когда каждая метка может занимать множество различных позиций, мы получаем задачу general satisfiability, которая является NP-полной. Однако, если ограничиться только двумя возможными позициями, то полученная задача будет задачей 2-SAT.
+
*Tomlin может выступить в отелях Aladdin и Caesars в дни 1 и 2;
* Расположение рёбер при рисовании графа. Аналогично предыдущему пункту, если ограничиться только двумя возможными способами провести ребро, то мы придём к 2-SAT.
+
*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> 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).
  
 
== См. также ==
 
== См. также ==

Версия 18:39, 9 декабря 2015

Рассмотрим функцию, записанную в виде 2-КНФ (КНФ Крома).

Решим задачу 2-SAT выполнимости данной функции.

Задача:
2-SAT (2-satisfiability) выполнимость данной функции — задача распределения аргументов таким образом, чтобы результат данной функции был равен [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]
  • Докажем достаточность: Пусть 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] 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]

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

  • Построим граф импликаций.
  • Найдём в этом графе компоненты сильной связности за время [math]O(N + M)[/math], пусть [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]. Если это условие не выполняется, то вернуть "решение не существует".
  • Если [math]comp[x] \gt comp[\overline x][/math], то переменной 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.

Можно ли составить расписание так, чтобы не возникало никаких конфликтов? Для решения этой задачи можно ввести семь булевых переменных [math]{t, u, v, w, x, у, z}, [/math] где [math]t[/math] например, означает выступление Tomlin в Aladdin в первый день и в Caesars во второй, в то время как [math] \overline t [/math] означает, что дни соответствуют отелям в обратном порядке: выступление в Aladdin — во второй день, а в Caesars — в первый. Тогда мы можем записать ограничения, означающие, что никакие два комедианта не выступают в одном отеле в один и тот же день, следующим образом.

Тогда мы можем записать ограничения, означающие, что никакие два комедианта не выступают в одном отеле в один и тот же день, следующим образом. (В квадратных скобках указаны первая буква отеля и день, в который двое участников не могут выступать одновременно).

[math]\overline {(t \wedge w)} {[}A1{]} [/math] [math]\overline {(y \wedge \overline z)} {[}B2{]} [/math] [math]\overline {(t \wedge z)} {[}C2{]} [/math] [math]\overline {(w \wedge y)} {[}D3{]} [/math]
[math]\overline {(u \wedge z)} {[}B1{]} [/math] [math]\overline {(\overline t \wedge x)} {[}C1{]} [/math] [math]\overline {(v \wedge \overline y)} {[}D2{]} [/math] [math]\overline {(\overline u \wedge \overline x)} {[}E1{]} [/math]
[math]\overline {(\overline u \wedge y)} [B2] [/math] [math]\overline {(\overline t \wedge \overline z)} [C1] [/math] [math]\overline {(\overline v \wedge w)} [D3] [/math] [math]\overline {(u \wedge \overline v)} [E2] [/math]
[math]\overline {(\overline u \wedge \overline z)} [B2] [/math] [math]\overline {(x \wedge \overline z)} [C1] [/math] [math]\overline {(\overline v \wedge y)} [D3] [/math] [math]\overline {(v \wedge x)} [E3] [/math]

Каждое из этих ограничений, конечно же, представляет собой дизъюнкт Крома, которые мы должны выполнить

[math] (\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 [/math]

[math] (\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) [/math]

Кроме того, дизъюнкты Крома могут быть записаны в виде импликаций:

[math] (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 [/math]

[math] (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) [/math]

И каждая такая импликация может также быть представлена в альтернативном, "контрапозитивном" виде:

[math] (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 [/math] [math] (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) [/math]

При решение данной задачи можно найти следующий цикл:

[math] u \to \overline z \to \overline y \to \overline v \to \overline u \to z \to \overline t \to \overline x \to \overline u [/math]

Этот цикл говорит о том, что [math] v [/math] и [math] \overline v [/math] должны иметь одно и то же значение; так что нет никакой возможности удовлетворить все условия. Если расписание должно быть составлено любой ценой, организаторам фестиваля придется провести переговоры и пересмотреть соглашение по крайней мере с одним из семи комедиантов.

Организаторы могут, например, попытаться временно вывести за рамки картины [math] v [/math]. Тогда пять из шестнадцати ограничений исчезнут, и останутся только 22 из импликаций. Такое решение будет иметь циклы наподобие [math] z \to \overline u \to x \to z [/math] или [math] t \to \overline z \to t [/math]. Можно заметить что значение [math] tuwxyz = 110000 [/math] выполняют каждый дизъюнкт. Эти значения дают нам расписание, которое выполняет шесть из семи исходных условий, начиная с выступления (Tomlin, Unwin, Zany, Williams, Xie) в первый день в (Aladdin, Bellagio, Caesars, Desert, Excalibur).

См. также

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