2-SAT: решение системы логических ограничений за O(V+E)

Коротко

Удивительный факт: задача выполнимости с двумя переменными в скобке решается за линейное время, хотя с тремя она NP-полна.

Постановка

Дана формула вида

(a ∨ ¬b) ∧ (¬a ∨ c) ∧ (b ∨ ¬c)

Каждая скобка содержит ровно два литерала (переменную или её отрицание). Нужно определить, можно ли присвоить переменным значения так, чтобы вся формула стала истинной, и если да — найти такое присвоение.

Практические задачи, которые к этому сводятся:

• расстановка объектов с ограничениями «либо A, либо B»;
• расписание: каждое событие в одном из двух слотов, некоторые пары конфликтуют;
• раскраска в два цвета с дополнительными условиями;
• размещение подписей на карте: каждая метка слева или справа от точки, метки не должны пересекаться.

Общий признак: у каждого объекта ровно два варианта, и есть парные ограничения.

Ключевой приём: скобка это две импликации

Скобка (a ∨ b) эквивалентна паре импликаций:

¬a → b      если a ложно, то b обязано быть истинно
¬b → a      если b ложно, то a обязано быть истинно

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

Теперь построим граф. Вершины — все литералы: x и ¬x для каждой переменной. Рёбра — импликации. Получается граф импликаций из 2n вершин.

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

Формула невыполнима тогда и только тогда, когда для какой-то переменной x литералы x и ¬x лежат в одной компоненте сильной связности.

Логика прозрачна: если x и ¬x взаимно достижимы, значит из x следует ¬x, и из ¬x следует x. Противоречие — любое значение переменной приводит к обратному.

Как восстановить ответ

Здесь тоже красивая идея. Строим конденсацию графа импликаций — она ациклическая. Для каждой переменной сравниваем порядок компонент в топологической сортировке:

если comp[x] стоит ПОЗЖЕ comp[¬x]  →  x = истина
иначе                               →  x = ложь

Интуиция: импликации ведут «вперёд», и брать нужно тот литерал, из которого ничего лишнего не следует.

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

Реализация

import sys


class TwoSAT:
    def __init__(self, n: int):
        self.n = n
        # 2n вершин: 2*i — переменная i истинна, 2*i+1 — ложна
        self.graph = [[] for _ in range(2 * n)]
        self.rgraph = [[] for _ in range(2 * n)]

    def _var(self, x: int, value: bool) -> int:
        return 2 * x + (0 if value else 1)

    def add_clause(self, x: int, xval: bool, y: int, yval: bool) -> None:
        """Добавить скобку (x=xval ИЛИ y=yval)."""
        # ¬x → y
        self._add_edge(self._var(x, not xval), self._var(y, yval))
        # ¬y → x
        self._add_edge(self._var(y, not yval), self._var(x, xval))

    def _add_edge(self, u: int, v: int) -> None:
        self.graph[u].append(v)
        self.rgraph[v].append(u)

    def solve(self):
        """Возвращает список значений или None, если решения нет."""
        size = 2 * self.n
        visited = [False] * size
        order = []

        # первый обход: порядок завершения
        for start in range(size):
            if visited[start]:
                continue
            stack = [(start, iter(self.graph[start]))]
            visited[start] = True
            while stack:
                node, it = stack[-1]
                advanced = False
                for nxt in it:
                    if not visited[nxt]:
                        visited[nxt] = True
                        stack.append((nxt, iter(self.graph[nxt])))
                        advanced = True
                        break
                if not advanced:
                    order.append(node)
                    stack.pop()

        # второй обход по транспонированному графу
        comp = [-1] * size
        current = 0
        for node in reversed(order):
            if comp[node] != -1:
                continue
            stack = [node]
            comp[node] = current
            while stack:
                v = stack.pop()
                for u in self.rgraph[v]:
                    if comp[u] == -1:
                        comp[u] = current
                        stack.append(u)
            current += 1

        # проверка и восстановление
        result = []
        for i in range(self.n):
            if comp[2 * i] == comp[2 * i + 1]:
                return None            # противоречие
            # компоненты нумеруются в обратном топологическом порядке
            result.append(comp[2 * i] < comp[2 * i + 1])

        return result


# (a ∨ ¬b) ∧ (¬a ∨ c) ∧ (b ∨ ¬c)
sat = TwoSAT(3)          # 0 = a, 1 = b, 2 = c
sat.add_clause(0, True, 1, False)
sat.add_clause(0, False, 2, True)
sat.add_clause(1, True, 2, False)

solution = sat.solve()
print(solution)          # [True, True, True]


# заведомо противоречивая система: (a) ∧ (¬a)
bad = TwoSAT(1)
bad.add_clause(0, True, 0, True)     # a ∨ a  →  a истинно
bad.add_clause(0, False, 0, False)   # ¬a ∨ ¬a →  a ложно
print(bad.solve())       # None

Кодирование одиночных условий

Часто нужны ограничения из одного литерала. Приём: продублировать литерал в скобке.

# «переменная x обязательно истинна»
sat.add_clause(x, True, x, True)

# «x и y не могут быть истинны одновременно»  →  (¬x ∨ ¬y)
sat.add_clause(x, False, y, False)

# «x и y обязаны совпадать»  →  (x∨¬y) ∧ (¬x∨y)
sat.add_clause(x, True, y, False)
sat.add_clause(x, False, y, True)

Таблица типовых ограничений экономит много времени при решении задач.

Почему 3-SAT сложнее

Скобка из двух литералов даёт импликацию — детерминированное следствие, которое ложится на граф.

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

Граница между полиномиальной и NP-полной задачей проходит ровно между двумя и тремя литералами. Это одна из самых наглядных иллюстраций теории сложности.

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

Одна импликация вместо двух. Скобка даёт две импликации; забыв одну, получите неверный ответ.

Неправильное сравнение компонент. Направление зависит от того, как алгоритм нумерует компоненты. При Тарьяне и при Косарайю знак может отличаться — проверьте на маленьком примере.

Отсутствие проверки на противоречие. Без неё вернётся мусор вместо None.

Путаница индексов литералов. Схема 2i и 2i+1 требует аккуратности; ошибка на единицу ломает всё.

Что запомнить

• 2-SAT решается за O(V + E) через граф импликаций и компоненты сильной связности.
• Каждая скобка (a ∨ b) превращается в две импликации: ¬a → b и ¬b → a.
• Решения нет, если x и ¬x попали в одну компоненту сильной связности.
• Ответ восстанавливается сравнением порядка компонент в топологической сортировке.
• С тремя литералами в скобке задача становится NP-полной.

Пройди собеседование в топ-компанию

Платформа для подготовки

Решай алгоритмические задачи как профи

✓ Популярные алгоритмы✓ Разбор решений✓ AI помощь

Начать сейчас→