一、问题引入

在了解2-SAT的定义之前，我们需要给出一些基础定义。

布尔变量（Boolean variable）：只能取$1$（true）或$0$（false）的变量。

否定连接词$\neg$（negation）：取布尔变量的否定。例如$\neg 1=0$，$\neg 0=1$。$\neg (\neg a)=a$。

合取连接词$\wedge$（conjunction）：表示“且”。$a\wedge b=1$当且仅当$a,b$同时为$1$。

析取连接词$\vee$（disjunction）：表示“或”。$a\vee b=1$当且仅当$a,b$之中至少有一个为$1$。

蕴含连接词$\to$（implication）：$a\to b$等价于$\neg a\vee b$。$a\to b=1$当且仅当$a=0$或$b=1$。换言之，若$a=1$，则必有$b=1$，否则蕴含关系不成立；若$a=0$，则不论$b$取何值，蕴含关系都成立。

文字（literal）：变量$x$及其否定$\neg x$称为文字。

子句/简单析取式（clause）：若干个文字由析取连接词连接起来形成的布尔表达式称为简单析取式。例如$a\vee b\vee \neg c$，$\neg d\vee d\vee e\vee \neg f$。

合取范式（CNF，Conjunctive Normal Form）：若干个简单析取式由合取连接词连接起来形成的布尔表达式称为合取范式（即“简单析取式的合取”）。例如$(p\vee \neg q)\wedge (\neg p\vee r\vee s)\wedge \neg r\wedge (s\vee \neg s)$，它有四个子句。

2-CNF：每个子句仅包含两个文字的合取范式。例如$(a\vee \neg b)\wedge (b\vee c)\wedge (c\vee \neg f)\vee (\neg d\vee e)$。

布尔表达式的可满足性：对于一个布尔表达式，如果存在各变量的一组赋值，使得该表达式的值为$1$，则称该表达式是可满足的。对于合取范式，因为各子句之间是且的关系，所以要使它取值为$1$就必须使各子句取值都为$1$。对于上面给出的式子$(a\vee \neg b)\wedge (b\vee c)\wedge (c\vee \neg f)\vee (\neg d\vee e)$，令$a=1,b=1,c=1,d=0,e=0,f=1$可以使其取值为$1$，所以它是可满足的；但对于式子$(a\vee \neg b)\wedge (b\vee c)\wedge (b\vee \neg c)\wedge (\neg a\vee \neg b)$，不论$a,b,c$取何值，式子的值都是$0$，因此它是不可满足的。

2-SAT：也称2-CNF-SAT，是判断2-CNF是否可满足的问题。（判断一般的合取范式是否可满足的问题是$\mathsf{NP}$完全问题，至今没有发现多项式时间的算法；但2-SAT是一个特例，具有高效算法。）

二、问题求解

1. 转化为蕴含关系

考虑2-CNF的一个子句$(a\vee \neg b)$，要让这个子句满足，就是让$(a\vee \neg b)=1$。现在令$a=0$，那么$\neg b$一定等于$1$，因为如果$\neg b$也等于$0$，那么$a$和$\neg b$同时为$0$，该子句的取值就是$0$了；同理，若$\neg b=0$，则可以知道$a$一定是$1$。换言之：$\neg a$（$a=0$）可以推出$\neg b$，而$b$（$\neg b=0$，即$\neg (\neg b)=b=1$）可以推出$a$。所以，$(a\vee \neg b)$就等价于$(\neg a\to \neg b)\wedge (b\to a)$。一般地，设$p,q$是两个文字，则子句$(p\vee q)$等价于两个蕴含关系$\neg p\to q$和$\neg q\to p$。若$p=a$，则$\neg p=\neg a$；若$p=\neg a$，则$\neg p=\neg (\neg a)=a$。

具体地说，我们获得蕴含关系方式由下表给出：

子句	蕴含关系
$a\vee b$	$\neg a\to b$和$\neg b\to a$
$a\vee \neg b$	$\neg a\to \neg b$和$b\to a$
$\neg a\vee b$	$a\to b$和$\neg b\to \neg a$
$\neg a\vee \neg b$	$a\to \neg b$和$b\to \neg a$

2. 建图

我们把每个子句表示成蕴含关系后，就可以根据蕴含关系建图。假设有$n$个布尔变量，那么图有$2n$个节点，每个变量及其否定各有一个节点（比如变量$a$对应两个节点：$a$和$\neg a$）。根据蕴含关系连边，若有$\neg a\to \neg b$就从$\neg a$向$\neg b$连一条边；若有$b\to a$就从$b$向$a$连一条边。注意，每个子句连$2$条边：若$p$到$q$有一条边，那么$\neg q$到$\neg p$也有一条边（可以通过逆否命题和原命题等价来理解）。

3. 判断可满足性

我们说“$a\to b$”，指的是若$a=1$，那么$b$一定等于$1$；若$a\ne 1$，那么$b$等于什么都可以。蕴含关系有传递性，例如$a\to b$、$b\to c$就有$a\to c$。若图中有从$a$到$b$的一条路径，那么就有$a\to b$。若$a$和$b$处于同一个强连通分量中，即$a$到$b$有路径、$b$到$a$有路径，那么就有$a\to b$、$b\to a$，此时，若$a=1$，则$b=1$；若$b=1$，则$a=1$；若$a=0$，则$b=0$，因为如果$b=1$的话就有$a=1$了。于是我们得出结论：若$a$和$b$处于同一个强连通分量中，则有$a\to b\wedge b\to a$，此时$a$和$b$取值必须相同。

什么时候不可满足呢？就是出现矛盾的时候。所谓矛盾，就是存在变量$x$，使得$x$和$\neg x$相等。换言之，如果某个变量和其否定出现在了同一个强连通分量中，那么这个式子就是不可满足的。如果没有这种情况，就是可满足的。

详细地说，如果$x$和$\neg x$在同一个强连通分量中，那么我们有$x\to \neg x$和$\neg x\to x$。如果$x=1$，那么由$x\to \neg x$得$\neg x=1$，即$x=0$，但是一个变量不能同时取$1$和$0$，所以不成立；如果$x=0$，那么$\neg x=1$，由$\neg x\to x$得$x=1$，同样出现了矛盾。反之，如果没有一个变量，使得它本身和它的否定在同一个强连通分量中，那么我们总能构造出一个可满足赋值，这就是下一段讨论的内容。因此，“某一个变量的本身和否定在同一个强连通分量中”是输入的2-CNF不可满足的充要条件。

4. 赋值

当我们知道某个式子是可满足的时候，我们希望找到使其值为$1$的一组变量的赋值。此时对于变量$x$，$x$和$\neg x$一定不属于同一个强连通分量。要求出强连通分量，就需要对原图进行缩点，顺便可以求出得到的有向无环图的拓扑序。令$x$所在强连通分量的拓扑序为$t_x$。我们这样进行赋值：

• 若$t_x<t_{\neg x}$，则令$x=0$；
• 若$t_x>t_{\neg x}$，则令$x=1$。

$t_x=t_{\neg x}$的情况是不存在的，因为$x$和$\neg x$不在同一个强连通分量中。

如果有从$x$到$\neg x$或从$\neg x$到$x$的路径，那么这个很好理解。

• $t_x<t_{\neg x}$就是说有从$x$到$\neg x$的路径，这种情况下我们有$x\to \neg x$，只有当$x=0$的时候才可满足。
• $t_x>t_{\neg x}$就是说有从$\neg x$到$x$的路径，这种情况下我们有$\neg x\to x$，只有当$x=1$的时候才可满足。

下面我们来证明这种赋值办法不会违反任何蕴含关系。

• 首先，它不会违反$x$和$\neg x$之间的蕴含关系，因为$x$和$\neg x$属于不同的强连通分量，二者之间最多只能有一个蕴含关系，而我们赋值的方法总能满足这个蕴含关系。
• 其次，我们考虑变量$x$和另一个变量$y$的蕴含关系。我们假设有$x\to y$（如果有$\neg x\to y$、$x\to \neg y$、$\neg x\to \neg y$同理）。我们担心的情况是：$x=1$但$y=0$，这样蕴含关系就被违反了。下面我们用反证法证明这种情况不存在。假设有$x=1$、$y=0$、$x\to y$三个条件，那么我们可以得出以下结论：
  • 由$x=1$知道$t_{\neg x}<t_x$（见两个赋值规则）；
  • 由$y=0$知道$t_y<t_{\neg y}$；
  • 由$x\to y$知道$t_x\le t_y$。（如果$x$与$y$在同一个强连通分量里，则$t_x=t_y$；如果在不同的强连通分量里，那么我们有从$x$到$y$的一条边，因此$x$比$y$先被访问。至于为什么如果有$x$到$y$的边那么$x$比$y$先被访问，这是拓扑排序的定义。）
• 综合这三个不等式，我们得到$t_{\neg x}<t_x\le t_y<t_{\neg y}$。但是，我们知道原命题等价于逆否命题，也就是说，$x\to y$成立意味着$\neg y\to \neg x$也一定成立，这表明$t_{\neg y}\le t_{\neg x}$，与绿色不等式矛盾。因此假设不成立，违反$x\to y$的情况不存在，换言之，所有蕴含关系都被满足了，这意味着输入的2-CNF公式被满足了。综上所述，我们的赋值策略是正确的。

三、两个例子

第一个例子

给定的2-CNF表达式为$(a\vee \neg b)\wedge (\neg a\vee b)\wedge (b\vee \neg c)\wedge (a\vee c)$。

图包含四个强连通分量： { a , b } , { c } , { ¬ a , ¬ b } , { ¬ c } \{a,b\},\{c\},\{\neg a,\neg b\},\{\neg c\} {a,b},{c},{¬a,¬b},{¬c}。没有出现某个变量及其否定在同一个强连通分量的情况，所以是可满足的。进行缩点：

拓扑序为$t_{\neg a,\neg b}<t_c<t_{\neg c}<t_{a,b}$。因为$t_{\neg a}<t_a$，所以$a=1$。同理$b=1$。因为$t_c<t_{\neg c}$，所以$c=0$。

将$a=1,b=1,c=0$代入2-CNF中验算可得其值为$1$。

第二个例子

给定的2-CNF表达式为$(a\vee \neg b)\wedge (b\vee c)\wedge (b\vee \neg c)\wedge (\neg a\vee \neg b)$。

所有节点都在同一个强连通分量中，所以这个式子不可满足。

四、基于Tarjan算法的代码实现

详细思路

设有$n$个变量，$m$个子句，则有$2n$个节点。编号$i$（$1\le i\le n$）的节点对应变量$x_i$，$i+n$对应$\neg x_i$。根据每个子句建图，图中共$2m$条边。使用Tarjan算法进行缩点，co数组存储每个节点的染色，实际上就是有向无环图的逆拓扑序（因为在DFS树中越深的节点越先被染色）。对于每个变量$x_i$，考察节点$i$和节点$i+n$的染色是否相同，若相同说明$x_i$和$\neg x_i$在同一个强连通分量，出现矛盾。而后根据拓扑序进行赋值：若$i$的拓扑序小于$i+n$，对应co[i] > co[i + n]，$x_i=0$；反之$x_i=1$。可以简写为$x_i=$co[i] < co[i + n]。

洛谷P4782 【模板】2-SAT 问题

题目描述

有 $n$ 个布尔变量 $x_1$~$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 ∈ { 0 , 1 } a, b\in \{0,1\} a,b∈{0,1})

输出格式

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

下一行 $n$ 个整数 $x_1$~$x_n$（ x i ∈ { 0 , 1 } x_i\in\{0,1\} xi​∈{0,1}），表示构造出的解。

样例 #1

样例输入 #1

3 1
1 1 3 0

样例输出 #1

POSSIBLE
0 0 0

提示

$1\le n,m\le 10^6$ , 前 $3$ 个点卡小错误，后面 $5$ 个点卡效率。

由于数据随机生成，可能会含有（10 0 10 0）之类的坑，但按照最常规写法的写的标程没有出错，各个数据点卡什么的提示在标程里

分析

我们需要把条件“$x_i$为$a$或$x_j$为$b$”转化为子句。其实$a=0$表示子句中$x_i$前面有否定连接词，$b=0$表示子句中$x_j$前面有否定连接词。转换关系如下：

$a$	$b$	子句	第一个蕴含关系	第二个蕴含关系
$1$	$1$	$x_i\vee x_j$	$\neg x_i\to x_j$	$\neg x_j\to x_i$
$1$	$0$	$x_i\vee \neg x_j$	$\neg x_i\to \neg x_j$	$x_j\to x_i$
$0$	$1$	$\neg x_i\vee x_j$	$x_i\to x_j$	$\neg x_j\to \neg x_i$
$0$	$0$	$\neg x_i\vee \neg x_j$	$x_i\to \neg x_j$	$x_j\to \neg x_i$

因为$\neg y$在图中对应的节点编号为$y$的编号加$n$，所以加入第一个蕴含关系时我们判断$a$是否为$1$，若为$1$则给$x_i$的编号加$n$变成$\neg x_i$；若$b$为$0$则给$x_j$的编号加$n$变成$\neg x_j$。加入第二个蕴含关系时，若$b=1$给$x_j$加$n$，若$a=0$给$x_i$加$n$。

代码实现

#include <iostream>
#include <cstdio>
#include <stack>

using namespace std;

const int MAXN = 2e6 + 5, MAXM = 2e6 + 5;

int n, m, tot, nxt[MAXM], first[MAXN], go[MAXM],
    dfn[MAXN], low[MAXN], co[MAXN], col; 
// n为变量个数，m为条件（子句）个数，nxt、first、go是链式前向星用到的数组，
// dfn为Tarjan算法的DFS序数组，low为Tarjan算法的low数组，
// co是颜色（即节点的强连通分量编号），col为强连通分量个数
stack<int> stk;

inline void add_edge(int u, int v) // 加边
{
    nxt[++tot] = first[u];
    first[u] = tot;
    go[tot] = v;
}

void Tarjan(int u) // Tarjan算法求强连通分量
{
    low[u] = dfn[u] = ++tot;
    stk.push(u);
    for(int e = first[u]; e; e = nxt[e])
    {
        int v = go[e];
        if(!dfn[v])
        {
            Tarjan(v);
            low[u] = min(low[u], low[v]);
        }
        else if(!co[v])
        {
            low[u] = min(low[u], low[v]);
        }
    }
    if(low[u] == dfn[u])
    {
        co[u] = ++col;
        while(stk.top() != u)
            co[stk.top()] = col, stk.pop();
        stk.pop();
    }
}

int main()
{
    cin >> n >> m;
    for(int t = 1; t <= m; ++t) // 连边
    {
        int i, a, j, b;
        cin >> i >> a >> j >> b;
        int u = i;
        if(a) u += n;
        int v = j;
        if(!b) v += n;
        add_edge(u, v);
        u = j;
        if(b) u += n;
        v = i;
        if(!a) v += n;
        add_edge(u, v);
    }
    for(int i = 1; i <= 2 * n; ++i)
        if(!dfn[i]) Tarjan(i); // Tarjan缩点
    for(int i = 1; i <= n; ++i)
        if(co[i] == co[i + n]) // 判断冲突
        {
            puts("IMPOSSIBLE");
            return 0;
        }
    puts("POSSIBLE");
    for(int i = 1; i <= n; ++i) // 赋值
        cout << (co[i] < co[i + n]) << ' ';
    cout << endl;
    return 0;
}