POJ 3678は2 SATを深く理解する

感じ:この问题は一晩见て、すべての问题の报告を见てやっと明日どうしたの......昨日独学で2 SATを理解していないで、だから辺さえどのように连れていることを知らないで、その上他の人の问题の报告を见ても分からないで、どうしてそんなに连れて、気を失って......
構想:ノードa,b,値c,そして判断方式OPを与えるので,このように見ると当然2 SATでやったことがわかる.なぜ2 SATを深く理解しているのか、なぜなら......2 SATの中で、関係が確定してこそ縁を結ぶことができ、そうでなければ縁を結ぶことができないと言ったからだ.もう1つ重要なのは、ある条件が値でなければならない場合、自身と自身の反対の条件も接続しなければならないということです.具体的には、以下の説明を参照してください.
現在2*aを1とし、2*a+1を0とする.もちろん2*bは1、2*b+1は0です.
1.OPが「And」の場合:
(1)c=1の場合、aとbが同時に1である場合のみ、a AND bは1に等しく、aとbがともに1である場合のみこの条件が成立するので、aとbは必ず1を待たなければならないので、辺<2*a+1,2*a>、<2*b+1,2*b>、<2*b+1,2*b>、いずれにしても、aとbの場合は1に等しく、すなわち、aが0である場合aは必ず1に等しく、bが0である場合bは必ず1に等しく、この最初は他の人の解題を見ていたレポートはこのように言って、それから自分もあまり理解していませんが、実は本当の内包はaとbを強制して1に等しいことです!(aが1に等しいなら当然この辺は役に立たないが、aが0に等しいならば、この連はaを強制的に1に等しくして問題条件に合致させることができる.このように簡単で、ゆっくり理解しなければならない)
(2)c=0の場合、aが0に等しい場合、bは0であっても1であってもよいので、不確定関係であり、上記のように必ず確定関係であってこそ辺を結ぶことができるので、aが0の場合は辺を結ぶことができない;aが1に等しい場合、bは必ず0であってこそa AND b=0になるので、辺:<2*a,2*b+1>、もちろん<2*b,2*a,+1>もある.
2.OPがORの場合、
(1)c=1の場合、a=1の場合、b=1またはb=0であるため、a=1の場合、2つの関係が現れたが、不確定であり、エッジを接続する必要はない;a=0の場合、bは一定=1であるので、決定関係であり、エッジ:<2*a+1,2*b>、もちろん<2*b+1,2*a>である.
(2)c=0の場合、a=b=0という関係しかないので、これは上の1(1)の場合と同様であり、上はa=b=1を強制的に実行する場合であり、ここではa=b=0の場合のみであるため、a=b=0、すなわち辺:<2*a,2*a+1>,<2*b,2*b+1>を強制的に実行する.
3.OPがXORの場合、a=1の場合、bは必ず=0である.a=0,b必=1;b=1,aは必ず=0である.b=0,aは必ず=1である.このように見ると、この4つの関係はすべて確定しているので、辺を結ぶ必要がありますが、実は私たちはつながっていなくてもいいです.1つの辺もつながっていません.a=1を出すときは必ずa=0は現れません.この4つの辺は矛盾しません.だから、強連通縮点後にbelong[2*a]=belong[2*a+1]は現れないので、つながっても始まらないのです.判断の時間が少し増えただけだ......これは他人の解題報告でグループリングを形成したという意味だ.例えば、a=1、b=0とb=0、a=1はtarjanの中で新しいノード、すなわち自環を形成するので......異或の場合はa=0またはa=1しか選択できないので矛盾は起こらない......だから縁を結ぶ必要はない!

#include <iostream>
#include <cstdio>
#include <fstream>
#include <algorithm>
#include <cmath>
#include <deque>
#include <vector>
#include <list>
#include <queue>
#include <string>
#include <cstring>
#include <map>
#include <stack>
#include <set>
#define PI acos(-1.0)
#define mem(a,b) memset(a,b,sizeof(a))
#define sca(a) scanf("%d",&a)
#define sc(a,b) scanf("%d%d",&a,&b)
#define pri(a) printf("%d
",a)
#define lson i<<1,l,mid
#define rson i<<1|1,mid+1,r
#define MM 200005
#define MN 2010
#define INF 1000000007
#define eps 1e-7
using namespace std;
typedef long long ll;
int DFN[MN],vis[MN],LOW[MN],Stack[MN*10],belong[MN],tem,Count,top;
vector<int>e[MN];
void tarjan(int u)
{
    DFN[u]=LOW[u]=++tem;
    vis[u]=true;
    Stack[++top]=u;
    int v,i,l=e[u].size();
    for(i=0;i<l;i++)
    {
        v=e[u][i];
        if(!DFN[v])
        {
            tarjan(v);
            LOW[u]=min(LOW[u],LOW[v]);
        }
        else if(vis[v]&&DFN[v]<LOW[u]) LOW[u]=DFN[v];
    }
    if(DFN[u]==LOW[u])
    {
        Count++;
        do
        {
            v=Stack[top--];
            vis[v]=false;
            belong[v]=Count;
        }while(v!=u);
    }
}
bool twoSAT(int n)
{
    for(int i=0;i<2*n;i++)
        if(!DFN[i]) tarjan(i);
    for(int i=0;i<n;i++)
        if(belong[2*i]==belong[2*i+1]) return false;
    return true;
}
int main()
{
    int n,m,i,a,b,c;
    char s[5];
    sc(n,m);
    for(i=0;i<m;i++)
    {
        scanf("%d%d%d%s",&a,&b,&c,s);
        if(s[0]=='A')
        {
            if(c)
            {
                e[2*a+1].push_back(2*a);
                e[2*b+1].push_back(2*b);
            }
            else
            {
                e[2*a].push_back(2*b+1);
                e[2*b].push_back(2*a+1);
            }
        }
        else if(s[0]=='O')
        {
            if(c)
            {
                e[2*a+1].push_back(2*b);
                e[2*b+1].push_back(2*a);
            }
            else
            {
                e[2*a].push_back(2*a+1);
                e[2*b].push_back(2*b+1);
            }
        }
    }
    if(twoSAT(n)) puts("YES");
    else puts("NO");
    return 0;
}