POJ 3678 Katu Puzzle（2-SAT）

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"

 

题目大意：每条边给出一个OP和一个ANS，要求每条边的连点A、B，符合A OP B == ANS，其中A、B、ANS都为0或1

思路：2-SAT问题

A AND B == 0则A真→B假，B真→A假

A AND B == 1则A、B都为真，即B假→B真，A假→A真（即不能出现A假推出A真的情况，A假不能被选上，在强连通图中，若A真通过多步推出A假，即成环，无解）

A OR B == 0则A、B都为假，即B真→B假，A真→A假（同上）

A OR B == 1则A假→B真，B假→A真

A XOR B == 0则A真↔B真，A假↔B假

A XOR B == 1则A真↔B假，A假↔B真

 

#include <cstdio>
#include <cstring>
using namespace std;

const int MAXN = 2010;
const int MAXM = 1000010*4;

struct TwoSAT{
    int n, ecnt, dfs_clock, scc_cnt;
    int St[MAXN], c;
    int head[MAXN], sccno[MAXN], lowlink[MAXN], pre[MAXN];
    int next[MAXM], to[MAXM];

    void init(int nn){
        n = nn;
        ecnt = 2; dfs_clock = scc_cnt = 0;
        memset(head,0,sizeof(head));
    }

    void addEdge(int x, int y){
        to[ecnt] = y; next[ecnt] = head[x]; head[x] = ecnt++;
    }

    void addEdge2(int x, int y){
        addEdge(x,y); addEdge(y,x);
    }

    void dfs(int u){
        lowlink[u] = pre[u] = ++dfs_clock;
        St[++c] = u;
        for(int p = head[u]; p; p = next[p]){
            int &v = to[p];
            if(!pre[v]){
                dfs(v);
                if(lowlink[u] > lowlink[v]) lowlink[u] = lowlink[v];
            }else if(!sccno[v]){
                if(lowlink[u] > pre[v]) lowlink[u] = pre[v];
            }
        }
        if(lowlink[u] == pre[u]){
            ++scc_cnt;
            while(true){
                int x = St[c--];
                sccno[x] = scc_cnt;
                if(x == u) break;
            }
        }
    }

    bool solve(){
        for(int i = 0; i < n; ++i)
            if(!pre[i]) dfs(i);
        for(int i = 0; i < n; i += 2)
            if(sccno[i] == sccno[i^1]) return false;
        return true;
    }

} G;

int main(){
    int n, m, a, b, c;
    char d[5];
    while(scanf("%d%d",&n,&m)!=EOF){
        G.init(2*n);
        while(m--){
            scanf("%d%d%d%s",&a,&b,&c,d);
            if(d[0] == 'A' && c == 0){//a&b=false
                G.addEdge(a*2, b*2+1);
                G.addEdge(b*2, a*2+1);
            }
            if(d[0] == 'A' && c == 1){//a&b=true
                G.addEdge(a*2+1, a*2);
                G.addEdge(b*2+1, b*2);
            }
            if(d[0] == 'O' && c == 0){//a|b=false
                G.addEdge(a*2, a*2+1);
                G.addEdge(b*2, b*2+1);
            }
            if(d[0] == 'O' && c == 1){//a|b=true
                G.addEdge(b*2+1, a*2);
                G.addEdge(a*2+1, b*2);
            }
            if(d[0] == 'X' && c == 0){//a^b=false
                G.addEdge2(a*2, b*2);
                G.addEdge2(a*2+1, b*2+1);
            }
            if(d[0] == 'X' && c == 1){//a^b=true
                G.addEdge2(a*2, b*2+1);
                G.addEdge2(a*2+1, b*2);
            }
        }
        if(G.solve()) printf("YES
");
        else printf("NO
");
    }
    return 0;
}