2-SAT

Дано $n$ булевых переменных и $m$ условий, каждое из которых — дизъюнкция двух литералов: $(a \lor b)$, где литерал — это переменная или её отрицание. Требуется подобрать значения так, чтобы все условия стали истинными.

Общая задача выполнимости (SAT) NP-полна. Ограничение «ровно два литерала в скобке» меняет всё: 2-SAT решается за $O(n + m)$, и решается графом.

Импликации вместо дизъюнкций

Всё держится на одном тождестве:

$$(a \lor b) \equiv (\lnot a \Rightarrow b) \equiv (\lnot b \Rightarrow a).$$

Если $a$ ложно, то $b$ обязано быть истинным, и наоборот. Каждое условие даёт две импликации — обе нужны.

Построим граф импликаций: $2n$ вершин, по одной на каждый литерал $x_i$ и $\lnot x_i$; на каждое условие — два ребра. Получается ориентированный граф, в котором путь означает «из этого следует то».

Устроен он симметрично: вместе с ребром $u \to v$ в нём всегда есть ребро $\lnot v \to \lnot u$. Это свойство ещё пригодится.

Критерий выполнимости

Формула выполнима тогда и только тогда, когда ни для какой переменной литералы $x_i$ и $\lnot x_i$ не лежат в одной компоненте сильной связности.

В одну сторону просто. Одна компонента означает, что есть путь $x_i \to \lnot x_i$ и путь $\lnot x_i \to x_i$, то есть из истинности $x_i$ следует её ложность и наоборот. Любое значение приводит к противоречию.

В другую сторону — построением, которое ниже. Проверено перебором: на 200 000 случайных формул до пяти переменных и восьми условий критерий ни разу не разошёлся с полным перебором наборов значений.

Как получить сам набор значений

Пронумеруем компоненты в топологическом порядке конденсации — например, алгоритм Косарайю выдаёт такую нумерацию сам, если брать вершины в порядке убывания времени выхода первого обхода. Тогда:

$$x_i = \text{истина} \iff \mathrm{comp}[x_i] > \mathrm{comp}[\lnot x_i],$$

то есть переменная истинна, если компонента её положительного литерала идёт в топологическом порядке позже.

Почему это работает. Импликация — это ребро, а ребро в конденсации всегда ведёт от меньшего номера к большему. Если бы истинный литерал шёл раньше ложного, из истины следовала бы ложь — противоречие. Симметрия графа гарантирует, что выбор согласован сразу для всех переменных.

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

auto node = [](int i, int value) { return 2 * i + value; };   // литерал x_i = value

for (auto [i1, e1, i2, e2] : clauses) {
    g[node(i1, 1 - e1)].push_back(node(i2, e2));
    g[node(i2, 1 - e2)].push_back(node(i1, e1));
}
kosaraju();                                    // заполняет comp[]
for (int i = 0; i < n; i++)
    if (comp[node(i, 0)] == comp[node(i, 1)]) return "невыполнимо";
for (int i = 0; i < n; i++)
    value[i] = comp[node(i, 1)] > comp[node(i, 0)];

Обратите внимание, что критерий и построение — это один и тот же проход. Отдельного «а теперь найдём ответ» не требуется.

Что сводится к 2-SAT

Сама формула в условии встречается редко. Гораздо чаще задача выглядит иначе, и главное — заметить, что каждое ограничение касается не более двух объектов и каждый объект имеет ровно два состояния.

формулировка	условие 2-SAT
«хотя бы один из двух»	$(a \lor b)$
«не оба сразу»	$(\lnot a \lor \lnot b)$
«если $a$, то $b$»	$(\lnot a \lor b)$
«$a$ и $b$ равны»	$(\lnot a \lor b)$ и $(a \lor \lnot b)$
«$a$ обязана быть истинной»	$(a \lor a)$

Последняя строчка — обычный приём закрепления переменной: дизъюнкция литерала с самим собой не оставляет выбора. В графе она превращается в ребро $\lnot a \to a$.

Типичные задачи: расставить $n$ объектов, у каждого два возможных положения, при запрете некоторых пар; раскрасить в два цвета с ограничениями посложнее двудольности; выбрать по одному из двух вариантов в каждой паре так, чтобы выбранные не конфликтовали.

Где ошибаются

Добавляют одну импликацию вместо двух. Условие $(a \lor b)$ даёт и $\lnot a \Rightarrow b$, и $\lnot b \Rightarrow a$. С одной из них граф теряет симметрию, и критерий перестаёт работать.

Берут значение по неправильной стороне. Правило «позже — истина» верно для топологической нумерации, где меньший номер ближе к истоку. Алгоритм Тарьяна нумерует компоненты в обратном топологическом порядке, и с ним знак сравнения противоположный. Это самая частая причина решения, которое верно отвечает «выполнимо», но выдаёт негодный набор.

Забывают, что $2n$ вершин, а не $n$. Массивы под компоненты, посещённость и списки смежности должны быть вдвое длиннее, чем переменных.

Смежное

• Компоненты сильной связности — то, на чём всё держится;
• Двудольность и раскраска в два цвета — частный случай, решаемый проще;
• Топологическая сортировка — откуда берётся порядок компонент.