题目链接：POJ3678-Katu Puzzle

题意：

给n个bool变量，然后给定他们之间的一些关系(and,or,xor)，判断是否存在一组解。

题解：

经典的2-sat问题。

首先，我们可以对每个变量进行拆点，对于变量x，我们可以将其拆为x0和x1两个点，分别表示x取0或取1的情况。

然后对于每个命题，我们可以判定其中的真假情况：

1. 若x取假，那么我们建边(x1,x0)。
2. 若x取真，那么我们建边(x0,x1)。

然后对这个图求强连通分量并缩点，若存在x1与x0在同一个连通块中的情况，那么则没有解。

简单描述一下建边的过程。

1. x&y=1：x，y全部为1，建边(x0,x1)，(y0,y1)。
2. x&y=0：x，y其中至少有一个为0，建边(x1,y0)，(y1,x0)。
3. x|y=1：x，y其中至少有一个为1，建边(x0,y1)，(y0,x1)。
4. x|y=0：x，y全部为0，建边(x1,x0)，(y1,y0)。
5. x^y=1：x，y不同，(x1,y0)，(y1,x0)，(x0,y1)，(y0,x1)。
6. x^y=0：x，y相同，(x1,x1)，(y1,y1)，(x0,x0)，(y0,y0)。

参考代码：

#include<cstdio>
#include<cstring>
#include<stack>
using namespace std;
const int MAXN=2e3+9;
const int MAXM=1e7+9;
int n,m;
struct EDGE
{
    int v,nxt;
} edge[MAXM*2];
int cnt=0,fir[MAXN];
void addedge(int u,int v)
{
    edge[cnt].v=v;
    edge[cnt].nxt=fir[u];
    fir[u]=cnt++;
}
int tot,sig;
int dfn[MAXN],low[MAXN],col[MAXN];
stack<int>  sta;
bool used[MAXN];
void Tarjan(int u)
{
    used[u]=1;
    dfn[u]=low[u]=++tot;
    sta.push(u);
    for(int i=fir[u]; i!=-1; i=edge[i].nxt)
    {
        int v=edge[i].v;
        if(!dfn[v])
        {
            Tarjan(v);
            low[u]=min(low[u],low[v]);
        }
        else   if(used[v])
            low[u]=min(low[u],dfn[v]);
    }
    if(low[u]==dfn[u])
    {
        sig++;
        while(1)
        {
            int temp=sta.top();
            sta.pop();
            used[temp]=0;
            col[temp]=sig;
            if(temp==u)
                break;
        }
    }
}
int main()
{
    scanf("%d%d",&n,&m);
    sig=tot=0;
    memset(fir,-1,sizeof(fir));
    memset(dfn,0,sizeof(dfn));
    memset(low,0,sizeof(low));
    for(int i=1; i<=m; i++)
    {
        int u,v,w;
        char op[10];
        scanf("%d%d%d %s",&u,&v,&w,op);
        if(op[0]=='A')
        {
            if(w)
                addedge(u+n,u),addedge(v+n,v);
            else
                addedge(u,v+n),addedge(v,u+n);
        }
        else    if(op[0]=='O')
        {
            if(w)
                addedge(u+n,v),addedge(v+n,u);
            else
                addedge(u,u+n),addedge(v,v+n);
        }
        else    if(op[0]=='X')
        {
            if(w)
                addedge(u,v+n),addedge(v,u+n),addedge(u+n,v),addedge(v+n,u);
            else
                addedge(u,u),addedge(v,v),addedge(u+n,v+n),addedge(v+n,u+n);
        }
    }
    for(int i=0; i<n*2; i++)
        if(!dfn[i])
            Tarjan(i);
    for(int i=0; i<n; i++)
        if(col[i]==col[i+n])
            return puts("NO"),0;
    puts("YES");
    return 0;
}