POJ3678Katu Puzzle（2sat）

POJ 2-sat 六题第二题

http://blog.sina.com.cn/s/blog_64675f540100k15b.html

题目描述：

一些点，点的取值可以是0或者1，没有告诉你具体取值。

一些边，有权值，有运算方式（并，或，异或），要求和这条边相连的两个点经过边上的运算后的结果是边的权值。

问你有没有可能把每个点赋值满足所有边的要求。

解题报告：

每个点只有0，1两种值，并且和边对面的点有约束条件，所以可以转化为2-sat问题。

令i表示点i去0，i + n表示点i取1.

点i与点j and 等于0时。 i + n -> j, j + n -> i

and 等于 1时，要求i和j必须为1，不能为0.

不能为0的处理时：如果i取0，那么i就要取1.

即：i -> i + n。

剩下的就是类似的方法了

// File Name: 3678.cpp
// Author: zlbing
// Created Time: 2013/1/22 23:13:52

#include<iostream>
#include<string>
#include<algorithm>
#include<cstdlib>
#include<cstdio>
#include<set>
#include<map>
#include<vector>
#include<cstring>
#include<stack>
using namespace std;
#define MAXN 1000+50
struct TwoSAT{
    int n;
    vector<int>G[MAXN*2];
    bool mark[MAXN*2];
    stack<int>S;
    bool dfs(int x)
    {
        if(mark[x^1])return false;
        if(mark[x])return true;
        mark[x]=true;
        S.push(x);
        for(int i=0;i<G[x].size();i++)
        {
            int v=G[x][i];
            if(!dfs(v))return false;
        }
        return true;
    }
    void init(int _n)
    {
        n=_n;
        for(int i=0;i<2*n;i++)
            G[i].clear();
        memset(mark,0,sizeof(mark));
    }
    void add_clause(int x,int y)
    {
        G[x].push_back(y);
    }
    bool solve()
    {
        for(int i=0;i<2*n;i=i+2)
        {
            if(!mark[i]&&!mark[i+1]){
                  while(!S.empty())
                  {
                      S.pop();
                  }
                if(!dfs(i))
                {
                    while(!S.empty())
                    {
                        mark[S.top()]=false;
                        S.pop();
                    }
                    if(!dfs(i+1))return false;
                }
            }
        }
        
//        for(int i=0;i<2*n;i++)
//            if(mark[i])printf("%d ",T[i/2][i%2]);
//        printf("\n");
        return true;
    }
};

int main(){
    int n,m;
    while(~scanf("%d%d",&n,&m))
    {
        TwoSAT solver;
        solver.init(n);
            int a,b,c;
            char ch[10];
        for(int i=0;i<m;i++)
        {
            scanf("%d%d%d",&a,&b,&c);
            scanf("%s",ch);
            if(c)
            {
                if(ch[0]=='A')
                {
                    solver.add_clause(2*a,2*a+1);
                    solver.add_clause(2*b,2*b+1);
                }
                if(ch[0]=='O')
                {
                    solver.add_clause(2*a,2*b+1);
                    solver.add_clause(2*b,2*a+1);
                }
                if(ch[0]=='X')
                {
                    solver.add_clause(2*a,2*b+1);
                    solver.add_clause(2*a+1,2*b);
                    solver.add_clause(2*b,2*a+1);
                    solver.add_clause(2*b+1,2*a);
                }
            }
            else
            {
                if(ch[0]=='A')
                {
                    solver.add_clause(2*a+1,2*b);
                    solver.add_clause(2*b+1,2*a);
                }
                if(ch[0]=='O')
                {
                    solver.add_clause(2*a+1,2*a);
                    solver.add_clause(2*b+1,2*b);
                }
                if(ch[0]=='X')
                {
                    solver.add_clause(2*a,2*b);
                    solver.add_clause(2*a+1,2*b+1);
                    solver.add_clause(2*b,2*a);
                    solver.add_clause(2*b+1,2*a+1);
                }
            }
        }
        if(solver.solve())
            printf("YES\n");
        else printf("NO\n");
    }
    return 0;
}