POJ 3678 - Katu Puzzle

http://poj.org/problem?id=3678

概要

ノード N 個，エッジ M 個の有向グラフが与えられ，各エッジには AND, OR, XOR のいずれかと真偽値がラベルされている．

ノードを変数とみたとき，すべての AND, OR, XOR の関係を満たすような真偽値を割り当てが存在するかどうか答える．

制約

解法

いわゆる 2-SAT 問題．

2-SAT は，論理式を (A→B)∧(C→D)∧…∧(Y→Z) (A, ..., Z は単なる変数かそれの否定)のような形に変形し，implication の関係を有向グラフで表して，同じ強連結成分に同じ変数の肯定と否定の両方が含まれているかどうか調べることで解くことができる．

  1 #include <cstdio>
  2 #include <string>
  3 #include <vector>
  4 #include <stack>
  5 using namespace std;
  6 
  7 void scc_visit(const vector<vector<int> >& g, int v, vector<int>& scc_map, int& scc_size,/*{{{*/
  8         stack<int>& stk, vector<bool>& in_stk, vector<int>& low, vector<int>& num, int& time)
  9 {
 10   low[v] = num[v] = ++time;
 11   stk.push(v);
 12   in_stk[v] = true;
 13   for (vector<int>::const_iterator it(g[v].begin()); it != g[v].end(); ++it) {
 14     const int u = *it;
 15     if (num[u] == 0) {
 16       scc_visit(g, u, scc_map, scc_size, stk, in_stk, low, num, time);
 17       low[v] = min(low[v], low[u]);
 18     } else if (in_stk[u]) {
 19       low[v] = min(low[v], num[u]);
 20     }
 21   }
 22   if (low[v] == num[v]) {
 23     for (;;) {
 24       const int u = stk.top();
 25       stk.pop();
 26       in_stk[u] = false;
 27       scc_map[u] = scc_size;
 28       if (u == v) {
 29         break;
 30       }
 31     }
 32     ++scc_size;
 33   }
 34 }/*}}}*/
 35 pair<vector<int>,int> strongly_connected_components(const vector<vector<int> >& g)/*{{{*/
 36 {
 37   const int N = g.size();
 38   vector<int> num(N), low(N);
 39   stack<int> stk;
 40   vector<bool> in_stk(N, false);
 41   int time = 0;
 42   vector<int> scc_map(N);
 43   int scc_size = 0;
 44   for (int v = 0; v < N; v++) {
 45     if (num[v] == 0) {
 46       scc_visit(g, v, scc_map, scc_size, stk, in_stk, low, num, time);
 47     }
 48   }
 49   return make_pair(scc_map, scc_size);
 50 }/*}}}*/
 51 
 52 // 2-SAT
 53 int main()
 54 {
 55   int N, M;
 56   scanf("%d %d", &N, &M);
 57   vector<vector<int> > g(2*N);
 58   for (int i = 0; i < M; i++) {
 59     int a, b, c;
 60     char o[16];
 61     scanf("%d %d %d %s", &a, &b, &c, o);
 62     const string op(o);
 63     if (op == "AND") {
 64       if (c) {
 65         // a && b = 1 == (!a -> a) && (!b -> b)
 66         g[a+N].push_back(a);
 67         g[b+N].push_back(b);
 68       } else {
 69         // a && b = 0 == (a -> !b) && (b -> !a)
 70         g[a].push_back(b+N);
 71         g[b].push_back(a+N);
 72       }
 73     } else if (op == "OR") {
 74       if (c) {
 75         // a || b = 1 == (!a -> b) && (!b -> a)
 76         g[a+N].push_back(b);
 77         g[b+N].push_back(a);
 78       } else {
 79         // a || b = 0 == (a -> !a) && (b -> !b)
 80         g[a].push_back(a+N);
 81         g[b].push_back(b+N);
 82       }
 83     } else {
 84       // XOR
 85       if (c) {
 86         // a ^ b = 1 == (a -> !b) && (b -> !a) && (!a -> b) && (!b -> a)
 87         g[a].push_back(b+N);
 88         g[b].push_back(a+N);
 89         g[a+N].push_back(b);
 90         g[b+N].push_back(a);
 91       } else {
 92         // a ^ b = 0 == (a -> b) && (b -> a) && (!a -> !b) && (!b -> !a)
 93         g[a].push_back(b);
 94         g[b].push_back(a);
 95         g[a+N].push_back(b+N);
 96         g[b+N].push_back(a+N);
 97       }
 98     }
 99   }
100 
101   const pair<vector<int>, int> p = strongly_connected_components(g);
102   vector<vector<bool> > has(p.second, vector<bool>(N, false));
103   for (int i = 0; i < N; i++) {
104     has[p.first[i]][i] = true;
105   }
106   for (int i = N; i < 2*N; i++) {
107     if (has[p.first[i]][i-N]) {
108       puts("NO");
109       return 0;
110     }
111   }
112   puts("YES");
113   return 0;
114 }
poj/3678.cc