2-SAT

Ликбез. Конъюнкция — это «правильный» термин для логического «И» (обозначается $\wedge$ или &). Конъюнкция возвращает true тогда и только тогда, когда обе переменные true.

Ликбез. Дизъюнкция — это «правильный» термин для логического «ИЛИ» (обозначается $\vee$ или |). Дизъюнкция возвращает false тогда и только тогда, когда обе переменные false.

Рассмотрим конъюнкцию дизъюнктов, то есть «И» от «ИЛИ» от каких-то переменных или их отрицаний. Например, такое выражение:

(a | b) & (!c | d) & (!a | !b)

Если буквами: (А ИЛИ B) И (НЕ C ИЛИ D) И (НЕ A ИЛИ НЕ B).

Можно показать, что любую логическую формулу можно представить в таком виде.

Задача satisfiability (SAT) заключается в том, чтобы найти такие значения переменных, при которых выражение становится истинным, или сказать, что такого набора значений нет. Для примера выше такими значениями являются a=1, b=0, c=0, d=1 (убедитесь, что каждая скобка стала true).

В случае произвольных формул эта задача быстро не решается. Мы же хотим решить её частный случай — когда у нас в каждой скобке ровно две переменные (2-SAT).

#Графы импликаций

Казалось бы — причем тут графы? Заметим, что выражение $a | b$ эквивалентно $(!a \rightarrow b) | (!b \rightarrow a)$. Здесь «$\rightarrow$» означает импликацию («если $a$ верно, то $b$ тоже верно»). С помощью этой подстановки приведем выражение к другому виду — импликативному.

Затем построим граф импликаций: для каждой переменной в графе будет по две вершины, (обозначим их через $x$ и $!x$), а рёбра в этом графе будут соответствовать импликациям.

Графы импликаций полезны тем, что если положить какое-либо выражение как верное, то нужно также положить верными и все выражения, которые следуют из него, то есть достижимые в графе импликаций.

Заметим, что если для какой-то переменной $x$ выполняется, что из $x$ достижимо $!x$, а из $!x$ достижимо $x$, то задача решения не имеет. Действительно: какое бы значение для переменной $x$ мы бы ни выбрали, мы всегда придём к противоречию — что должно быть выбрано и обратное ему значение.

Переформулируем данный критерий в терминах теории графов. Если из одной вершины достижима вторая и наоборот, то эти две вершины находятся в одной компоненте сильной связности. Тогда условие существования решения звучит так: для того, чтобы задача 2-SAT имела решение, необходимо, чтобы для любой переменной $x$ вершины $x$ и $!x$ находились в разных компонентах сильной связности графа импликаций.

Оказывается, что это условие является не только необходимым, но и достаточным. Доказательством этого факта служит описанный ниже алгоритм.

#Алгоритм решения 2-SAT

Пусть решение существует, и нам надо его найти. Заметим, что для некоторых переменных может выполняться, что из $x$ достижимо $!x$ или из $!x$ достижимо $x$ (но не одновременно). В таком случае выбор одного из значений переменной $x$ будет приводить к противоречию, в то время как выбор другого — не будет. Чтобы выбирать из двух значений то, которое не приводит к возникновению противоречий, можно воспользоваться следующим простым правилом.

Правило. Пусть $с[x]$ обозначает номер компоненты сильной связности, которой принадлежит вершина $x$, причём номера упорядочены в порядке топологической сортировки компонент сильной связности: если есть путь из $x$ в $y$, то $c[x] \leq c[y]$. Тогда, если $c[x] > c[!x]$, то выбираем значение $x$, иначе выбираем $!x$.

Докажем, что при таком выборе значений мы не придём к противоречию. Пусть, для определённости, $c[x] > c[!x]$, и поэтому была выбрана вершина $x$ (для случая $!x$ доказательство аналогичное).

• Покажем, что из $x$ не достижимо $!x$. Так как номер компоненты сильной связности $c[ x ]$ больше номера компоненты $c[ !x ]$, то компонента связности $x$ расположена «левее» компоненты связности $!x$, и из первой никак не может быть достижима последняя.
• Покажем, что из любой вершины $y$, достижимой из $x$, недостижимо $!y$. Докажем от противного: пусть из $x$ достижимо $y$, а из $y$ достижимо $!y$. Так как мы получали граф импликаций преобразованием $(a | b) \leftrightarrow ((!a \rightarrow b) | (!b \rightarrow a))$, и из $x$ достижимо $y$, то из $!y$ будет достижимо $!x$. Но, по предположению, из $y$ достижимо $!y$. Тогда мы получаем, что из $x$ достижимо $!x$, что противоречит условию.

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

Итак, мы построили алгоритм, который находит искомые значения переменных в предположении, что для любой переменной $x$ вершины $x$ и $!x$ находятся в разных компонентах сильной связности:

0. Построим граф импликаций, заменив все выражения вида $a | b$ двумя ребрами $!a \rightarrow b$ и $!b \rightarrow a$.
1. Найдем все компоненты сильной связности в графе импликаций.
2. Проверим, что для любого значения $x$ его отрицание лежит в другой компоненте сильной связности: $c[ x ] \neq c[ !x ]$. Если это не так, то решения не существует.
3. Если требуется выводить ответ, то положим условие $x$ верным, если $c[ x ] < c[ !x ]$, и неверным в противном случае.