SAT (булева выполнимость) — это задача присвоения переменным значений истинности так, чтобы заданная булева формула стала истинной.
Формула называется 2-SAT, если она записана в форме 2-CNF, то есть как И конъюнкция клауз, где каждая клауза содержит ровно два литерала.
Например:
Задача 2-SAT может быть решена за линейное время.
Основная идея — преобразовать формулу в граф импликаций.
Клауза
Решите эти внешние задачи (например, из Codeforces) чтобы закрепить материал урока:
эквивалентна паре импликаций
Действительно, если ложно, то должно быть истинно. Аналогично, если ложно, то должно быть истинно.
Таким образом, каждая клауза даёт нам две направленные импликации.
Мы строим ориентированный граф с вершинами, где — число переменных.
Для каждой переменной мы создаём две вершины:
Для клаузы
мы добавляем рёбра:
Например, для формулы
мы получаем следующие импликации:
После построения графа импликаций мы находим все сильно связные компоненты.
Пусть comp[x] — номер компоненты вершины x.
Если для некоторой переменной вершины и принадлежат одной и той же сильно связной компоненте, то решения не существует.
Почему? Потому что в этом случае:
то есть оба значения вынуждают друг друга, что невозможно.
Если для каждой переменной выполняется
то решение существует.
Чтобы построить одно корректное присваивание:
comp[x] > comp[not x];Это работает, когда компоненты обрабатываются в топологическом порядке.
Итоговая сложность:
где — число переменных, а — число импликаций.
int n;
vector<int> v[N]; // implication graph
vector<int> g[N]; // reversed graph
vector<int> order;
int comp[N];
bool used[N];
vector<int> res;
void add_edge(int x, int y) {
v[x].push_back(y);
g[y].push_back(x);
v[y ^ 1].push_back(x ^ 1);
g[x ^ 1].push_back(y ^ 1);
}
// add disjunction (x OR y)
void add_disjunction(int x, int y) {
add_edge(x ^ 1, y);
add_edge(y ^ 1, x);
}
void dfs1(int x) {
used[x] = true;
for (int y : v[x]) {
if (!used[y]) {
dfs1(y);
}
}
order.push_back(x);
}
void dfs2(int x, int c) {
comp[x] = c;
for (int y : g[x]) {
if (comp[y] == -1) {
dfs2(y, c);
}
}
}
bool solve_2SAT() {
order.clear();
for (int i = 0; i < 2 * n; i++) {
used[i] = false;
comp[i] = -1;
}
for (int i = 0; i < 2 * n; i++) {
if (!used[i]) {
dfs1(i);
}
}
for (int i = 2 * n - 1, C = 0; i >= 0; i--) {
int x = order[i];
if (comp[x] == -1) {
dfs2(x, C++);
}
}
res.clear();
for (int i = 0; i < 2 * n; i += 2) {
if (comp[i] == comp[i ^ 1]) {
return false;
} else if (comp[i] > comp[i ^ 1]) {
res.push_back(i);
}
}
return true;
}