P4782 【模板】2-SAT 问题 && 2-SAT问题

2-SAT到图论

(k-SAT) 是 k-适应性问题（Satisfiability）的简称。
(k-SAT) 问题（除 (k = 2)）已被证明为是 (NP) 完全问题，而对于 (k = 2) 的 (2-SAT) 问题，我们可以用图论求解。

(k-SAT) 与 (2-SAT) 最大的不同在与这个(2) 废话，就因为这个 “2”，我们可以由假设的第一个限制条件推知第二个限制条件
举个栗子：限制条件为 (a) ^ $b = 1 $ （对于 (a) ）有

[ a xor b = 1 Rightarrow left{ egin{aligned} a = 1 Rightarrow b = 0 \ a = 0 Rightarrow b = 1 end{aligned} ight. ]

依据限制条件，我们可以搞一个通式有助后边理解： (a = x) 则 (b = y) （a、 b、 x 已知且 (x, y in {0, 1}) ）
于是，我们把问题转换到图中：引入一条有向边，起点为通式则的左边，终点为则右边，这条边的意义为 必须选中，即选择了起点就必须选择终点。

以上文的限制条件为例，我们将 x 变量为假设为 x （(x << 1)）， x 变量为真设为 x'（(x << 1 | 1)），可以作如下转换（对于 (a) ）：

[ a xor b = 1 Rightarrow left{ egin{aligned} a' ightarrow b \ a ightarrow b' end{aligned} ight. ]

其代表的含义为： 选择了 a 为真则一定选择 b 为假，选了 a 为假则一定选择 b 为真
这只是对 (a) 进行讨论，事实上对于异或这一条件我们需要连 (4) 条边（上面两条和对于 (b) 的两条）

可以联想到： 在此图中沿着一条路走下去其实就是逻辑推断的过程

合法性的判断

这样我们就得到了一个图。如何快速的判断是否能满足所有限制条件呢？我们需要在图上做文章了。
不合法显然意味着矛盾，什么时候会产生矛盾呢？
一个人不可能既是男的又是女的。花是妹子，花是男的，这显然就矛盾了吗
我们假设 (x) 为假，经过一系列推断，我们推出了 (x) 为真，这显然矛盾，问题无解

上文提到过， 推断过程其实就是走有向边遍历的过程，那么若是存在一个环，同时包含了 (x) 和 (x')，那么问题无解。
更确切的说：当一个变量的两对立面（即 (x) 和 (x')）同时存在于一个强联通分量中时，问题无解。

所以我们跑一次 (Tarjan) 判断每一元素的两对立面是否在同一强联通分量即可判断是否合法

方案输出

先导知识：你真的了解 Tarjan 吗

你可能知道： (Tarjan) 可以求强联通分量，并对在同一个强联通分量中的点染色
可你真的知道染色的顺序有什么流弊的东西吗

反向拓扑序？拜托，别搞那些花里胡哨的

因为 (Tarjan) 是利用 (dfs) 实现的，说到底用的是栈，先进后出，所以对于两个点 (u,v) 若是两个点没有被 (Tarjan) 过，且能从 (u) 点到达 (v) 点，那么 (col[v] <= col[u]) （其中 (=) 是两点处于一个强联通分量的时候），即 (v) 比 (u) 先完成染色（其实就是个逆拓扑序啦）
而对于两个点，他们无法互相通达，那么先 (Tarjan) 哪一个，那一个点的颜色编号较小

优先级

在 (2-SAT) 问题中，我们用 (Tarjan) 不仅是求出了强联通分量，他还进行了一个遍历整个图的过程，也就是说，我们利用 (Tarjan) 完成了逻辑推理。

因为遍历有先后，所以所对应的逻辑推理也有一个优先级（这点很重要）：试想现在有一个点 (X)，我们从 (X) 出发进行 (Tarjan) ，他的所有子节点（(x_{1},x_{2}...,x_{n})）的颜色编号小于等于此节点的颜色编号（即 (col[X] >= col[x_{1},x_{2}...,x_{n}])），我们可以认为这些子节点是由这一个点逻辑推理出来的；好的现在我们遍历下一个点 (Y)，他的所有子节点（(y_{1},y_{2}...,y_{m})）颜色编号小于 (col[Y])，所以我们可以得到一个式子：

[col[x_{1},x_{2}...,x_{n}] <= col[X] <= col[y_{1},y_{2}...,y_{m}] <= col[Y] ]

从中间的 (<=) 号处切开，左右分类，可以很清晰的看出他们的优先级关系，所以我们得到结论： 颜色标号越小，优先级越高

所以输出方案时（当然已经判断合法后）选取真和假这两个对立面中颜色编号较小的点，他的优先级高，我们选取他即可

几种模型

逻辑运算无非 (or, and, xor) 这三种，所以模型并不是很多（依然 (x) 代表假， (x') 代表真）

(a or b = 0)

即 (a = b = 0)，优先级 (0 >1)
(a' ightarrow a)
(b' ightarrow b)

(a or b = 1)

即两个不能同时为 (0 Rightarrow) 一个为 (0) 则另一个为 (1)
(a ightarrow b')
(b ightarrow a')

(a and b = 0)

即两个不能同时为 (1 Rightarrow) 一个为 (1) 则另一个为 (0)
(a' ightarrow b)
(b' ightarrow a)

(a and b = 1)

即 (a = b = 1)，优先级 (1 > 0)
(a ightarrow a')
(b ightarrow b')

(a xor b = 0)

即两个变量相同
(a ightarrow b)
(a' ightarrow b')
(b ightarrow a)
(b' ightarrow a')

(a xor b = 1)

即两个变量不同
(a ightarrow b')
(a' ightarrow b)
(b ightarrow a')
(b' ightarrow a)

P4782 【模板】2-SAT 问题

题目背景
2-SAT 问题模板

题目描述
有n个布尔变量 x_1x ~ 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})

输出格式：
如无解，输出“IMPOSSIBLE”（不带引号）; 否则输出"POSSIBLE"（不带引号),下一行n个整数 x_1 ~ x_n（ x_i∈{0,1}），表示构造出的解。

蛮裸的，主要靠输出方案，搞清楚优先级即可

Code

#include<iostream>
#include<cstdio>
#include<queue>
#include<cstring>
#include<algorithm>
typedef long long LL;
using namespace std;
int RD(){
    int out = 0,flag = 1;char c = getchar();
    while(c < '0' || c >'9'){if(c == '-')flag = -1;c = getchar();}
    while(c >= '0' && c <= '9'){out = out * 10 + c - '0';c = getchar();}
    return flag * out;
    }
const int maxn = 2000019,INF = 1e9 + 19;
int head[maxn],nume = 1;
struct Node{
    int v,dis,nxt;
    }E[maxn << 2];
void add(int u,int v,int dis){
    E[++nume].nxt = head[u];
    E[nume].v = v;
    E[nume].dis = dis;
    head[u] = nume;
    }
int num, nr;
int DFN[maxn], LOW[maxn], INDEX;
int S[maxn], top;
bool ins[maxn];
int col[maxn], numc;
void Tarjan(int u){
	DFN[u] = LOW[u] = ++INDEX;
	S[++top] = u;ins[u] = 1;
	for(int i = head[u];i;i = E[i].nxt){
		int v = E[i].v;
		if(!DFN[v])Tarjan(v), LOW[u] = min(LOW[u], LOW[v]);
		else if(ins[v])LOW[u] = min(LOW[u], DFN[v]);
		}
	if(DFN[u] == LOW[u]){
		numc++;
		while(S[top + 1] != u){
			col[S[top]] = numc;
			ins[S[top--]] = 0;
			}
		}
	}
int main(){
	num = RD();nr = RD();
	for(int i = 1;i <= nr;i++){
		int a = RD(), x = RD(), b = RD(), y = RD();
		//<< 1 | 0 -> 0 , << 1 | 1 -> 1
		add(a << 1 | (x ^ 1), b << 1 | y, 1);
		add(b << 1 | (y ^ 1), a << 1 | x, 1);
		}
	for(int i = 2;i <= (num << 1 | 1);i++)if(!DFN[i])Tarjan(i);
	for(int i = 1;i <= num;i++){
		if(col[i << 1] == col[i << 1 | 1]){
			puts("IMPOSSIBLE");
			return 0;
			}
		}
	puts("POSSIBLE");
	for(int i = 1;i <= num;i++){
		if(col[i << 1] < col[i << 1 | 1])printf("0 ");
		else printf("1 ");
		}
	puts("");
	return 0;
	}