0w1

POJ 3678 Katu Puzzle

Problem Description:
Given some constraints formed with two variables, and operator of OR, AND, or XOR, you are to find whether there exists a solution to satisfy all the constraints.

Constraints:
1 ≤ N ≤ 1000 (number of variables)
1 ≤ M ≤ 1e6 (number of constraints)

Solution:
It is always possible to decompose OR, AND, and XOR into forms of if a then b. Then solve with 2-SAT algorithm. Look at the code if you are interested in the details.

Code:

#include <iostream>
#include <vector>
#include <string>
#include <algorithm>

void topo_sort(const std::vector<std::vector<int> > &graph, int u, std::vector<int> &stk, std::vector<int> &vis) {
  if (vis[u]) return;
  vis[u] = 1;
  for (int i = 0; i < int(graph[u].size()); ++i) {
    topo_sort(graph, graph[u][i], stk, vis);
  }
  stk.push_back(u);
}

void ksrj(const std::vector<std::vector<int> > &graph, int u, std::vector<int> &scc, int scc_id) {
  if (scc[u]) return;
  scc[u] = scc_id;
  for (int i = 0; i < int(graph[u].size()); ++i) {
    ksrj(graph, graph[u][i], scc, scc_id);
  }
}

std::vector<int> scc_dcmp(const std::vector<std::vector<int> > &graph) {
  std::vector<int> scc(graph.size()); {
    std::vector<int> stk, vis(graph.size()); {
      for (int i = 0; i < int(graph.size()); ++i) {
        topo_sort(graph, i, stk, vis);
      }
    }
    std::vector<std::vector<int> > rgraph(graph.size()); {
      for (int i = 0; i < int(graph.size()); ++i) {
        for (int j = 0; j < int(graph[i].size()); ++j) {
          rgraph[graph[i][j]].push_back(i);
        }
      }
    }
    std::reverse(stk.begin(), stk.end());
    for (int i = 0; i < int(stk.size()); ++i) {
      if (scc[stk[i]]) continue;
      static int scc_id = 0;
      ++scc_id;
      ksrj(rgraph, stk[i], scc, scc_id);
    }
  }
  return scc;
}

signed main() {
  std::ios::sync_with_stdio(false);
  int N, M;
  std::cin >> N >> M;
  std::vector<std::vector<int> > G(N << 1);
  for (int i = 0; i < M; ++i) {
    int A, B, C;
    std::string OP;
    std::cin >> A >> B >> C >> OP;
    if (OP == "OR") {
      if (C) {
        G[N + A].push_back(B);
        G[N + B].push_back(A);
      } else {
        G[A].push_back(N + A);
        G[B].push_back(N + B);
      }
    } else if (OP == "AND") {
      if (C) {
        G[N + A].push_back(A);
        G[N + B].push_back(B);
      } else {
        G[A].push_back(N + B);
        G[B].push_back(N + A);
      }
    } else if (OP == "XOR") {
      if (C) {
        G[N + A].push_back(B);
        G[A].push_back(N + B);
        G[N + B].push_back(A);
        G[B].push_back(N + A);
      } else {
        G[N + A].push_back(N + B);
        G[A].push_back(B);
        G[N + B].push_back(N + A);
        G[B].push_back(A);
      }
    }
  }
  std::vector<int> at_scc = scc_dcmp(G);
  bool ng = false;
  for (int i = 0; i < N; ++i) {
    ng |= at_scc[i] == at_scc[N + i];
  }
  std::cout << (ng ? "NO" : "YES") << std::endl;
  return 0;
}