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