poj 3678 Katu Puzzle(2-sat)

时间:2022-10-23 09:53:27

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 ( ≤ c ≤ ). One Katu is solvable if one can find each vertex Vi a value Xi ( ≤ Xi ≤ ) 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 ( ≤ N ≤ ) and M,( ≤ M ≤ ,,) indicating the number of vertices and edges.
The following M lines contain three integers a ( ≤ a < N), b( ≤ b < N), c and an operator op each, describing the edges.

Output

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

Sample Input

   AND
OR
AND
XOR

Sample Output

YES

Hint

X0 = , X1 = , X2 = , X3 = .

Source

 
胡乱地搞,竟然就AC了
借用别人的解题报告

思路:因为给出结点 a ,b,值 c,还有判断方式OP,这种一看当然就知道是用2SAT做了。为什么说是深刻理解2SAT呢,因为……2SAT中说过,只有关系确定的才能连边,否则不能连边;还有一个重要的是,如果某个条件必须为某个值时,自身与自身的相反条件也要连边,具体看下面解释:

现在设 2*a为1,2*a+1为0;当然 2*b为1,2*b+1为0:

1.当OP为’And‘时:

(1)当c=1时,那么只有a 与 b同时为1时,a  AND b才等于1,并且有且只有当a与b都为1时这个条件才成立,所以a与b一定要等1,所以连边<2*a+1,2*a>,<2*b+1,2*b>,表示不管怎么样,a与b的情况都等于1,即:当a等于0时a必等于1,b等于0时b必等于1,这个刚开始我看别人的解题报告就是这么说的,然后自己也没太理解,其实真正的内涵就是强制执行a与b都等于1 !(如果a等于1了的话当然这条边就没用了,如果a等于0的话,那么这条连就可以起到把a强制等于1以符合题目条件情况了,就是如此简单,得慢慢理解)

(2)当c=0时,那么当a等于0时,b可能为0也可以为1,所以是不确定关系,由上面说的一定是确定关系才能连边,所以a为0的情况就不能连边了;当a等于1时,b一定为0才能使 a AND b =0,所以连边:<2*a,2*b+1>,当然还有<2*b,2*a,+1>。

2.当OP为OR时,

(1)当c=1时,那么当a=1时,b=1或者b=0,所以当a=1时出现了两种关系,就是不确定了,就不用连边了;当a=0时,那么b一定=1,所以是确定关系,连边:<2*a+1,2*b>,当然还有<2*b+1,2*a>。

(2)当c=0时,那么只有当a=b=0这个关系,所以这个和上面1(1)情况就一样了,上面是强制执行a=b=1的情况,而这里因为只有a=b=0的情况,所以也要强制执行a=b=0,即连边:<2*a,2*a+1>,<2*b,2*b+1>。

3.当OP为XOR时,因为如果a=1,那么b必=0;a=0,b必=1;b=1,a必=0;b=0,a必=1。如此看,这四个关系都是确定的,所以都要连边,但是其实我们可以不连,一条边都不用连,因为出a=1的时候一定不会再出现a=0了,这四条边是不会产生矛盾的,所以强连通缩点后不会出现belong[2*a]=belong[2*a+1]的情况的,所以连了也没用,只是多加了点判断的时间罢了……这在别人的解题报告里说的是形成了组环了,都是一个意思。比如:a=1,b=0与b=0,a=1在tarjan中会形成一个新的结点,也就是自环,所以……在异或这种情况中只能选择a=0或者a=1,所以不会出现矛盾……故不用连边了!

 #pragma comment(linker, "/STACK:1024000000,1024000000")
#include<iostream>
#include<cstdio>
#include<cstring>
#include<cmath>
#include<math.h>
#include<algorithm>
#include<queue>
#include<set>
#include<bitset>
#include<map>
#include<vector>
#include<stdlib.h>
#include <stack>
using namespace std;
#define PI acos(-1.0)
#define max(a,b) (a) > (b) ? (a) : (b)
#define min(a,b) (a) < (b) ? (a) : (b)
#define ll long long
#define eps 1e-10
#define MOD 1000000007
#define N 1006
#define inf 1e12
int n,m;
vector<int> e[N]; int tot;
int head[N];
int vis[N];
int tt;
int scc;
stack<int>s;
int dfn[N],low[N];
int col[N];
struct Node
{
int from;
int to;
int next;
}edge[N*N];
void init()
{
tot=;
scc=;
tt=;
memset(head,-,sizeof(head));
memset(dfn,-,sizeof(dfn));
memset(low,,sizeof(low));
memset(vis,,sizeof(vis));
memset(col,,sizeof(col));
}
void add(int s,int u)//邻接矩阵函数
{
edge[tot].from=s;
edge[tot].to=u;
edge[tot].next=head[s];
head[s]=tot++;
}
void tarjan(int u)//tarjan算法找出图中的所有强连通分支
{
dfn[u] = low[u]= ++tt;
vis[u]=;
s.push(u);
int cnt=;
for(int i=head[u];i!=-;i=edge[i].next)
{
int v=edge[i].to;
if(dfn[v]==-)
{
// sum++;
tarjan(v);
low[u]=min(low[u],low[v]);
}
else if(vis[v]==)
low[u]=min(low[u],dfn[v]);
}
if(dfn[u]==low[u])
{
int x;
scc++;
do{
x=s.top();
s.pop();
col[x]=scc;
vis[x]=;
}while(x!=u);
}
}
bool two_sat(){ for(int i=;i<*n;i++){
if(dfn[i]==-){
tarjan(i);
}
}
for(int i=;i<n;i++){
if(col[*i]==col[*i+]){
return false;
}
}
return true;
}
int main()
{
while(scanf("%d%d",&n,&m)==){
init();
for(int i=;i<N;i++) e[i].clear();
while(!s.empty()){
s.pop();
}
int a,b,c;
char s[];
for(int i=;i<m;i++){
scanf("%d%d%d%s",&a,&b,&c,s);
if(s[]=='A'){
if(c==){
//e[2*a+1].push_back(2*a);
//e[2*b+1].push_back(2*b);
add(*a+,*a);
add(*b+,*b);
}
else{
//e[2*a].push_back(2*b+1);
//e[2*b].push_back(2*a+1);
add(*a,*b+);
add(*b,*a+);
}
}
else if(s[]=='O'){
if(c==){
//e[2*a+1].push_back(2*b);
//e[2*b+1].push_back(2*a);
add(*a+,*b);
add(*b+,*a);
}
else{
//e[2*a].push_back(2*a+1);
//e[2*b].push_back(2*b+1);
add(*a,*a+);
add(*b,*b+);
}
}
}
if(two_sat()){
printf("YES\n");
}
else{
printf("NO\n");
}
}
return ;
}