图论--2-SAT--详解

问题描述：

现有一个由N个布尔值组成的序列A，给出一些限制关系，比如A[x]AND A[y]=0、A[x] OR A[y] OR A[z]=1等，要确定A[0..N-1]的值，使得其满足所有限制关系。这个称为SAT问题，特别的，若每种限制关系中最多只对两个元素进行限制，则称为2-SAT问题。

由于在2-SAT问题中，最多只对两个元素进行限制，所以可能的限制关系共有11种：

A[x]
NOT A[x]
A[x] AND A[y]
A[x] AND NOT A[y]
A[x] OR A[y]
A[x] OR NOT A[y]
NOT (A[x] AND A[y])
NOT (A[x] OR A[y])
A[x] XOR A[y]
NOT (A[x] XOR A[y])
A[x] XOR NOT A[y]

进一步，3可以用1表示：A[x]，A[y]，NOT(A[x] XOR A[y]) 相当于 NOT A[x] AND NOT A[y]。狄摩根定律。只剩下了9中基本关系类型。

在实际问题中，2-SAT问题在大多数时候表现成以下形式：有N对物品，每对物品中必须选取一个，也只能选取一个，并且它们之间存在某些限制关系（如某两个物品不能都选，某两个物品不能都不选，某两个物品必须且只能选一个，某个物品必选）等，这时，可以将每对物品当成一个布尔值（选取第一个物品相当于0，选取第二个相当于1），如果所有的限制关系最多只对两个物品进行限制，则它们都可以转化成9种基本限制关系，从而转化为2-SAT模型。

(引自：http://www.cnblogs.com/kuangbin/archive/2012/10/05/2712429.html)

2-SAT模型建立:

1.我们利用一条有向边<i,j>，来表示选i的情况下，一定要选j;

2.用i表示某个点是true,那么i'表示某个点是false

3.因为限制的两两之间的关系，所以我们可以通过逻辑关系来建边：

1）如果给出A和B的限制关系，A和B必须一起选，(A and B)||(!A and !B )==true 那么选A必须选B，建边<i,j>和<j,i>还有<i',j'>和<j',i'>

2）如果给出A和B的限制关系，选A不能选B，那么(A && !B)||(!A && B )==true,建边<i,j'>和<j,i'>

3）如果必须选A,那么A==true,建边<i',i>

4）如果A一定不能选，那么!A==true.建边<i,i'>

这么建图之后，会出现一个有向图，这个有向图会导致一个连通环，导致某个点一旦选取，那么这条链上的所有点都要被选中。如果我们找到一个强连通分量，那么这个强连通分量当中的点，如果选取必须全部选取，不选取的话一定是全部不选取，所以只要满足这个有向图中连通的点不会导致i和i'同时被选取，如果不存在矛盾，那么当前问题就是有解的。但是往往在求解过程中，我们要求的解会要求一些性质，所以提供以下几种解决方案。

用离散的的知识解释的话就是下面这位大佬的讲解（别人发给我的）

首先，把「2」和「SAT」拆开。SAT 是 Satisfiability 的缩写，意为可满足性。即一串布尔变量，每个变量只能为真或假。要求对这些变量进行赋值，满足布尔方程。

举个例子：教练正在讲授一个算法，代码要给教室中的多位同学阅读，代码的码风要满足所有学生。假设教室当中有三位学生：Anguei、Anfangen、Zachary_260325。现在他们每人有如下要求：

Anguei: 我要求代码当中满足下列条件之一：
1. 不写 using namespace std; （ ¬a）
2. 使用读入优化（b）
3. 大括号不换行（ ¬c）
Anfangen: 我要求代码当中满足下条件之一：
1. 写 using namespace std; （a）
2. 使用读入优化（b）
3. 大括号不换行（ $\neg �c$ ）
Zachary_260325：我要求代码当中满足下条件之一：
1. 不写 using namespace std; （ $\neg �a$ ）
2. 使用 scanf （ $\neg �b$ ）
3. 大括号换行（c）

我们不妨把三种要求设为 a,b,ca,b,c，变量前加 \neg¬ 表示「不」，即「假」。上述条件翻译成布尔方程即： $(\neg a\vee b\vee\neg c) \wedge (a\vee b\vee\neg c) \wedge (\neg a\vee\neg b\vee c)(�a%u2228b%u2228�c)%u2227(a%u2228b%u2228�c)%u2227(�a%u2228�b%u2228c)$ 。其中， $\vee%u2228$ 表示或， $\wedge%u2227$ 表示与。

现在要做的是，为 ABC 三个变量赋值，满足三位学生的要求。

Q: 这可怎么赋值啊？暴力？

A: 对，这是 SAT 问题，已被证明为 NP 完全 的，只能暴力。

Q: 那么 2-SAT 是什么呢？

A: 2-SAT，即每位同学 只有两个条件（比如三位同学都对大括号是否换行不做要求，这就少了一个条件）不过，仍要使所有同学得到满足。于是，以上布尔方程当中的 c, $\neg cc$ ,¬c 没了，变成了这个样子： $(\neg a\vee b) \wedge (a\vee b) \wedge (\neg a\vee\neg b)$

公式杀招：

怎么求解 2-SAT 问题？

使用强连通分量。 对于每个变量 xx，我们建立两个点：x ,¬x 分别表示变量 xx 取 true 和取 false。所以，图的节点个数是两倍的变量个数。在存储方式上，可以给第 ii 个变量标号为 ii，其对应的反值标号为 i + ni+n。对于每个同学的要求 (a∨b)，转换为 ¬a→b∧¬b→a。对于这个式子，可以理解为：「若 aa 假则 bb 必真，若 bb 假则 aa 必真」然后按照箭头的方向建有向边就好了。综上，我们这样对上面的方程建图：

原式	建图
$\neg a\vee b$	a→b∧¬b→¬a
$a \vee b$	¬a→b∧¬b→a
$\neg a\vee\neg b\space \space$	a→¬b∧b→¬a

于是我们得到了这么一张图：

可以看到，¬a 与 b 在同一强连通分量内，a与 ¬b 在同一强连通分量内。同一强连通分量内的变量值一定是相等的。也就是说，如果 x 与 ¬x 在同一强连通分量内部，一定无解。反之，就一定有解了。

但是，对于一组布尔方程，可能会有多组解同时成立。要怎样判断给每个布尔变量赋的值是否恰好构成一组解呢？

这个很简单，只需要 当 xx 所在的强连通分量的拓扑序在 \neg x¬x 所在的强连通分量的拓扑序之后取 xx 为真 就可以了。在使用 Tarjan 算法缩点找强连通分量的过程中，已经为每组强连通分量标记好顺序了——不过是反着的拓扑序。所以一定要写成 color[x] < color[-x] 。

代码实现：

//暴力DFS，求字典序最小的解，也是求字典序唯一的方法
#include<cstdio>
#include<cstring>
#include<vector>
using namespace std;
const int maxn=10000+10;
struct TwoSAT
{int n;//原始图的节点数(未翻倍)vector<int> G[maxn*2];//G[i]==j表示如果mark[i]=true,那么mark[j]也要=truebool mark[maxn*2];//标记int S[maxn*2],c;//S和c用来记录一次dfs遍历的所有节点编号void init(int n){this->n=n;for(int i=0;i<2*n;i++) G[i].clear();memset(mark,0,sizeof(mark));}//加入(x,xval)或(y,yval)条件//xval=0表示假，yval=1表示真void add_clause(int x,int xval,int y,int yval){x=x*2+xval;y=y*2+yval;G[x^1].push_back(y);G[y^1].push_back(x);}//从x执行dfs遍历,途径的所有点都标记//如果不能标记,那么返回falsebool dfs(int x){if(mark[x^1]) return false;//这两句的位置不能调换if(mark[x]) return true;mark[x]=true;S[c++]=x;for(int i=0;i<G[x].size();i++)if(!dfs(G[x][i])) return false;return true;}//判断当前2-SAT问题是否有解bool solve(){for(int i=0;i<2*n;i+=2)if(!mark[i] && !mark[i+1]){c=0;if(!dfs(i)){while(c>0) mark[S[--c]]=false;if(!dfs(i+1)) return false;}}return true;}
};

//联通分量+拓扑排序，求任意意一组解，比较快#include <cstdio>
#include <cstring>
#include <queue>
#include <vector>
#include <stack>
#include <algorithm>
#define MAXN 2000+10
#define MAXM 400000
#define INF 1000000
using namespace std;
vector<int> G[MAXN];
int low[MAXN], dfn[MAXN];
int dfs_clock;
int sccno[MAXN], scc_cnt;
stack<int> S;
bool Instack[MAXN];
int N, M;
void init()
{for(int i = 0; i < 2*N; i++) G[i].clear();
}
void getMap()
{int a, b, c;char op[10];while(M--){scanf("%d%d%d%s", &a, &b, &c, op);switch(op[0]){case 'A': if(c == 1)//a,b取1 {G[a + N].push_back(a);G[b + N].push_back(b);}else//a,b至少一个不为真 {G[a].push_back(b + N);G[b].push_back(a + N);}break;case 'O':if(c == 1)//a,b最少有一个为真 {G[b + N].push_back(a);G[a + N].push_back(b);}else//a,b都为假 {G[a].push_back(a + N);G[b].push_back(b + N);}break;case 'X':if(c == 1)//a b 不同值 {G[a + N].push_back(b);G[a].push_back(b + N);G[b].push_back(a + N);G[b + N].push_back(a);}else//a b 同真同假 {G[a].push_back(b);G[b].push_back(a);G[a + N].push_back(b + N);G[b + N].push_back(a + N);}}}
}
void tarjan(int u, int fa)
{int v;low[u] = dfn[u] = ++dfs_clock;S.push(u);Instack[u] = true;for(int i = 0; i < G[u].size(); i++){v = G[u][i];if(!dfn[v]){tarjan(v, u);low[u] = min(low[u], low[v]);}else if(Instack[v])low[u] = min(low[u], dfn[v]);}if(low[u] == dfn[u]){scc_cnt++;for(;;){v = S.top(); S.pop();Instack[v] = false;sccno[v] = scc_cnt;if(v == u) break; }}
}
void find_cut(int l, int r)
{memset(low, 0, sizeof(low));memset(dfn, 0, sizeof(dfn));memset(sccno, 0, sizeof(sccno));memset(Instack, false, sizeof(Instack));dfs_clock = scc_cnt = 0;for(int i = l; i <= r; i++)if(!dfn[i]) tarjan(i, -1);
}
void solve()
{for(int i = 0; i < N; i++){if(sccno[i] == sccno[i + N]){printf("NO\n");return ;}}printf("YES\n");
}
int main()
{while(scanf("%d%d", &N, &M) != EOF){init();getMap();find_cut(0, 2*N-1);solve();}return 0;
}