2-SAT模板

用的是刘汝佳大白书里面的版本。网上还有tarjan缩点后再拓扑排序构造解的版本，感觉靠谱一点，但太长了。。。

ps:为什么说“如果当前考虑的变量不管赋值为真还是假都会引起矛盾，可以证明整个2-SAT问题无解”？？？

是这样的：比如说，某个点探测到的所有点，构成了一个集合。如果有必要调整前面的策略，那就是这个“某个点”探测到的那些点的集合的对立面被访问到了，也就是说，有条边从外面指向里面的点的对立面，然而，如果是这样，那根据图的对称性，这个被指向对立面的里面的某个点也会指向指向他对立面的点的对立面，所以这个指进来的点也属于这个集合，与条件矛盾。---CYC

int n;
#define maxn ???
struct Edge{int to,next;};
#define maxe ???
struct Graph
{
    Edge edge[maxe];int le;
    int first[maxn],vis[maxn];
    void clear()
    {
        le=2;
        memset(first,0,sizeof(first));
    }
    void insert(int x,int y)
    {
        edge[le].to=y;
        edge[le].next=first[x];
        first[x]=le++;
    }
    void add_clause(int x,int y)
    {
        insert(x^1,y);
        insert(y^1,x);
    }
    int sta[maxn],top;
    bool dfs(int x)
    {
        if (vis[x^1]) return 0;
        if (vis[x]) return 1;
        vis[x]=1;
        sta[++top]=x;
        for (int i=first[x];i;i=edge[i].next)
            if (!dfs(edge[i].to)) return 0;
        return 1;
    }
    bool twosat()
    {
        memset(vis,0,sizeof(vis));
        for (int i=1;i<=n;i++)
            if (!vis[i*2] && !vis[i*2+1])
            {
                top=0;
                if (!dfs(i*2))
                {
                    for (;top;top--) vis[sta[top]]=0;
                    if (!dfs(i*2+1)) return 0;
                }
            }
        return 1;
    }
}G;