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;
}