2SAT

Рассмотрим функцию, записанную в виде 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).

См. также

• КНФ
• Специальные формы КНФ. КНФ в форме Крона (2-КНФ)
• Ориентированные графы
• NP-полнота задачи о выполнимости булевой формулы в форме 3-КНФ
• MAXimal :: algo :: Поиск компонент сильной связности за O(N + M)

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

• MAXimal :: algo :: Задача 2-SAT (2-CNF)
• 2-satisfiability - Википедия