POJ 3678 2-SAT

题目链接

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.

题意

n个点,m个关系,每个关系给a,b,c三个数字，和一个字符串(or,and,xor)表示
a opt b == c,然后问你是否有一种取值满足所有关系

思路

2-SAT,xi 表示变量i取0, xi+n表示i取1.把关系变成有向图，如果i, i + n在同一强连通分量中那么显然关系错误。

#include <cstdio>
#include <cstring>
#include <algorithm>
#include <iostream>
#include <stack>using namespace std;
const int MAXN = 2e3 + 7;
const int MAXM = 2e6 + 7;struct Node {int to, w, next;
} edge[MAXM * 2];int first[MAXN], sign, dfn[MAXN], low[MAXN], ins[MAXN], n, m, idx, tot, color[MAXN];stack<int>st;inline void init() {memset(first, -1, sizeof(first));memset(dfn, 0, sizeof(dfn));memset(low, 0, sizeof(low));memset(ins, 0, sizeof(ins));memset(color, 0, sizeof(color));sign = idx = tot = 0;while(!st.empty()) {st.pop();}
}inline void add_edge(int u, int v, int w) {edge[sign].to = v;edge[sign].w = w;edge[sign].next = first[u];first[u] = sign++;
}void tarjan(int x) {low[x] = dfn[x] = ++idx;st.push(x), ins[x] = 1;for(int i = first[x]; ~i; i = edge[i].next) {int to = edge[i].to;if(!dfn[to]) {tarjan(to);low[x] = min(low[x], low[to]);} else if(ins[to]) {low[x] = min(low[x], dfn[to]);}}int top;if(dfn[x] == low[x]) {tot++;do {top = st.top();st.pop();ins[top] = 0;color[top] = tot;} while(top != x);}
}void TwoSAT() {for(int i = 1; i <= n; i++ ) {if(!dfn[i]) {tarjan(i);}}bool ok = 1;for(int i = 1; i <= n; i++ ) {if(color[i] == color[i + n]) {ok = 0;break;}}puts(ok ? "YES" : "NO");
}int main() {int a, b, c;char opt[15];while(~scanf("%d %d", &n, &m)) {init();for(int i = 1; i <= m; i++ ) {scanf("%d %d %d %s", &a, &b, &c, opt);a++, b++;if(opt[0] == 'A') {if(c == 1) { /// A and B == 1;add_edge(a, a + n, 1), add_edge(b, b + n, 1);add_edge(a + n, b + n, 1), add_edge(b + n, a + n, 1);} else {     /// A and B == 0;add_edge(a + n, b, 1);add_edge(b + n, a, 1);}} else if(opt[0] == 'O') {if(c == 1) { /// A or B == 1;add_edge(a, b + n, 1), add_edge(b, a + n, 1);} else {     /// A or B == 0;add_edge(a, b, 1), add_edge(b, a, 1);add_edge(a + n, a, 1), add_edge(b + n, b, 1);}} else if(opt[0] == 'X') {if(c == 1) { /// A xor B == 1;add_edge(a, b + n, 1), add_edge(b, a + n, 1);add_edge(a + n, b, 1), add_edge(b + n, a, 1);} else {     /// A xor B == 0;add_edge(a, b, 1), add_edge(b, a, 1);add_edge(a + n, b + n, 1), add_edge(b + n, a + n, 1);}}}TwoSAT();}return 0;
}