HDU 3062 Party

题意：中文题，裸的SAT

思路：推荐一个聚聚关于SAT的讲解（传送门），poj也有类似的板子题，谁知道poj挂了

代码：

#include <bits/stdc++.h>
using namespace std;
const int maxn=3005;
const int maxm=2000005;

struct node
{
    int to,nxt;
} edge[maxm];
int head[maxn];
int low[maxn],dfn[maxn],stk[maxn],be[maxn];
int top,tim,num,tot;/// init -1 0 0 0
bool instk[maxn];

void add_edge(int u,int v)
{
    edge[tot].to=v;
    edge[tot].nxt=head[u];
    head[u]=tot++;
}
void init()
{
    tot=0;num=0;tim=0;
    top=-1;
    memset(dfn,0,sizeof(dfn));
    memset(head,-1,sizeof(head));
    memset(instk,false,sizeof(instk));
}
void tarjan(int u)
{
    int v;
    low[u]=dfn[u]=++tim;
    stk[++top]=u;
    instk[u]=1;
    for(int k=head[u];~k;k=edge[k].nxt){
        v=edge[k].to;
        if(!dfn[v]){
            tarjan(v);
            low[u]=min(low[u],low[v]);
        }
        else if(instk[v]){
            low[u]=min(low[u],dfn[v]);
        }
    }
    if(dfn[u]==low[u]){
        ++num;
        do{
            v=stk[top--];
            instk[v]=false;
            be[v]=num;
        }
        while(u!=v);
    }
}
int main()
{
    int n,m;
    while(~scanf("%d%d",&n,&m)){
        init();
        for(int i=0;i<m;i++){
            int a,b,c,d;
            scanf("%d%d%d%d",&a,&b,&c,&d);
            a=(a<<1)+c;
            b=(b<<1)+d;
            add_edge(a,b^1);
            add_edge(b,a^1);
        }
        for(int i=0;i<2*n;i++){
            if(!dfn[i])tarjan(i);
        }
        bool ok=true;
        for(int i=0;i<n;i++){
            if(be[2*i]==be[2*i+1]){
                ok=false;break;
            }
        }
        if(ok)printf("YES
");
        else printf("NO
");
    }
    return 0;
}