2–SAT 学习笔记

~~现在 2–SAT 已经是蓝题了吗。~~

由于我的模板都不知道是多少年前写的了，所以就有了这边文章。

2–SAT 问题

题意：

有 $n$ 个布尔变量 $x_1,x_2,\cdots,x_n$，另有 $m$ 个需要满足的条件，每个条件的形式都是「$x_i$ 为 true / false 或 $x_j$ 为 true / false」。比如「$x_1$ 为真或 $x_3$ 为假」、「$x_7$ 为假或 $x_2$ 为假」。

2–SAT 问题的目标是给每个变量赋值使得所有条件得到满足。

输入格式：

第一行两个整数 $n$ 和 $m$，意义如题面所述。

接下来 $m$ 行每行 $4$ 个整数 $i,a,j,b$，表示「$x_i$ 为 $a$ 或 $x_j$ 为 $b$」$(a, b\in \{0,1\})$

输出格式：

如无解，输出 IMPOSSIBLE；否则输出 POSSIBLE。

下一行 $n$ 个整数 $x_1,x_2,\cdots, x_n~(x_i\in\{0,1\})$，表示构造出的解。

数据范围：

$1\leq n, m\leq 10^6$

SAT 问题（satisfiability problem）指解决给定限制下，若干布尔变量的可满足性问题。

例如我想要知道

$(\neg a \vee b \vee \neg c) \wedge(a \vee b \vee \neg c) \wedge(\neg a \vee \neg b \vee c)$

对于布尔变量 $a,b,c$ 的一种可行方案

这里出现了 $3$ 个变量，即这是一个 3–SAT 问题；而本题只有两个变量和 $m$ 条限制，即 2–SAT 问题。

然而除了 2–SAT 问题以外的 SAT 问题均为 NPC 问题，因此关于 SAT 问题这部分的介绍就到此为止了。

现在考虑怎么做本题。我们把每个点看作 $x$ 和 $\lnot x$ ，不妨编号为 $x$ 和 $x + n$ 。

那么对于每条限制，我们可以转化为图上的一条边

$\begin{array}{|l|l|} \hline \neg a \vee b & a \rightarrow b \wedge \neg b \rightarrow \neg a \\ \hline a \vee b & \neg a \rightarrow b \wedge \neg b \rightarrow a \\ \hline \neg a \vee \neg b & a \rightarrow \neg b \wedge b \rightarrow \neg a \\ \hline \end{array}$

对应的代码就是：

while(m--)
{
    static int i, j; static bool a, b;
    cin >> i >> a >> j >> b;
    vec[i + n * a].pb(j + n * (b ^ 1));
    vec[j + n * b].pb(i + n * (a ^ 1));
}

注意到存在某个点 $x$ 满足 $x$ 和 $\lnot x$ 在同一个强连通分量中，一定无解。

对于有解的情况，我们取命题「 $x$ 的拓扑序大于 $\lnot x$ 的拓扑序」的值即可，这里拓扑序指缩点后的拓扑序。

不过由于 Tarjan 缩点以后每个点的编号正好是逆拓扑序，我们用小于判断即可。

时间复杂度 $\mathcal{O}(n + m)$

代码：（注意空间要开两倍）

#include <bits/stdc++.h>
using namespace std;
#define int long long
#define INF 0x3f3f3f3f3f3f3f3f
void up(int &x, int y) { x < y ? x = y : 0; }
void down(int &x, int y) { x > y ? x = y : 0; }
#define rep(i, a, b) for(int i = (a), i##END = (b); i <= i##END; i++)
#define Rep(i, a, b) for(int i = (a), i##END = (b); i >= i##END; i--)
#define pb push_back
#define N ((int)(2e6 + 15))

bool ins[N];
vector<int> vec[N];
int stktop, scnt, stk[N], low[N], dfn[N], scc[N], top[N]; 
void Tarjan(int u)
{
    static int tim = 0; dfn[u] = low[u] = ++tim;
    stk[++stktop] = u; ins[u] = true;
    for(int v : vec[u])
    {
        if(!dfn[v]) { Tarjan(v); down(low[u], low[v]); }
        else if(ins[v]) down(low[u], dfn[v]);
    }
    if(low[u] == dfn[u])
    {
        top[++scnt] = u;
        for(int p = 0; p != u; )
        { 
            p = stk[stktop--];
            ins[p] = false; scc[p] = scnt;
        }
    }
}
signed main()
{
    ios::sync_with_stdio(0);
    cin.tie(0); cout.tie(0);
    // freopen("check.in","r",stdin);
    // freopen("check.out","w",stdout);
    int n, m; cin >> n >> m;
    while(m--)
    {
        static int i, j; static bool a, b;
        cin >> i >> a >> j >> b;
        vec[i + n * a].pb(j + n * (!b));
        vec[j + n * b].pb(i + n * (!a));
    }
    rep(i, 1, n * 2) if(!dfn[i]) Tarjan(i);
    rep(i, 1, n) if(scc[i] == scc[i + n]) return cout << "IMPOSSIBLE\n", 0;
    cout << "POSSIBLE\n";
    rep(i, 1, n) cout << (scc[i] < scc[i + n]) << " \n"[i == n];
    return 0;
}