算法：POJ 3678 Katu Puzzle（2-SAT判断）

算法：POJ 3678 Katu Puzzle（2-SAT判断）2014-01-10 csdn shuangde800【题目大意】

有一个有向图G（V，E），每条边e（a,b）上有一个位运算符op（AND， OR或XOR）和一个值c（0或1）。

问能不能在这个图上的每个点分配一个值X（0或1），使得每一条边e（a,b）满足 Xa op Xb = c

【思路】

每一个点上只能取0或者1，显然是2-SAT模型。

关键是怎样建边。

对于两个点a和 b， a有两个值a1=0，a2=1， b也有两个值 b1=0, b2=1.

那么枚举这两点的所有关系

（a1, b1）

（a1, b2）

（a2, b1）

（a2, b2）

然后根据位运算符看每个关系时符合条件还是不符合，如果不符合就说明这个关系时矛盾对，要添加两条边

假设是关系（a1，b1）矛盾，那么就要添加边 a1—>b2, b1— >a2即可。

依次类推。

【代码】

#include<iostream> #include<cstdio>#include<cstring>using namespace std;typedef long long int64;const int MAXN = 2010;const int VN = MAXN*2;const int EN = 4000010;int n, m;class Graph{public:void init（）{size = 0;memset（head, -1, sizeof（head））;}void addEdge（int u, int v）{E[size].v = v;E[size].next = head[u];head[u] = size++;}public:int size;int head[VN];struct Edge{ int v, next; }E[EN];}g;class Two_Sat{public:bool check（const Graph&g, const int n）{scc（g, n）; for（int i=0; i<n; ++i）if（belong[i*2] == belong[i*2+1]）return false;return true;}private:void tarjan（const Graph&g, const int u）{int v;DFN[u] = low[u] = ++idx;sta[top++] = u;inStack[u] = true;for（int e=g.head[u]; e！=-1; e=g.E[e].next）{v = g.E[e].v;if（DFN[v] == -1）{tarjan（g, v）;low[u] = min（low[u], low[v]）;}else if（inStack[v]）{low[u] = min（low[u], DFN[v]）;}}if（low[u] == DFN[u]）{++bcnt;do{v = sta[--top];inStack[v] = false;belong[v] = bcnt;}while（u ！= v）;}}void scc（const Graph&g, const int n）{top = idx = bcnt = 0;memset（DFN, -1, sizeof（DFN））;memset（inStack, 0, sizeof（inStack））;for（int i=0; i<2*n; ++i）{if（DFN[i] == -1） tarjan（g, i）;}}private:int top, idx, bcnt;int sta[VN];int DFN[VN];int low[VN];int belong[VN];bool inStack[VN];}sat;int main（）{int u, v, w;char op[5];while（~scanf（"%d%d", &n, &m））{g.init（）;for（int i=0; i<m; ++i） {scanf（"%d%d%d%s",&u, &v, &w, op）; if（！strcmp（op, "AND"））{if（w）{g.addEdge（u*2, v*2+1）,g.addEdge（v*2, u*2+1）; //0, 0 g.addEdge（u*2, v*2）,g.addEdge（v*2+1, u*2+1）; // 0, 1g.addEdge（u*2+1, v*2+1）,g.addEdge（v*2, u*2）; // 1, 0}else{g.addEdge（u*2+1, v*2）,g.addEdge（v*2+1, u*2）; // 1, 1 }}else if（！strcmp（op, "OR"））{if（w）{g.addEdge（u*2, v*2+1）,g.addEdge（v*2, u*2+1）; //0, 0 }else{g.addEdge（u*2, v*2）,g.addEdge（v*2+1, u*2+1）; // 0, 1g.addEdge（u*2+1, v*2+1）,g.addEdge（v*2, u*2）; // 1, 0g.addEdge（u*2+1, v*2）,g.addEdge（v*2+1, u*2）; // 1, 1 }}else{ // XORif（w）{g.addEdge（u*2, v*2+1）,g.addEdge（v*2, u*2+1）; //0, 0 g.addEdge（u*2+1, v*2）,g.addEdge（v*2+1, u*2）; // 1, 1 }else{g.addEdge（u*2, v*2）,g.addEdge（v*2+1, u*2+1）; // 0, 1g.addEdge（u*2+1, v*2+1）,g.addEdge（v*2, u*2）; // 1, 0}}}if（sat.check（g, n）） puts（"YES"）;else puts（"NO"）;}return 0;}