poj3678 Katu Puzzle 2-SAT

时间:2023-03-09 18:40:01
poj3678 Katu Puzzle 2-SAT

Katu Puzzle

Time Limit: 1000MS   Memory Limit: 65536K
Total Submissions: 6714   Accepted: 2472

Description

Katu Puzzle is presented as a directed graph G(V, E) with each edge e(a, b) labeled by a boolean operator op (one of AND, OR, XOR) and an integer c (0 ≤ c ≤ 1). One Katu is solvable if one can find each vertex Vi a value Xi (0 ≤ Xi ≤ 1) such that for each edge e(a, b) labeled by op and c, the following formula holds:

Xa op Xb = c

The calculating rules are:

AND 0 1
0 0 0
1 0 1
OR 0 1
0 0 1
1 1 1
XOR 0 1
0 0 1
1 1 0

Given a Katu Puzzle, your task is to determine whether it is solvable.

Input

The first line contains two integers N (1 ≤ N ≤ 1000) and M,(0 ≤ M ≤ 1,000,000) indicating the number of vertices and edges.
The following M lines contain three integers a (0 ≤ a < N), b(0 ≤ b < N), c and an operator op each, describing the edges.

Output

Output a line containing "YES" or "NO".

Sample Input

4 4
0 1 1 AND
1 2 1 OR
3 2 0 AND
3 0 0 XOR

Sample Output

YES

Hint

X0 = 1, X1 = 1, X2 = 0, X3 = 1.

Source

先进性tarjan算法找出强连通分量,判断每个点的取值是否矛盾,矛盾即为对于题意中每个点的0,1是否存在于一个强连通分量中,矛盾输出NO,不矛盾输出1;
建图规则:
a & b = 1 等价于 !a->a, !b->b;(旨在使得a或b取值为0是产生矛盾)
a & b = 0 等价于 a->!b, b->!a;
a | b = 1  等价于 !a->b, !b->a;
a | b = 0  等价于 a->!a, b->!b;
a ^ b = 1 等价于 !a->b, !b->a, a->!b, b->!a;
a ^ b = 0 等价于 a->b, b->a, !a->!b, !b->!a;  
#include <iostream>
#include <cstdio>
#include <cstring>
using namespace std;
const int MAX = 1005 * 2;
int n,m;
int head[MAX];
struct node {
int t,next;
}edge[4000000];
int cnt;
void add(int u, int v) {
edge[cnt].t = v;
edge[cnt].next = head[u];
head[u] = cnt++;
}
int bfn[MAX];
int low[MAX];
int vis[MAX];
int s[MAX];
int sn;
void tarbfs(int u, int lay, int & scc_num) {
vis[u] = 1;
bfn[u] = low[u] = lay;
s[sn++] = u;
int i;
for (i = head[u]; i != -1; i = edge[i].next) {
int tmp = edge[i].t;
if (!vis[tmp])tarbfs(tmp, ++lay, scc_num);
if (vis[tmp] == 1)low[u] = min(low[u], low[tmp]);
}
if (low[u] == bfn[u]) {
scc_num++;
while (1) {
sn--;
vis[s[sn]] = 2;
low[s[sn]] = scc_num;
if (s[sn] == u)break;
}
}
}
int tarjan() {
int scc_num = 0;
int lay = 1;
int i;
sn = 0;
memset(vis, 0, sizeof(vis));
for (i = 0; i < n; i++) {
if (!vis[i])
tarbfs(i, lay, scc_num);
}
return scc_num;
} int main() {
// freopen("in.txt","r",stdin);
int a,b,c;
char ch[5];
int i;
while (scanf("%d %d",&n,&m) != EOF) {
memset(head, -1, sizeof(head));
n = 2 * n;
cnt = 0;
for (i = 0; i < m; i++) {
scanf("%d %d %d %s",&a,&b,&c,ch);
if (ch[0] == 'A') {
if (c == 1) {
add(a<<1, a<<1|1);
add(b<<1, b<<1|1);
} else {
add(a<<1|1, b<<1);
add(b<<1|1, a<<1);
}
} else if (ch[0] == 'O') {
if (c == 1) {
add(a<<1, b<<1|1);
add(b<<1, a<<1|1);
} else {
add(a<<1|1, a<<1);
add(b<<1|1, b<<1);
}
} else {
if (c == 1) {
add(a<<1|1, b<<1);
add(b<<1|1, a<<1);
add(a<<1, b<<1|1);
add(b<<1, a<<1|1);
} else {
add(a<<1|1, b<<1|1);
add(b<<1|1, a<<1|1);
add(a<<1, b<<1);
add(b<<1, a<<1);
}
}
}
tarjan();
int flag = 0;
for (i = 0; i < n / 2; i++) {
if (low[i<<1] == low[i<<1|1]) {
flag = 1;
break;
}
}
if (flag)
printf("NO\n");
else
printf("YES\n");
}
return 0;
}