一、问题引入

在了解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是否可满足的问题。（判断一般的合取范式是否可满足的问题是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$。

2. 建图

我们把每个子句表示成蕴含关系后，就可以根据蕴含关系建图。假设有$n$个布尔变量，那么图有$2n$个节点，每个变量及其否定各有一个节点。根据蕴含关系连边，若有$\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$相等。换言之，如果某个变量和其否定出现在了同一个强连通分量中，那么这个式子就是不可满足的。如果没有这种情况，就是可满足的。

4. 赋值

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

1. 若有从$x$到$\neg x$的路径，即$x\to \neg x$，那么只有当$x=0$的时候才能满足，此时$t_x<t_{\neg x}$；

2. 若有从$\neg x$到$x$的路径，即$\neg x\to x$，那么只有当$x=1$的时候才能满足，此时$t_x>t_{\neg x}$；

3. 若从$x$到$\neg x$没有路径，我们需要使各个变量的取值不会违反蕴含关系。设有蕴含关系$x\to y$，则必有$\neg y\to \neg x$。

   • 若先访问$x$、后访问$\neg y$，则$t_x<t_y<t_{\neg y}<t_{\neg x}$；

   • 若先访问$\neg y$，后访问$x$，则$t_{\neg y}<t_{\neg x}<t_x<t_y$，

   因此，如果我们仍然令 x = { 0 ,   t x < t ¬ x 1 , t x > t ¬ x x=

   {0, tx<t¬x1,tx>t¬x" role="presentation" style="position: relative;">{0, 1,tx<t¬xtx>t¬x$$\{\begin{array}{ll}0,& t_x<t_{\mathrm{\neg }x}\\ 1,& t_x>t_{\mathrm{\neg }x}\end{array}$$
   x={0, 1,​tx​<t¬x​tx​>t¬x​​，$y$同理，那么$x$和$y$取值相同，均不违反$x\to y$。

所以，对于变量$x$，我们对它的赋值是 x = { 0 ,   t x < t ¬ x 1 , t x > t ¬ x x=

x={0, 1,​tx​<t¬x​tx​>t¬x​​。

现在我们有一个疑问：既然可以这样决定变量的值，还怎么保证同一个强连通分量中的变量值相等呢？其实我们不用担心，因为应用这种赋值策略，同一个强连通分量中的变量的值一定是相同的。我们有以下结论：

命题 若$x$和$y$属于同一个强连通分量，则$\neg x$和$\neg y$属于同一个强连通分量。

要证明这个结论，需要用到

引理 若存在$x$到$y$的路径，则存在$\neg y$到$\neg x$的路径。

证明：设$x$到$y$的路径为$x\to p_1\to p_2\to \cdots \to p_k\to y$。我们上面提到，若有$a\to b$，则有$\neg b\to \neg a$；所以下列边存在：$\neg y\to \neg p_k$，$\neg p_k\to \neg p_{k-1}$，…，$\neg p_1\to \neg x$。所以$\neg y\to \neg p_k\to \neg p_{k-1}\to \cdots \to \neg p_1\to \neg x$就是从$\neg y$到$\neg x$的一条路径。

下面证明命题：

证明：由于$x$和$y$属于同一个强连通分量，那么有$x$到$y$的路径，也有$y$到$x$的路径。因此根据引理有$\neg y$到$\neg x$的路径，也有$\neg x$到$\neg y$的路径。于是$\neg x$和$\neg y$属于同一个强连通分量。

于是，对于同一个强连通分量中的两个变量$x$和$y$，，这样得出$x$和$y$的赋值一定是相等的。

三、两个例子

第一个

给定的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=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$$\sim$$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\sim x_n$（ x i ∈ { 0 , 1 } x_i\in\{0,1\} xi​∈{0,1}），表示构造出的解。

样例 #1

样例输入 #1

3 1
1 1 3 0
1
2

样例输出 #1

POSSIBLE
0 0 0
1
2

提示

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

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

代码实现

#include 
#include 
#include 

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;
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)
{
    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;
}
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77