POJ 3678 Katu Puzzle（2-SAT，合取范式大集合）

Katu Puzzle

Time Limit: 1000MS		Memory Limit: 65536K
Total Submissions: 9987		Accepted: 3741

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 V_i a value X_i (0 ≤ X_i ≤ 1) such that for each edge e(a, b) labeled by op and c, the following formula holds:

 X_a op X_b = 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

X₀ = 1, X₁ = 1, X₂ = 0, X₃ = 1.

题目链接：POJ 3678

一开始不知道c是干嘛的，看了题解发现原来意思是 a op b = c，那这就很简单了，分3*2*2种情况讨论，因为每一种情况还要判断a是否等于b，如果等于的话加的边会不一样，甚至像$a xor a = 0$这种东西显然不存在的，可以直接判断NO了。其余的式子自己用化简成合取范式就OK。当然另外有一些时候化出来像$a lor lnot a=1$的，那直接就是1可以去掉不用考虑。

嗯做完这题基本可以告别2-SAT了，快做吐了……

代码：

#include <stdio.h>
#include <iostream>
#include <algorithm>
#include <cstdlib>
#include <sstream>
#include <numeric>
#include <cstring>
#include <bitset>
#include <string>
#include <deque>
#include <stack>
#include <cmath>
#include <queue>
#include <set>
#include <map>
using namespace std;
#define INF 0x3f3f3f3f
#define LC(x) (x<<1)
#define RC(x) ((x<<1)+1)
#define MID(x,y) ((x+y)>>1)
#define fin(name) freopen(name,"r",stdin)
#define fout(name) freopen(name,"w",stdout)
#define CLR(arr,val) memset(arr,val,sizeof(arr))
#define FAST_IO ios::sync_with_stdio(false);cin.tie(0);
typedef pair<int, int> pii;
typedef long long LL;
const double PI = acos(-1.0);
const int N = 2010;
const int M = 1000010 << 2;
struct edge
{
	int to, nxt;
	edge() {}
	edge(int _to, int _nxt): to(_to), nxt(_nxt) {}
};
edge E[M];
int head[N], tot;
int dfn[N], low[N], st[N], belong[N], sc, ts, top;
bitset<N>ins;
int n, m;

void init()
{
	CLR(head, -1);
	CLR(low, 0);
	CLR(st, 0);
	CLR(belong, 0);
	sc = ts = top = 0;
	ins.reset();
}
inline int rev(const int &k)
{
	return k < n ? k + n : k - n;
}
inline void add(int s, int t)
{
	E[tot] = edge(t, head[s]);
	head[s] = tot++;
}
void scc(int u)
{
	dfn[u] = low[u] = ++ts;
	ins[u] = 1;
	st[top++] = u;
	int i, v;
	for (i = head[u]; ~i; i = E[i].nxt)
	{
		v = E[i].to;
		if (!dfn[v])
		{
			scc(v);
			low[u] = min(low[u], low[v]);
		}
		else if (ins[v])
			low[u] = min(low[u], dfn[v]);
	}
	if (low[u] == dfn[u])
	{
		++sc;
		do
		{
			v = st[--top];
			ins[v] = 0;
			belong[v] = sc;
		} while (u != v);
	}
}
int check()
{
	for (int i = 0; i < (n << 1); ++i)
		if (!dfn[i])
			scc(i);
	for (int i = 0; i < n; ++i)
		if (belong[i] == belong[i + n])
			return 0;
	return 1;
}
int main(void)
{
	int a, b, c, i;
	char ops[10];
	while (~scanf("%d%d", &n, &m))
	{
		init();
		int flag = 1;
		for (i = 0; i < m; ++i)
		{
			scanf("%d%d%d%s", &a, &b, &c, ops);
			if (ops[0] == 'A')
			{
				if (c)
				{
					add(rev(a), a);
					if (a != b)
						add(rev(b), b);
				}
				else
				{
					if (a == b)
						add(a, rev(a));
					else
					{
						add(a, rev(b));
						add(b, rev(a));
					}
				}
			}
			else if (ops[0] == 'O')
			{
				if (c)
				{
					if (a == b)
					{
						add(rev(a), a);
					}
					else
					{
						add(rev(a), b);
						add(rev(b), a);
					}
				}
				else
				{
					if (a == b)
						add(a, rev(a));
					else
					{
						add(a, rev(a));
						add(b, rev(b));
					}
				}
			}
			else if (ops[0] == 'X')
			{
				if (c)
				{
					if (a == b)
						flag = 0;
					else
					{
						add(rev(a), b);
						add(rev(b), a);
						add(a, rev(b));
						add(b, rev(a));
					}
				}
				else
				{
					if (a == b)
						;
					else
					{
						add(a, b);
						add(rev(b), rev(a));
						add(rev(a), rev(b));
						add(b, a);
					}
				}
			}
		}
		puts((!flag || !check()) ? "NO" : "YES");
	}
	return 0;
}