17.2 Задача 2SAT¶

Что такое 2SAT¶

Задача 2SAT — это специальный вариант задачи выполнимости булевых формул. Нам дана формула вида

( a1 ∨ b1 ) ∧ ( a2 ∨ b2 ) ∧ ... ∧ ( am ∨ bm )

Здесь каждый литерал ai и bi — это либо переменная x, либо её отрицание ¬x.

Нужно определить, можно ли присвоить каждой переменной значение true или false так, чтобы вся формула стала истинной.

Это важная задача, потому что она часто возникает в олимпиадных постановках:

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

Главная особенность 2SAT в том, что, в отличие от общей SAT-задачи, её можно решать эффективно.

Интуиция на простом примере¶

Рассмотрим формулу:

( x1 ∨ x2 ) ∧ ( ¬x1 ∨ x3 ) ∧ ( ¬x2 ∨ ¬x3 )

Что означает каждая скобка?

(x1 ∨ x2) означает: хотя бы одно из x1, x2 должно быть истинно;
(¬x1 ∨ x3) означает: если x1 = true, то тогда x3 тоже должно быть true;
(¬x2 ∨ ¬x3) означает: нельзя одновременно сделать x2 = true и x3 = true.

Если попробовать подобрать значения вручную, можно найти, например:

x1 = true
x2 = false
x3 = true

Тогда формула истинна.

Но ручной перебор работает только для очень маленьких примеров. Если переменных много, нужен структурный способ решения.

Ключевая идея: граф импликаций¶

2SAT удобно переводится в ориентированный граф.

Вершины графа¶

Для каждой переменной x создаются две вершины:

x
¬x

То есть для n переменных будет 2n вершин.

Рёбра графа¶

Каждую скобку

( a ∨ b )

можно переписать в виде двух импликаций:

¬a → b
¬b → a

Почему это верно?

Потому что если a ложно, то чтобы дизъюнкция (a ∨ b) была истинной, обязано быть истинным b. Аналогично, если b ложно, то обязано быть истинным a.

Это и есть основа всего алгоритма.

Как построить импликации¶

Рассмотрим несколько типичных скобок.

1. Скобка `(x ∨ y)`¶

Она даёт рёбра:

¬x → y
¬y → x

2. Скобка `(x ∨ ¬y)`¶

Она даёт рёбра:

¬x → ¬y
y → x

3. Скобка `(¬x ∨ ¬y)`¶

Она даёт рёбра:

x → ¬y
y → ¬x

4. Скобка `(x ∨ x)`¶

Она эквивалентна условию x = true.

Рёбра будут:

¬x → x
¬x → x

То есть фактически одно условие: если ¬x истинно, то x тоже истинно, а это возможно только когда выбирается x = true.

5. Скобка `(¬x ∨ ¬x)`¶

Она эквивалентна условию x = false.

Рёбра:

x → ¬x
x → ¬x

Почему здесь появляются компоненты сильной связности¶

После построения графа возникает вопрос: как понять, существует ли корректное присваивание?

Ответ связан с компонентами сильной связности.

Напоминание¶

Компонента сильной связности — это группа вершин, в которой из любой вершины можно добраться до любой другой.

Если в одном и том же компоненте сильной связности одновременно находятся вершины:

x
¬x

то решения не существует.

Почему?¶

Потому что тогда:

есть путь x → ¬x, значит из истинности x следует истинность ¬x;
есть путь ¬x → x, значит из истинности ¬x следует истинность x.

Получается, что x и ¬x оказываются жёстко связанными и должны иметь одинаковую истинность. Но это невозможно: переменная и её отрицание не могут быть одновременно истинны.

Отсюда важный критерий.

Критерий существования решения¶

Формула 2SAT выполнима тогда и только тогда, когда для любой переменной x вершины x и ¬x лежат в разных компонентах сильной связности.

Это основной тест.

Если хотя бы для одной переменной они попали в одну компоненту, ответ: NO.
Если для всех переменных они в разных компонентах, ответ: YES, и решение можно восстановить.

Именно эта идея описана в книге: задача сводится к поиску компонент сильной связности в графе импликаций fileciteturn1file0.

Пример выполнимой формулы¶

Возьмём формулу:

( x1 ∨ x2 ) ∧ ( ¬x1 ∨ x3 ) ∧ ( ¬x2 ∨ x3 ) ∧ ( ¬x3 ∨ x1 )

Построим импликации.

Из (x1 ∨ x2):

¬x1 → x2
¬x2 → x1

Из (¬x1 ∨ x3):

x1 → x3
¬x3 → ¬x1

Из (¬x2 ∨ x3):

x2 → x3
¬x3 → ¬x2

Из (¬x3 ∨ x1):

x3 → x1
¬x1 → ¬x3

Здесь нет переменной, для которой x и ¬x попадают в одну и ту же сильную компоненту. Значит решение существует.

Одно из возможных решений:

x1 = true
x2 = true
x3 = true

Пример невыполнимой формулы¶

Теперь рассмотрим формулу:

( x1 ∨ x1 ) ∧ ( ¬x1 ∨ ¬x1 )

Первая скобка заставляет x1 = true. Вторая скобка заставляет x1 = false.

Построим рёбра:

Из (x1 ∨ x1):

¬x1 → x1

Из (¬x1 ∨ ¬x1):

x1 → ¬x1

Теперь есть путь в обе стороны между x1 и ¬x1, значит они находятся в одной компоненте сильной связности. Следовательно, формула противоречива.

Как восстановить значения переменных¶

Проверить существование решения — это только половина задачи. Часто в олимпиадной задаче нужно ещё вывести одно подходящее присваивание.

После того как мы нашли компоненты сильной связности, мы сжимаем граф в DAG компонент.

Дальше используется важное правило:

если компонента переменной x расположена позже компоненты ¬x в топологическом порядке компонент, то обычно выбирают x = true;
иначе выбирают x = false.

На практике после алгоритма Косараджу или Тарьяна часто просто сравнивают номера компонент:

если comp[x] == comp[¬x], ответа нет;
иначе значение можно взять как comp[x] > comp[¬x] или наоборот — в зависимости от того, как нумеровались компоненты в реализации.

Важно не запомнить конкретный знак, а понимать идею:

мы назначаем истину той вершине, чья компонента стоит «выше по приоритету» в порядке обработки, чтобы не нарушать импликации.

Почему правило с порядком компонент корректно¶

Если из компоненты A есть путь в компоненту B, и мы сделали какую-то вершину из A истинной, то все вершины, до которых есть путь, тоже обязаны быть истинными.

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

Именно поэтому в книге предлагается идти по графу компонент в обратном топологическом порядке: так мы сначала принимаем решения в «конечных» компонентах, а затем распространяем последствия дальше fileciteturn1file0.

Удобная модель для олимпиадных задач¶

Обычно переменная означает выбор одного из двух состояний.

Например:

x = true — ученик идёт в группу A;
x = false — ученик идёт в группу B.

Тогда ограничения переводятся так:

«хотя бы один из u, v выбран» → (u ∨ v);
«не могут быть выбраны одновременно u и v» → (¬u ∨ ¬v);
«если выбран u, то должен быть выбран v» → (¬u ∨ v);
«ровно один из двух» → (u ∨ v) ∧ (¬u ∨ ¬v).

Это делает 2SAT очень полезным инструментом моделирования.

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

Для каждой переменной создать две вершины: x и ¬x.
Для каждой скобки (a ∨ b) добавить рёбра ¬a → b и ¬b → a.
Найти компоненты сильной связности.
Если x и ¬x лежат в одной компоненте хотя бы для одной переменной, вывести NO.
Иначе восстановить значения переменных по порядку компонент.

Сложность¶

Пусть:

n — число переменных;
m — число скобок.

Тогда:

вершин в графе: 2n;
рёбер: 2m.

Алгоритм поиска компонент сильной связности работает за линейное время:

O(n + m)

с точностью до констант, если считать по числу вершин и рёбер графа импликаций.

Это очень быстро и подходит для больших ограничений.

Реализация на C++¶

Ниже — удобная реализация 2SAT через алгоритм Косараджу.

#include <bits/stdc++.h>
using namespace std;

struct TwoSAT {
    int n;
    vector<vector<int>> g, gr;
    vector<int> used, order, comp, ans;

    TwoSAT(int n) : n(n) {
        g.assign(2 * n, {});
        gr.assign(2 * n, {});
    }

    int id(int v, bool val) {
        return 2 * v + (val ? 0 : 1);
    }

    int neg(int x) {
        return x ^ 1;
    }

    void add_edge(int a, int b) {
        g[a].push_back(b);
        gr[b].push_back(a);
    }

    void add_or(int v1, bool val1, int v2, bool val2) {
        int a = id(v1, val1);
        int b = id(v2, val2);
        add_edge(neg(a), b);
        add_edge(neg(b), a);
    }

    void add_true(int v, bool val) {
        add_or(v, val, v, val);
    }

    void dfs1(int v) {
        used[v] = 1;
        for (int to : g[v]) {
            if (!used[to]) dfs1(to);
        }
        order.push_back(v);
    }

    void dfs2(int v, int c) {
        comp[v] = c;
        for (int to : gr[v]) {
            if (comp[to] == -1) dfs2(to, c);
        }
    }

    bool solve() {
        used.assign(2 * n, 0);
        order.clear();

        for (int i = 0; i < 2 * n; i++) {
            if (!used[i]) dfs1(i);
        }

        comp.assign(2 * n, -1);
        int c = 0;
        for (int i = (int)order.size() - 1; i >= 0; i--) {
            int v = order[i];
            if (comp[v] == -1) dfs2(v, c++);
        }

        ans.assign(n, 0);
        for (int i = 0; i < n; i++) {
            if (comp[2 * i] == comp[2 * i + 1]) {
                return false;
            }
            ans[i] = (comp[2 * i] > comp[2 * i + 1]);
        }
        return true;
    }
};

int main() {
    int n = 3;
    TwoSAT sat(n);

    sat.add_or(0, true, 1, true);
    sat.add_or(0, false, 2, true);
    sat.add_or(1, false, 2, true);
    sat.add_or(2, false, 0, true);

    if (!sat.solve()) {
        cout << "NO\n";
    } else {
        cout << "YES\n";
        for (int i = 0; i < n; i++) {
            cout << "x" << i + 1 << " = " << (sat.ans[i] ? "true" : "false") << "\n";
        }
    }

    return 0;
}

Как пользоваться этой реализацией¶

Обозначения¶

Вызов

add_or(v1, val1, v2, val2)

добавляет скобку

( literal1 ∨ literal2 )

где:

v1, v2 — номера переменных от 0 до n-1;
val = true означает саму переменную;
val = false означает отрицание переменной.

То есть:

add_or(0, true, 1, false) означает (x1 ∨ ¬x2);
add_or(2, false, 2, false) означает (¬x3 ∨ ¬x3).

Полезные шаблоны¶

Хотим записать условие x = true:

sat.add_true(x, true);

Хотим записать условие x = false:

sat.add_true(x, false);

Хотим записать импликацию a → b. Это то же самое, что (¬a ∨ b).

Например, если нужно записать x1 → ¬x3:

sat.add_or(0, false, 2, false);

Пример моделирования задачи¶

Пусть нужно посадить трёх учеников либо в первую, либо во вторую команду.

Обозначим:

xi = true — ученик i в первой команде;
xi = false — ученик i во второй команде.

Ограничения:

Хотя бы один из 1-го и 2-го должен быть в первой команде:

(x1 ∨ x2)

Если 1-й в первой, то 3-й тоже в первой:

x1 → x3, то есть (¬x1 ∨ x3)

2-й и 3-й не могут одновременно быть в первой:

(¬x2 ∨ ¬x3)

Код:

TwoSAT sat(3);
sat.add_or(0, true, 1, true);
sat.add_or(0, false, 2, true);
sat.add_or(1, false, 2, false);

После solve() получим одно допустимое распределение.

Частые ошибки¶

1. Перепутать, какие рёбра добавляются¶

Для (a ∨ b) надо добавлять именно:

¬a → b
¬b → a

А не a → b и b → a.

2. Перепутать вершину и её отрицание¶

Нужно заранее выбрать чёткую схему индексации и везде придерживаться её.

Например:

2*i — xi
2*i+1 — ¬xi

или наоборот. Главное — не смешивать соглашения.

3. Ошибка в восстановлении ответа¶

Сравнение компонент зависит от того, в каком порядке они нумеровались. Если все ответы получаются инвертированными, обычно проблема именно в этом.

4. Забыть про нумерацию с нуля¶

Во многих задачах переменные даны с 1, а в коде удобнее хранить их с 0.

Что важно запомнить¶

2SAT — это формула, где каждая скобка содержит ровно два литерала.
Каждая скобка (a ∨ b) превращается в две импликации: ¬a → b и ¬b → a.
Строится граф импликаций на 2n вершинах.
Если x и ¬x в одной компоненте сильной связности, решения нет.
Иначе решение существует и восстанавливается по порядку компонент.
Временная сложность — линейная по размеру графа импликаций.

Небольшое сравнение: 2SAT и 3SAT¶

Важно понимать разницу:

2SAT решается эффективно;
3SAT в общем случае считается вычислительно трудной задачей.

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

Итог¶

Задача 2SAT — один из самых красивых примеров того, как логическая задача превращается в графовую.

На уровне формулы всё выглядит как работа с булевыми выражениями. На уровне алгоритма всё сводится к трём шагам:

построить граф импликаций;
найти компоненты сильной связности;
восстановить ответ по порядку компонент.

17.2 Задача 2SAT¶

Что такое 2SAT¶

Интуиция на простом примере¶

Ключевая идея: граф импликаций¶

Вершины графа¶

Рёбра графа¶

Как построить импликации¶

1. Скобка (x ∨ y)¶

2. Скобка (x ∨ ¬y)¶

3. Скобка (¬x ∨ ¬y)¶

4. Скобка (x ∨ x)¶

5. Скобка (¬x ∨ ¬x)¶

Почему здесь появляются компоненты сильной связности¶

Напоминание¶

Почему?¶

Критерий существования решения¶

Пример выполнимой формулы¶

Пример невыполнимой формулы¶

Как восстановить значения переменных¶

Почему правило с порядком компонент корректно¶

Удобная модель для олимпиадных задач¶

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

Сложность¶

Реализация на C++¶

Как пользоваться этой реализацией¶

Обозначения¶

Полезные шаблоны¶

Пример моделирования задачи¶

Частые ошибки¶

1. Перепутать, какие рёбра добавляются¶

2. Перепутать вершину и её отрицание¶

3. Ошибка в восстановлении ответа¶

4. Забыть про нумерацию с нуля¶

Что важно запомнить¶

Небольшое сравнение: 2SAT и 3SAT¶

Итог¶

1. Скобка `(x ∨ y)`¶

2. Скобка `(x ∨ ¬y)`¶

3. Скобка `(¬x ∨ ¬y)`¶

4. Скобка `(x ∨ x)`¶

5. Скобка `(¬x ∨ ¬x)`¶