2-SAT问题

SAT问题

• SAT: Satisfiability 满足
• 给出很多个包含多个命题的条件，给出命题的真假方案，使得所有条件成立
• 如：$对于命题x_1, x_2, x_3, x_4, x_5 \dots \\ 使得 x_1 \lor \neg x_2 \lor x_5成立$

2-SAT问题

• 每个条件包含两个命题的SAT问题

• 如：$对于x_1, x_2, x_3 \\ 使得 x_1 \lor x_3, \neg x_2 \lor x_3 成立$

• 转化：建图

• 用$x_i$表示$x_i = True$，用$\neg x_i$表示$x_i = False$

• 用图论里的每一个点表示每一个命题，每一条边表示每两个命题间的推导关系

  • 推导关系：$a \to b \Leftrightarrow \neg a \lor b \\ a, b \in \{\mathrm{True}, \mathrm{False}\}$
  • 即：$a \lor b \Leftrightarrow \neg a \to b \Leftrightarrow \neg b \to a$
  • 那么我们可以把每一个条件表示为图论中的边了

• 解的情况

• 无解：$x_i \to \dots \to x_i \land \neg x_i \to \dots x_i$

  • 即$x_i$和$\neg x_i$在同一个强连通分量里，说明$x_i$不管取真或假都是相反的，这就有问题了

• 有解：枚举所有$x_i$，缩点找强连通分量，当$x_i$所在的强连通分量的拓扑排序在$\neg x$所在的强连通分量的拓扑排序之后时，取$x$为true

• 模板（AcWing 2402）

#include <iostream>
#include <cstring>
#include <algorithm>

const int N = 2e6 + 5, M = 2 * 1e6 + 5;

int n, m;
int h[N], e[M], ne[M], idx;
int dfn[N], low[N], ts, stk[N], top;
int id[N], cnt;
bool ins[N];

void Add(int a, int b)
{
    e[idx] = b, ne[idx] = h[a], h[a] = idx++;
}

void Tarjan(int u)
{
    dfn[u] = low[u] = ++ts;
    stk[++top] = u;
    ins[u] = true;

    for (int i = h[u]; ~i; i = ne[i])
    {
        int j = e[i];
        if (!dfn[j])
        {
            Tarjan(j);
            low[u] = std::min(low[u], low[j]);
        }
        else if (ins[j])
        {
            low[u] = std::min(low[u], dfn[j]);
        }
    }

    if (low[u] == dfn[u])
    {
        int y;
        cnt++;
        do
        {
            y = stk[top--];
            ins[y] = false;
            id[y] = cnt;
        }
        while (y != u);
    }
}

int main()
{
    std::ios::sync_with_stdio(false);

    std::cin >> n >> m;
    memset(h, -1, sizeof h);

    while (m--)
    {
        int i, a, j, b;
        std::cin >> i >> a >> j >> b;
        i--, j--;
        Add(2 * i + !a, 2 * j + b);
        Add(2 * j + !b, 2 * i + a);
    }

    for (int i = 0; i < n * 2; i++)
        if (!dfn[i])
            Tarjan(i);

    for (int i = 0; i < n; i++)
        if (id[i * 2] == id[i * 2 + 1])
        {
            std::cout << "IMPOSSIBLE" << std::endl;
            return 0;
        }

    std::cout << "POSSIBLE" << std::endl;
    for (int i = 0; i < n; i++)
        if (id[i * 2] < id[i * 2 + 1])
            std::cout << "0 ";
        else std::cout << "1 ";
    return 0;
}