浅谈2—SAT问题

2-SAT：

2 - SAT就是2判定性问题，是一种特殊的逻辑判定问题。
2

2 - SAT问题有何特殊性？该如何求解？
3

我们从一道例题来认识2 - SAT问题，并提出对一类2 - SAT问题通用的解法。
4

Poi 0106 Peaceful Commission [和平委员会]：

某国有n个党派，每个党派在议会中恰有2个代表。

现在要成立和平委员会，该会满足：

每个党派在和平委员会中有且只有一个代表

如果某两个代表不和，则他们不能都属于委员会

代表的编号从1到2n，编号为2a - 1 、2a的代表属于第a个党派

输入n（党派数），m（不友好对数）及m对两两不和的代表编号

其中1≤n≤ 8000 ， 0 ≤m ≤ 20000

求和平委员会是否能创立。若能，求一种构成方式。

输入：输出：

3 2 1

1 3 4

2 4 5

原题可描述为：

有n个组，第i个组里有两个节点Ai, Ai ' 。需要从每个组中选出一个。而某些点不可以同时选出（称之为不相容）。任务是保证选出的n个点都能两两相容。

（在这里把Ai, Ai ' 的定义稍稍放宽一些，它们同时表示属于同一个组的两个节点。也就是说，如果我们描述Ai，那么描述这个组的另一个节点就可以用Ai ' ）

初步构图

如果Ai与Aj不相容，那么如果选择了Ai，必须选择Aj‘ ；同样，如果选择了Aj，就必须选择Ai’ 。

Ai Aj '

Aj Ai‘

这样的两条边对称

我们从一个例子来看：

假设4个组，不和的代表为：1和4，2和3，7和3，那么构图：

假设：首先选1 3必须选，2不可选 8必须选， 4 、7不可选 5 、6可以任选一个

矛盾的情况为：

存在Ai，使得Ai既必须被选又不可选。

得到算法1：

枚举每一对尚未确定的Ai, Ai‘ ，任选1个，推导出相关的组，若不矛盾，则可选择；否则选另1个，同样推导。若矛盾，问题必定无解。

此算法正确性简要说明：

由于Ai,Ai ' 都是尚未确定的，它们不与之前的组相关联，前面的选择不会影响Ai, Ai ' 。

算法的时间复杂度在最坏的情况下为O(nm)。

在这个算法中，并没有很好的利用图中边的对称性

更一般的说：

在每个一个环里，任意一个点的选择代表将要选择此环里的每一个点。不妨把环收缩成一个子节点（规定这样的环是极大强连通子图）。新节点的选择表示选择这个节点所对应的环中的每一个节点.

对于原图中的每条边Ai -> Aj（设Ai属于环Si，Aj属于环Sj）如果Si≠Sj，则在新图中连边:Si -> Sj

这样构造出一个新的有向无环图。

此图与原图等价。

通过求强连通分量，可以把图转换成新的有向无环图，在这个基础上，介绍一个新的算法。

新算法中，如果存在一对Ai, Ai ' 属于同一个环，则判无解，否则将采用拓扑排序，以自底向上的顺序进行推导，一定能找到可行解。

至于这个算法的得来及正确性，将在下一段文字中进行详细分析。

回忆构图的过程：

对于两个不相容的点 Ai, Aj，构图方式为：Ai -> Aj ' ,Aj->Ai ' ,前面提到过，这样的两条边对称，也就是说：

如果存在Ai -> Aj，必定存在Aj ' ->Ai ' 。

等价于：Ai -> Ak,Ak ' ->Ai ' 方便起见，之后“ -> ”代表这样一种传递关系.

猜测1：图中的环分别对称

如果存在Ai,Aj，Ai,Aj属于同一个环(记作Si),那么Ai ' , Aj ' 也必定属于一个环(记作Si ' ).

再根据前面的引理，不难推断出每个环分别对称。

证明方式与引理相类似

一个稍稍复杂点的结构,其中红、蓝色部分分别为两组对称的链结构

推广2：对于任意一对Si, Si ' ，Si的后代节点与Si ' 的前代节点相互对称。

继而提出:

猜测2：若问题无解，则必然存在Ai, Ai ' ，使得Ai,Ai ' 属于同一个环。也就是，如果每一对Ai,Ai ' 都不属于同一个环，问题必定有解。下面给出简略证明：

先提出一个跟算法1相似的步骤：

如果选择Si，那么对于所有Si -> Sj，Sj都必须被选择。

而Si ' 必定不可选，这样Si’的所有前代节点也必定不可选（将这一过程称之为删除）。

由推广2可以得到，这样的删除不会导致矛盾。

假设选择S3 '

选择S3 ' 的后代节点, S1 '

删除S3

删除S3的前代节点S1

S1与S1 ' 是对称的

每次找到一个未被确定的Si，使得不存在Si -> Si ' 选择Si及其后代节点而删除Si’及Si‘的前代节点。一定可以构造出一组可行解。

因此猜测2成立。

另外，若每次盲目的去找一个未被确定的Si，时间复杂度相当高。

以自底向上的顺序进行选择、删除，这样还可以免去“选择Si的后代节点”这一步。

用拓扑排序实现自底向上的顺序。

一组可能的拓扑序列(自底向上）:S1 ' ,S2,S2 ' ,S3 ' ,S3,S1

算法2的流程：

1 ．构图

2 ．求图的极大强连通子图

3 ．把每个子图收缩成单个节点，根据原图关系构造一个有向无环图

4 ．判断是否有解，无解则输出（退出）

5 ．对新图进行拓扑排序

6 ．自底向上进行选择、删除

7 ．输出

小结：

整个算法的时间复杂度大概是O(m)，解决此问题可以说是相当有效了。

在整个算法的构造、证明中反复提到了一个词：对称。发现、利用了这个图的特殊性质，我们才能够很好的解决问题。

并且，由2 - SAT问题模型变换出的类似的题目都可以用上述方法解决。

全文总结：

充分挖掘图的性质，能够更好的解决问题。

不仅仅是对于图论，这种思想可以在很多问题中得到很好的应用。

希望我们能掌握此种解题的思想，在熟练基础算法的同时深入分析、灵活运用、大胆创新，从而解决更多更新的难题。

2-sat问题

2013 年 02 月 02 日 isnowfy algorithm

Go to comment

Implication_graph

在这篇文章我们提到过sat问题，sat问题是第一个npc问题，具体是这样的SAT全称是satisfiability，他是问对于一个合取范式，是否有一种输入使得他的输出是1，具体点就是类似这样的布尔表达式（x1 or x2 or x3）and(x3 or x4)and(not x1 or x5)对于所有的x是否有一种01取值，使得最后的结果是1。而2-sat问题就是每一个由or连接的子式都只包含两个变量，比如这样(x1 or x2) and (not x3 or x1)，2-sat问题是有多项式解法的，而3-sat就是npc问题了，前段时间有人宣称证明了p=np就是因为他自己找到了3-sat的多项式解法，当然最后被证明解法是错误的。。。那么对于2-sat问题解法而言，经典的就是利用强连通分支的算法来解决，最近上的coursera上的algo2有个随机算法也很有趣这里我们也要讲一下。

先来看经典的利用强连通分支的图论解法。我们把每个变量x都拆成2个点，两个点x和~x分别表示这个点取1和这个点取0，所以最后我们就是在这2n个点中选择满足要求的n个点。对于每个子式，假设子式是(x1 or x2)，对于2-sat问题而言我们需要每个子式都得1，也就是对于这个子式而言，x1和x2至少要取一个，对应于图中就是，如果我们取~x1就必须取x2，取~x2就必须取x1，所以我们就在图中从~x1到x2和从~x2到x1连两条有向边。同样的如果子式中有not也是类似方法，比如(not x1 or x2)那么就是X1到x2和~x2到~x1两条有向边。一开始的图片构成的图表示的这个式子。

(x0∨x2)∧(x0∨¬x3)∧(x1∨¬x3)∧(x1∨¬x4)∧(x2∨¬x4)∧(x0∨¬x5)
∧(x1∨¬x5)∧(x2∨¬x5)∧(x3∨x6)∧(x4∨x6)∧(x5∨x6)

构建好图之后对图求强连通分支，很显然的如果xi和~xi在同一个强连通分支中那么就是不存在解的。之后进行染色判定，强连通分支缩点之后，把所有的边反向，然后按照拓扑排序的顺序遍历节点，如果节点没有被染色，就涂成红色，然后把和这个点互斥的点（所谓互斥的点就是如果x和~x所在的点），以及这个点的子孙都涂成蓝色，这样取出红色的点就是满足条件的解。这里就不证明了，详细的可以看伍昱的《由对称性解2-SAT问题》和赵爽的《2-SAT解法浅析》两篇。看证明的时候注意对称性，就是说如果x，y在同一个连通分支，那么~x，~y也在同一个连通分支，如果x到y有路，那么~y到~x也有路，注意这个对称性的特点的话，那两篇文章里的证明也就不难看懂了。

talk is easy，show me the code，那么让我们看一下代码吧，这里就用poj 3648来举例。

  #include <cstdio> 
 #include <cstring> 
 const  int maxn = 10010; 
 int n, m, nxt [maxn ], head [maxn ], pnt [maxn ], ne, e, a, b, a0, b0; 
 char c1, c2; 
 int nnxt [maxn ], nhead [maxn ], npnt [maxn ]; 
 int order [maxn ], norder, id [maxn ], v [maxn ]; 
 int ans [maxn ], op [maxn ]; 
 void dfs ( int d ) { 
v [d ]  =  1; 
for ( int i =head [d ]; i != -1; i =nxt [i ] ) 
if ( !v [pnt [i ] ] ) 
dfs (pnt [i ] ); 
order [norder ++ ]  = d; 
 } 
 void ndfs ( int d,  int k ) { 
v [d ]  =  1; 
id [d ]  = k; 
for ( int i =nhead [d ]; i != -1; i =nnxt [i ] ) 
if ( !v [npnt [i ] ] ) 
ndfs (npnt [i ], k ); 
 } 
 void addedge ( int s,  int t ) { 
pnt [e ]  = t; nxt [e ]  = head [s ]; head [s ]  = e ++; 
 } 
 void addnedge ( int t,  int s ) { 
npnt [ne ]  = s; nnxt [ne ]  = nhead [t ]; nhead [t ]  = ne ++; 
 } 
 void color ( int d ) { 
ans [d ]  =  2; 
for ( int i =head [d ]; i != -1; i =nxt [i ] ) 
if ( !ans [pnt [i ] ] ) 
color (pnt [i ] ); 
 } 
 int main ( ) { 
while ( 1 ) { 
norder  = e  = ne  =  0; 
memset (head,  -1,  sizeof head ); 
memset (nhead,  -1,  sizeof nhead ); 
scanf ( "%d%d",  &n,  &m ); 
if ( !n &&!m ) 
break; 
for ( int i = 0; i<m;  ++i ) { 
scanf ( "%d%c%d%c",  &a,  &c1,  &b,  &c2 ); 
if (c1 == 'h' ) 
a0  = n +a; 
else { 
a0  = a; 
a  += n; 
} 
if (c2 == 'h' ) 
b0  = n +b; 
else { 
b0  = b; 
b  += n; 
} 
addedge (a0, b ); 
addnedge (b, a0 ); 
addedge (b0, a ); 
addnedge (a, b0 ); 
} 
addedge ( 0, n ); 
addnedge (n,  0 ); 
memset (v,  0,  sizeof v ); 
for ( int i = 0; i< 2 *n;  ++i ) 
if ( !v [i ] ) 
dfs (i ); 
int k = 0; 
memset (v,  0,  sizeof v ); 
memset (id,  -1,  sizeof id ); 
for ( int i =norder -1; i> = 0;  --i ) 
if ( !v [order [i ] ] ) 
ndfs (order [i ], k ++ ); 
int mark  =  1; 
for ( int i = 0; i<n;  ++i ) 
if (id [i ] ==id [i +n ] ) 
mark  =  0; 
if ( !mark ) { 
printf ( "bad luck\n" ); 
continue; 
} 
for ( int i = 0; i<n;  ++i ) { 
op [id [i ] ]  = id [i +n ]; 
op [id [i +n ] ]  = id [i ]; 
} 
e  = norder  =  0; 
memset (head,  -1,  sizeof head ); 
memset (v,  0,  sizeof v ); 
memset (ans,  0,  sizeof ans ); 
for ( int i = 0; i<n;  ++i ) 
for ( int j =nhead [i ]; j != -1; j =nnxt [j ] ) 
addedge (id [i ], id [npnt [j ] ] ); 
for ( int i = 0; i<k;  ++i ) 
if ( !v [i ] ) 
dfs (i ); 
for ( int i =norder -1; i> = 0;  --i ) 
if ( !ans [order [i ] ] ) { 
ans [order [i ] ]  =  1; 
color (op [order [i ] ] ); 
} 
for ( int i = 1; i<n;  ++i ) { 
if (ans [id [i ] ]  ==  1 ) 
printf ( "%dh", i ); 
else 
printf ( "%dw", i ); 
if (i<n -1 ) 
printf ( " " ); 
else 
printf ( "\n" ); 
} 
} 
return  0; 
 } 
 

代码自我感觉还是比较清晰的就不解释了，整个过程就是按照上面说的算法进行的。ok，到这里而言acmer的内容已经足够了，下面我们来说说algo2里提到的随机算法。

在讲随机算法之前，首先要介绍“random walks on a line”，假设我们在数轴的点0的位置，在点0的话，下一个时刻我们会移动到点1上，如果在其他的点x，我们有50%的概率下一个时刻移动到点x-1上，有50%的概率移动到x+1上。现在让我们来算一下，从点0开始移动到点n，期望需要移动多少步。这个期望的算法和之前写的这篇的方法差不多。设E(i)是从点i(i<=n)移动到点n所需要的期望的步数。于是我们有

E(n)=0
E(0)=E(1)+1
E(i)=0.5∗(1+E(i+1))+0.5∗(1+E(i−1))

有上面的式子我们可以得到最后的结果，推导比较简单，就不赘述了

E(0)=n2

设Tn表示从0走到n的步数，于是我们有

n2=E(Tn)=∑2n2k=0(k∗P(Tn=k))+∑∞k=2n2+1(k∗P(Tn=k))
因为 ∑2n2k=0(k∗P(Tn=k))≥0
所以 n2≥∑∞k=2n2+1(k∗P(Tn=k))
≥∑∞k=2n2+1((2n2)∗P(Tn=k))
=2n2∗P(Tn>2n2)

于是我们得到

P(Tn>2n2)≤12

也就是说我们从0开始走2*n*n步，我们有大于1/2的概率已经经过n这个点了。

ok回到我们的2-sat问题。

我们的算法是这样的，我们开始时随机给变量赋值0或者1，然后迭代足够多的次数（大于2*n*n的次数），如果某次迭代，我们找到了答案就可以返回结果了，如果我们迭代足够多的次数都没找到答案就返回无解。每次迭代，我们找一个不满足要求的子式，然后两个变量随机挑一个改变他的值。

假设我们现在的解是a，满足要求的解是a*，那么我们的解和满足要求的解，值不同的变量的个数是x，某次迭代，我们找到一个子式(xi or xj)不满足条件，因为子式不满足条件，所以xi和xj不可能同时和a*里值是相同的，如果两个值都不同，那么我们这次改动使得x=x-1，如果有一个值不同，那么我们有50%的概率使得x=x-1有50%的概率使得x=x+1，所以，答案变好的概率要大于50%，所以迭代2*n*n次能得到解的概率就会小于1/2。

很有趣的算法，并且我们用这个算法，可以AC掉poj 3648这道题！看代码

  #include <cstdio> 
 #include <cstdlib> 
 #include <cstring> 
 #include <ctime> 
 const  int maxn = 10010; 
 int n, m, a, b; 
 char c1, c2; 
 int ans [maxn ], record [maxn ] [ 2 ]; 
 int get ( int x ) { 
if (x<n ) 
return ans [x ]; 
return  !ans [x -n ]; 
 } 
 int main ( ) { 
//srand(time(NULL));这里如果调用time，poj会报 runtime error的错误 
srand ( 7 ); 
while ( 1 ) { 
scanf ( "%d%d",  &n,  &m ); 
memset (ans,  0,  sizeof ans ); 
if ( !n &&!m ) 
break; 
for ( int i = 0; i<m;  ++i ) { 
scanf ( "%d%c%d%c",  &a,  &c1,  &b,  &c2 ); 
if (c1 == 'w' ) 
a  += n; 
if (c2 == 'w' ) 
b  += n; 
record [i ] [ 0 ]  = a; 
record [i ] [ 1 ]  = b; 
} 
int mark  =  0; 
for ( int i = 0; i< 5 *n *n;  ++i ) { 
mark  =  1; 
for ( int j = 0; j<m;  ++j ) 
if ( (record [j ] [ 0 ] %n !=record [j ] [ 1 ] %n ) &&! (get (record [j ] [ 0 ] )||get (record [j ] [ 1 ] ) ) ) { 
int tmp  = rand ( ) % 2; 
if (record [j ] [ 0 ] %n == 0 ) 
tmp  =  1; 
if (record [j ] [ 1 ] %n == 0 ) 
tmp  =  0; 
ans [record [j ] [tmp ] %n ]  =  1 -ans [record [j ] [tmp ] %n ]; 
mark  =  0; 
break; 
} 
if (mark ) 
break; 
} 
if ( !mark ) { 
printf ( "bad luck\n" ); 
continue; 
} 
for ( int i = 1; i<n;  ++i ) { 
if (ans [i ] ) 
printf ( "%dh", i ); 
else 
printf ( "%dw", i ); 
if (i<n -1 ) 
printf ( " " ); 
else 
printf ( "\n" ); 
} 
} 
return  0; 
 } 
 

记得之前gcj曾经有道题目需要用到生日悖论来解决，感觉和这个随机算法都是很有趣的算法阿。

hdu3062 Party(2-SAT入门)

分类： 2-SAT 图论 2013-07-21 10:25 44人阅读评论(0) 收藏举报

2-SAT 图论

Party

Time Limit: 2000/1000 MS (Java/Others) Memory Limit: 32768/32768 K (Java/Others)
Total Submission(s): 3149 Accepted Submission(s): 991

Problem Description

有n对夫妻被邀请参加一个聚会，因为场地的问题，每对夫妻中只有1人可以列席。在2n 个人中，某些人之间有着很大的矛盾（当然夫妻之间是没有矛盾的），有矛盾的2个人是不会同时出现在聚会上的。有没有可能会有n 个人同时列席？

Input

n：表示有n对夫妻被邀请 (n<= 1000)
m：表示有m 对矛盾关系 ( m < (n - 1) * (n -1))

在接下来的m行中，每行会有4个数字，分别是 A1,A2,C1,C2
A1,A2分别表示是夫妻的编号
C1,C2 表示是妻子还是丈夫，0表示妻子，1是丈夫
夫妻编号从 0 到 n -1

Output

如果存在一种情况则输出YES
否则输出 NO

Sample Input

      2 
1
0 1 1 1

Sample Output

YES

Source

2009 Multi-University Training Contest 16 - Host by NIT

题目大意：中文题，不解释。

题目分析：2-sat入门题。

2-SAT就是2判定性问题，是一种特殊的逻辑判定问题。

求解过程：

1．构图
2．求图的极大强连通子图
3．把每个子图收缩成单个节点，根据原图关系构造一个有向无环图
4．判断是否有解，无解则输出（退出）
5．对新图进行拓扑排序
6．自底向上进行选择、删除
7．输出

这题只需要判断是否有解，强连通用Gabow算法。

详情请见代码：

[cpp] view plain copy print ?

#include <iostream>
#include<cstdio>
#include<cstring>
using namespace std;
const int N = 2005;
const int M = 2000000;
int head[N];
struct edge
{
int to,next;
}g[M];
bool flag;
int stack1[N];
int stack2[N];
int vis[N];
int scc[N];
int n,m;
void build(int s,int t,int num)
{
g[num].to = t;
g[num].next = head[s];
head[s] = num;
}
void dfs(int cur,int &sig,int &num)
{
if(!flag)
return;
vis[cur] = ++sig;
stack1[++stack1[0]] = cur;
stack2[++stack2[0]] = cur;
for(int i = head[cur];i != -1;i = g[i].next)
{
if(!vis[g[i].to])
dfs(g[i].to,sig,num);
else
{
if(scc[g[i].to] == 0)
{
while(vis[stack2[stack2[0]]] > vis[g[i].to])
stack2[0] --;
}
}
}
if(stack2[stack2[0]] == cur)
{
++ num;
stack2[0] --;
do
{
scc[stack1[stack1[0]]] = num;
int tmp = stack1[stack1[0]];
if(tmp > n)
{
if(scc[tmp - n] && scc[tmp - n] == num)
{
flag = false;
return;
}
}
else
{
if(scc[tmp + n] && scc[tmp + n] == num)
{
flag = false;
return;
}
}
}while(stack1[stack1[0] --] != cur);
}
}
void Gabow()
{
int i,sig,num;
memset(vis,0,sizeof(vis));
memset(scc,0,sizeof(scc));
stack1[0] = stack2[0] = sig = num = 0;
for(i = 1;i <= n + n && flag;i ++)
if(!vis[i])
dfs(i,sig,num);
}
int nextint()
{
char c;
int ret;
while((c = getchar()) > '9' || c < '0')
;
ret = c - '0';
while((c = getchar()) >= '0' && c <= '9')
ret = ret * 10 + c - '0';
return ret;
}
int main()
{
int i,j,a,b,c,d;
while(scanf("%d",&n) != EOF)
{
//scanf("%d",&m);
m = nextint();
memset(head,-1,sizeof(head));
for(i = 1;i <= m + m;i += 2)//每对矛盾建两条边
{
a = nextint();
b = nextint();
c = nextint();
d = nextint();
//scanf("%d%d%d%d",&a,&b,&c,&d);//1-n husband n + 1 - 2n wife
a ++;
b ++;
switch(c + d)
{
case 0:build(a + n,b,i);build(b + n,a,i + 1);break;//a+n b+n 矛盾
case 1:if(c)//a b + n矛盾
{
build(a,b,i);build(b + n,a + n,i + 1);
}
else//a + n b矛盾
{
build(a + n,b + n,i);build(b,a,i + 1);
}break;
case 2:build(a,b + n,i);build(b,a + n,i + 1);break;
}
}
flag = true;
Gabow();
if(flag)
printf("YES\n");
else
printf("NO\n");
}
return 0;
}
//93MS 808K

  hdu4115 Eliminate the Conflict(3SAT->2SAT) 
 
  分类：  2-SAT  图论  2013-07-24 10:05  63人阅读 评论(0) 收藏 举报 
  图论

 
  Eliminate the Conflict
 Time Limit: 2000/1000 MS (Java/Others) Memory Limit: 32768/32768 K (Java/Others)Total Submission(s): 982 Accepted Submission(s): 410
 
 Problem Description 
 Conflicts are everywhere in the world, from the young to the elderly, from families to countries. Conflicts cause quarrels, fights or even wars. How wonderful the world will be if all conflicts can be eliminated.Edward contributes his lifetime to invent a 'Conflict Resolution Terminal' and he has finally succeeded. This magic item has the ability to eliminate all the conflicts. It works like this:If any two people have conflict, they should simply put their hands into the 'Conflict Resolution Terminal' (which is simply a plastic tube). Then they play 'Rock, Paper and Scissors' in it. After they have decided what they will play, the tube should be opened and no one will have the chance to change. Finally, the winner have the right to rule and the loser should obey it. Conflict Eliminated!But the game is not that fair, because people may be following some patterns when they play, and if the pattern is founded by others, the others will win definitely.Alice and Bob always have conflicts with each other so they use the 'Conflict Resolution Terminal' a lot. Sadly for Bob, Alice found his pattern and can predict how Bob plays precisely. She is very kind that doesn't want to take advantage of that. So she tells Bob about it and they come up with a new way of eliminate the conflict:They will play the 'Rock, Paper and Scissors' for N round. Bob will set up some restricts on Alice.But the restrict can only be in the form of "you must play the same (or different) on the ith and jth rounds". If Alice loses in any round or break any of the rules she loses, otherwise she wins.Will Alice have a chance to win? 
  
 
 Input 
 The first line contains an integer T(1 <= T <= 50), indicating the number of test cases.Each test case contains several lines.The first line contains two integers N,M(1 <= N <= 10000, 1 <= M <= 10000), representing how many round they will play and how many restricts are there for Alice.The next line contains N integers B ₁,B ₂, ...,B _N, where B _i represents what item Bob will play in the i ^th round. 1 represents Rock, 2 represents Paper, 3 represents Scissors.The following M lines each contains three integers A,B,K(1 <= A,B <= N,K = 0 or 1) represent a restrict for Alice. If K equals 0, Alice must play the same on A ^th and B ^th round. If K equals 1, she must play different items on Ath and Bthround. 
  
 
 Output 
 For each test case in the input, print one line: "Case #X: Y", where X is the test case number (starting with 1) and Y is "yes" or "no" represents whether Alice has a chance to win. 
  
 
 Sample Input 
         2
3 3
1 1 1
1 2 1
1 3 1
2 3 1
5 5
1 2 3 2 1
1 2 1
1 3 1
1 4 1
1 5 1
2 3 0
 
  
 
 Sample Output 
         Case #1: no
Case #2: yesHint
'Rock, Paper and Scissors' is a game which played by two person. They should play Rock, Paper or Scissors by their hands at the same time. 
Rock defeats scissors, scissors defeats paper and paper defeats rock. If two people play the same item, the game is tied..
 
 
  
 
 Source 
  2011 Asia ChengDu Regional Contest 
 
 
 题目大意：ACM两位神牛Alice和Bob又来玩游戏了，这次他们玩石头剪刀布。规定石头、布、剪刀分别用1、2、3表示。他们准备玩n局，现在Alice已知Bob的n局的出法，但是为了公平，对于Alice，Bob给了m个限制，每个限制3个参数：a b k。k=0或1。当k = 0的时候，表示第a局和第j局Alice必须出相同的手势，k= 1表示Alice在第a局和第j局必须出不同的手势。如果n轮比完，Alice一局没输的话，Alice赢，否则Bob赢。求Alice是否有赢的可能。
 题目分析：因为每一轮有3种手势，乍一看是3-sat问题。但因为对于Alice来说，一局也不能输，所以只要n局保持不败就可以了，所以对于Alice来说，每一局其实只有2种情况，于是利用这个条件可以将此3-sat问题转化为2-sat问题。
 先来看一张表：
 Bob Alice
 平 赢
 1 1 2
 2 2 3
 3 3 1
 一共就这6种情况。可以看出，无论Bob第a局和第b局出什么，Alice要保持不败，至少有一种手势可以在第a局和第b局同时做。所以我们先根据Bob第i局的手势，找出Alice第i局保持不败的2种手势，然后开始建图。
 如果第a局和第b局Alice的手势要不同，那么矛盾的情况是Alice第a局和第b局手势相同，那么枚举这4种情况，找到矛盾的点对，建边，如果ab矛盾，建a->b',b->a'。
 如果第a局和第b局Alice的手势要相同，那么矛盾的情况是Alice第a局和第b局手势不同，根据分析可知，无论第a局和第b局Bob出什么手势，Alice在这两局保持不败的策略中至少有一对是相同的，先考虑2对都相同的，即Bob在第a局和第b局手势相同，那么直接建边a->b,b->a,a + n->b + n,b + n->a + n(假设ab同，a+n b+n同)，一共4条边。如果没有2对相同，那么至少一对相同，依次枚举，找到那对相同的，只有这对相同的合理，其他的都不合理，那么仿照经典的And和Or操作中的建图，假设ab相同，那么只有ab是合法的，所以直接建a+n->a,b+n->b。
 详情请见代码：
 
    [cpp] view plain copy print ? 
 
 #include <iostream> 
#include<cstdio> 
#include<cstring> 
using namespace std; 
const int N = 10001; 
const int M = 10001; 
struct edge 
{ 
int to,next; 
}g[M<<1]; 
int head[N<<1]; 
int scc[N<<1]; 
int vis[N<<1]; 
int stack1[N<<1]; 
int stack2[N<<1]; 
int n,m,num; 
int lcm[N][2]; 
bool flag; 
void init() 
{ 
memset(head,-1,sizeof(head)); 
memset(vis,0,sizeof(vis)); 
memset(scc,0,sizeof(scc)); 
stack1[0] = stack2[0] = num = 0; 
flag = true; 
} 
void build(int s,int e) 
{ 
g[num].to = e; 
g[num].next = head[s]; 
head[s] = num ++; 
} 
void dfs(int cur,int &sig,int &cnt) 
{ 
if(!flag) 
return; 
vis[cur] = ++sig; 
stack1[++stack1[0]] = cur; 
stack2[++stack2[0]] = cur; 
for(int i = head[cur];~i;i = g[i].next) 
{ 
if(!vis[g[i].to]) 
dfs(g[i].to,sig,cnt); 
else 
{ 
if(!scc[g[i].to]) 
{ 
while(vis[stack2[stack2[0]]] > vis[g[i].to]) 
stack2[0] --; 
} 
} 
} 
if(stack2[stack2[0]] == cur) 
{ 
stack2[0] --; 
cnt ++; 
do 
{ 
scc[stack1[stack1[0]]] = cnt; 
int tmp = stack1[stack1[0]]; 
if((tmp > n && scc[tmp - n] == cnt) || (tmp <= n && scc[tmp + n] == cnt)) 
{ 
flag = false; 
return; 
} 
}while(stack1[stack1[0] --] != cur); 
} 
} 
void Gabow() 
{ 
int i,sig,cnt; 
sig = cnt = 0; 
for(i = 1;i <= n + n && flag;i ++) 
if(!vis[i]) 
dfs(i,sig,cnt); 
} 
int nextint() 
{ 
char c; 
int ret; 
while((c = getchar()) > '9' || c < '0') 
; 
ret = c - '0'; 
while((c = getchar()) >=  '0' && c <= '9') 
ret = ret * 10 + c - '0'; 
return ret; 
} 
int main() 
{ 
int i,j,T,t,a,b; 
scanf("%d",&T); 
int cas = 0; 
while(T --) 
{ 
scanf("%d%d",&n,&m); 
for(i = 1;i <= n;i ++) 
{ 
scanf("%d",&t); 
lcm[i][0] = t;//tie 
lcm[i][1] = t + 1;//win 
if(lcm[i][1] > 3) 
lcm[i][1] = 1; 
if(lcm[i][0] > lcm[i][1]) 
lcm[i][0] ^= lcm[i][1] ^= lcm[i][0] ^= lcm[i][1]; 
} 
init(); 
while(m --) 
{ 
scanf("%d%d%d",&a,&b,&t); 
if(t)//different 
{//建图小心 找矛盾 
if(lcm[a][0] == lcm[b][0]) 
{ 
build(a,b + n); 
build(b,a + n); 
} 
if(lcm[a][0] == lcm[b][1]) 
{ 
build(a,b); 
build(b + n,a + n); 
} 
if(lcm[a][1] == lcm[b][0]) 
{ 
build(a + n,b + n); 
build(b,a); 
} 
if(lcm[a][1] == lcm[b][1]) 
{ 
build(a + n,b); 
build(b + n,a); 
} 
} 
else//same  
{ 
if(lcm[a][0] == lcm[b][0] && lcm[a][1] == lcm[b][1]) 
{ 
build(a,b); 
build(b,a); 
build(a + n,b + n); 
build(b + n,a + n); 
} 
else 
{//必有一对相同的，只能选这一对 
if(lcm[a][0] == lcm[b][0]) 
{ 
build(a + n,a); 
build(b + n,b); 
} 
if(lcm[a][0] == lcm[b][1]) 
{ 
build(a + n,a); 
build(b,b + n); 
} 
if(lcm[a][1] == lcm[b][0]) 
{ 
build(a,a + n); 
build(b + n,b); 
} 
if(lcm[a][1] == lcm[b][1]) 
{ 
build(a,a + n); 
build(b,b + n); 
} 
} 
} 
} 
Gabow(); 
printf("Case #%d: ",++cas); 
if(flag) 
printf("yes\n"); 
else 
printf("no\n"); 
} 
return 0; 
} 
//0MS 556K