POJ 3678 Katu Puzzle(2-SAT,合取范式大集合)

时间:2023-03-09 09:00:54
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(VE) 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 ≤ X≤ 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 (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.

题目链接: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;
}