2-SAT 问题其实就是几个值  只有  0 1状态可取.在有限制的情况下,能不能有一组值可以满足这种限制。

通过强联通判断会不会有一个值  0 1状态同时出现,如果出现 就不可能 ,不出现就可能。

就按照下题讲一下。

POJ 3687Katu Puzzle

Katu Puzzle

Time Limit: 1000MS   Memory Limit: 65536K
Total Submissions:11446   Accepted: 4241

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 ≤ 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 (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

POJ Founder Monthly Contest – 2008.07.27, Dagger

 

先分析下各种运算符

AND    

0 0-> 0

0 1->0

1 0->0

1 1 ->1

当AND 操作出现的时候

第一种 x&y==0    如果 x=0 y可以为0 1两种所以当x ==0的时候没有限制 ,但当x=1时 x=1,y必然为 0 所以就出现了限制

这个时候就添一条边 x-y'        y'表示值 y 等于0 (其它博客写的都是   y'表示 为1 )

同理 y=1  x=0   y->x'

当  x&y==1     这就只有一种可能性   x==1 y==1  所以 x必须等1 所以添加一条边  x'->x 0->1 表示 x=0 时必须为 1 一旦出现x=0 就直接错了。    同理  y'->y;

其它操作符就自己推吧 我就说一下 x|y==0   x,和y 必须为 0  所以,有 x->x'  y->y' 这两种限制。

 

AC代码

#include<iostream>
#include<algorithm>
#include<cstring>
#include<string>
#include<vector>
#include<cstdio>
#include<cmath>
#include<queue>
#include<map>
#include<set>
#include<stack>

using namespace std;
typedef long long ll;
typedef unsigned long long ull;
typedef pair<int,int> P;

const long long mod=1e9+7;
const int maxn=1e5+25;
const int maxm=1e5+25;
const int INF=0x7fffffff;
const int inf=0x3f3f3f3f;
const double eps=1e-8;
int n,m;
struct two {
    int a,b;
} node[maxm];
bool bmp(two x,two y) {
    return (x.a==y.a)?x.b<y.b:x.a<y.a;
}
int N,M;
vector<int> G[maxn];
vector<int> rG[maxn];
vector<int> vs;
bool used[maxn];
int cmp[maxn];
void add(int from,int to) {         //有向图添边
    G[from].push_back(to);
    rG[to].push_back(from);
}

void dfs(int v) {
    used[v]=true;
    for(int i=0; i<G[v].size(); i++) {
        if(!used[G[v][i]])dfs(G[v][i]);
    }
    vs.push_back(v);                        //加入那些最后跑到的结点
}

void rdfs(int v,int k) {
    used[v]=true;
    cmp[v]=k;
    for(int i=0; i<rG[v].size(); i++) {
        if(!used[rG[v][i]])rdfs(rG[v][i],k);
    }
}

int scc() {
    memset(used,0,sizeof(used));
    vs.clear();
    for(int v = 0; v < N ; v ++) {
        if(!used[v]) {
            dfs(v);
        }
    }
    memset(used,0,sizeof(used));
    int k=0;
    for(int i =vs.size()-1; i>=0; i--) {       //每次从最后跑
        if(!used[vs[i]])rdfs(vs[i],k++);
    }
    return k;
}

int main() {
//    freopen("int.txt","r",stdin);
    scanf("%d%d",&n,&m);
    for(int i=0; i<m; i++) {
        int a,b,c;
        char ch[10];
        scanf("%d%d%d%s",&a,&b,&c,ch);
        if(ch[0]=='A') {
            if(c==1) {            //还是不会推,留言,或者 +Q3035536707
                add(a,a+n);
                add(b,b+n);
                add(a+n,b+n);
                add(b+n,a+n);
            }
            if(c==0) {
                add(a+n,b);
                add(b+n,a);
            }
        } else if(ch[0]=='O') {
            if(c==1) {
                add(a,b+n);
                add(b,a+n);
            } else {
                add(a+n,a);
                add(b+n,b);
                add(a,b);
                add(b,a);
            }
        } else {
            if(c==1) {
                add(a+n,b);
                add(a,b+n);
                add(b+n,a);
                add(b,a+n);
            } else {
                add(a,b);
                add(b,a);
                add(a+n,b+n);
                add(b+n,a+n);
            }
        }
    }
    N=2*n;
    scc();
    int flag=1;
    for(int i=0; i<n; i++) {
        if(cmp[i]==cmp[i+n])flag=0;
    }
    puts(flag?"YES":"NO");
    return 0;
}