2-SAT

#include <cstdio>
#include <cstring>
#include <algorithm>
#include <vector>
using namespace std;

const int N=10010;
struct TwoSAT{
int n;
vector<int> G[N*2];
bool flag[N*2];
int S[N*2],top;
bool dfs(int x){
if(flag[x^1]) return false;
if(flag[x]) return true;
flag[x]=true;
S[top++]=x;
int sz=G[x].size();
for(int i=0;i<sz;i++)
if(!dfs(G[x][i])) return false;
return true;
}
void init(int tn){
n=tn;
for(int i=0;i<n*2;i++) G[i].clear();
memset(flag,0,sizeof(flag));
}
void addClause(int x,int xval,int y,int yval){
x=x*2+xval;
y=y*2+yval;
G[x].push_back(y^1);
G[y].push_back(x^1);
}
bool solve(){
for(int i=0;i<n*2;i+=2){
if(!flag[i] && !flag[i+1]){
top=0;
if(!dfs(i)){
while(top>0) flag[S[--top]]=false;
if(!dfs(i+1)) return false;
}
}
}
return true;
}
};

TwoSAT s;
int b
[2];
int main(){
int T,C=0;
scanf("%d",&T);
int n,m;
while(T--){
scanf("%d%d",&n,&m);
s.init(n);
for(int i=0;i<n;i++){
int t;
scanf("%d",&t);
t--;
b[i][0]=(t+1)%3;
b[i][1]=(t+2)%3;
}
for(int i=0;i<m;i++){
int x,y,k;
scanf("%d%d%d",&x,&y,&k);
x--; y--;
if(k==0){
if(b[x][0]!=b[y][0]) s.addClause(x,0,y,0);
if(b[x][0]!=b[y][1]) s.addClause(x,0,y,1);
if(b[x][1]!=b[y][0]) s.addClause(x,1,y,0);
if(b[x][1]!=b[y][1]) s.addClause(x,1,y,1);
} else{
if(b[x][0]==b[y][0]) s.addClause(x,0,y,0);
if(b[x][0]==b[y][1]) s.addClause(x,0,y,1);
if(b[x][1]==b[y][0]) s.addClause(x,1,y,0);
if(b[x][1]==b[y][1]) s.addClause(x,1,y,1);
}
}
printf("Case #%d: ",++C);
if(s.solve()) printf("yes\n");
else printf("no\n");
}
return 0;
}