2-SAT

Материал из Algocode wiki
Версия от 18:53, 26 сентября 2020; Tyoma (обсуждение | вклад) (была смысловая опечатка)
Перейти к: навигация, поиск

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

Ликбез. Дизъюнкция — это «правильный» термин для логического «ИЛИ» (обозначается \(\wedge\) или |). Дизъюнкция возвращает 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\)), а рёбра в этом графе будут соответствовать импликациям.

Https---upload.wikimedia.org-wikipedia-commons-thumb-2-2f-Implication graph.svg-1920px-Implication graph.svg.png

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

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

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

Пусть решение существует, и нам надо его найти. Заметим, что, несмотря на то, что решение существует, для некоторых переменных может выполняться, что из \(x\) достижимо \(!x\) или из \(!x\) достижимо \(x\) (но не одновременно). В таком случае выбор одного из значений переменной \(x\) будет приводить к противоречию, в то время как выбор другого — не будет. Научимся выбирать из двух значений то, которое не приводит к возникновению противоречий. Сразу заметим, что, выбрав какое-либо значение, мы должны запустить из него обход в глубину/ширину и пометить все значения, которые следуют из него, т.е. достижимы в графе импликаций. Соответственно, для уже помеченных вершин никакого выбора между \(x\) и \(!x\) делать не нужно, для них значение уже выбрано и зафиксировано. Нижеописанное правило применяется только к непомеченным ещё вершинам.

Утверждается следующее. Пусть \(\space{\rm comp}[V]\) обозначает номер компоненты сильной связности, которой принадлежит вершина \(V\), причём номера упорядочены в порядке топологической сортировки компонент сильной связности в графе компонентов (т.е. более ранним в порядке топологической сортировки соответствуют большие номера: если есть путь из \(v\) в \(w\), то \(\space{\rm comp}[v] \leq \space{\rm comp}[w]\)). Тогда, если \(\space{\rm comp}[x] < \space{\rm comp}[!x]\), то выбираем значение !x, иначе выбираем x.

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

Во-первых, докажем, что из \(x\) не достижимо \(!x\). Действительно, так как номер компоненты сильной связности \(\space{\rm comp}[x]\) больше номера компоненты \(\space{\rm comp}[!x]\) , то это означает, что компонента связности, содержащая \(x\), расположена левее компоненты связности, содержащей \(!x\), и из первой никак не может быть достижима последняя.

Во-вторых, докажем, что из любой вершины \(y\), достижимой из \(x\) недостижима \(!y\). Докажем это от противного. Пусть из \(x\) достижимо \(y\), а из \(y\) достижимо \(!y\). Так как из \(x\) достижимо \(y\), то, по свойству графа импликаций, из \(!y\) будет достижимо \(!x\). Но, по предположению, из \(y\) достижимо \(!y\). Тогда мы получаем, что из \(x\) достижимо \(!x\), что противоречит условию, что и требовалось доказать.

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