POJ.3678.Katu Puzzle(2-SAT)

題目連接

如下轉自：zck921031.
對於本題，咱們逐個考慮每一個邏輯運算：

一、A AND B=0.這要求A和B不一樣時爲1。既然不一樣時爲1，那麼A取1時，B必須取0；B取1時，A必須取0.因此，連邊A+n->B, B+n->A。

二、A AND B=1.這要求A和B同時爲1。換句話說，A和B不能是0.那要怎麼樣體如今圖中呢？咱們知道，判斷一個2-sat問題是否存在合法方案的方法是，縮點後判斷有沒有兩個同組點屬於同一個連通份量。

咱們須要A和B都必須是1，那麼咱們就讓A和B必須選0時無解便可。也就是說，連邊A->A+n, B->B+n。這樣的話，假如構圖完成後，A必須取0，那麼因爲存在邊A->A+n，因此A也必須取1，那麼就不多是一個合法方案。因此，這兩條邊能保證，有合法方案的話，必定是A取1（選A+n節點）的狀況。

三、A OR B=0.這要求A和B同時爲0.和2相似。

四、A XOR B=0.這要求A=B。因此，A爲0/1時，B必須爲0/1，同理B爲0/1時，A必須爲0/1.因此添加邊：A->B,B->A,A+n->B+n,B+n->A+n。

鏈接某邊是爲了推出矛盾。x->y表示選x則必須選y.

注意數據下標是從0開始的

//624K  63MS
#include <cstdio>
#include <cctype>
#include <algorithm>
#define gc() getchar()
const int N=2005,M=4e6+5;

int n,m,H[N],Enum,nxt[M],to[M];
int top,sk[N],dfn[N],low[N],id,bel[N],cnt;
bool ins[N];

inline int read()
{
    int now=0;register char c=gc();
    for(;!isdigit(c);c=gc());
    for(;isdigit(c);now=now*10+c-'0',c=gc());
    return now;
}
inline void AddEdge(int u,int v){
    to[++Enum]=v, nxt[Enum]=H[u], H[u]=Enum;
}
void Tarjan(int x)
{
    dfn[x]=low[x]=++id, sk[++top]=x, ins[x]=1;
    for(int v,i=H[x]; i; i=nxt[i])
        if(!dfn[v=to[i]]) Tarjan(v), low[x]=std::min(low[x],low[v]);
        else if(ins[v]) low[x]=std::min(low[x],dfn[v]);
    if(low[x]==dfn[x])
    {
        ++cnt;
        do{
            bel[sk[top]]=cnt, ins[sk[top--]]=0;
        }while(x!=sk[top+1]);
    }
}

int main()
{
    n=read(),m=read();
    int a,b,c; char opt[6];
    for(int i=1; i<=m; ++i)
    {
        a=read()+1,b=read()+1,c=read(),scanf("%s",opt);
        if(opt[0]=='A')
            if(c) AddEdge(a,a+n),AddEdge(b,b+n);
            else AddEdge(a+n,b),AddEdge(b+n,a);
        else if(opt[0]=='O')
            if(c) AddEdge(a,b+n),AddEdge(b,a+n);
            else AddEdge(a+n,a),AddEdge(b+n,b);
        else//Xor
            if(c) AddEdge(a,b+n),AddEdge(b,a+n),AddEdge(a+n,b),AddEdge(b+n,a);
            else AddEdge(a,b),AddEdge(b,a),AddEdge(a+n,b+n),AddEdge(b+n,a+n);
    }
    for(int i=1; i<=n<<1; ++i)
        if(!dfn[i]) Tarjan(i);
    bool f=1;
    for(int i=1; i<=n; ++i)
        if(bel[i]==bel[i+n]) {f=0; break;}
    puts(f?"YES":"NO");

    return 0;
}