# 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;
}
```