关于2-SAT的一些总结

2-SAT：
二选一时进行联想。
多和二分答案联系。
可以用来解一些含不等号的不等式。
（而含等号的不等式则可以用差分约束系统来解。）

 

2-SAT就是给你一组变量，变量的取值只有01（或者其它的）两种，变量之间有一些不兼容的关系，问你如何给变量赋一组值使得满足这些条件。

可能会有判断是否有解的情况，这样就只需要求强连通然后判断一组的两个是否在同一分量里。

而另一种则是需要输出解，那么则需要建立反拓扑序然后染色。

 

2010AsiaRegional in ChengDu的Go Deeper这题就是这么个典型的例子。一定不要拘泥于2-SAT的形式，果断发现x[i]只有0和1两种取值这个“二选一”的典型的2-SAT的特征。抓住这个关键之后，二分应该会自然而然地被联想到。

 

zju 4085 二分+2-SAT。

要特别注意此题二分的写法。之前天津网赛的BombGame的二分我自己的写法是可以的但是这题必须把查找区间左右各扩大一。因为这个WA了很多次啊~~~另外就是加边的时候明显要根据对称性，不等于1的那个加四条。

 

#include<iostream>
#include<cstdio>
#include<cstring>
using namespace std;
const int maxn = 410;
const int maxm = 10010;
int n,m;
int T;
int G[maxn][maxn],G2[maxn][maxn];
struct node
{
    int a,b,c;
}Q[maxm];
int col[maxn],vis[maxn];
int dfn[maxn],low[maxn],stack[maxn];
int cnt,order,TOP,inx;
int tm[maxn],ID[maxn];
void dfs(int u)
{
    dfn[u] = low[u] = ++inx;
    stack[++TOP] = u;
    vis[u] = 1;
    for(int v = 0;v<2*n;v++)if(G[u][v])
    {
        if(!dfn[v])
        {
            dfs(v);
            low[u] = min(low[u],low[v]);
        }
        else if(vis[v])
          low[u] = min(low[u],dfn[v]);
    }
    if(low[u]==dfn[u])
    {
        int x;
        do{
             x = stack[TOP--];vis[x] = 0;ID[x] = order;
        }while(x!=u);
        order++;
    }
}
void Tarjan()
{
    int i;
    TOP = -1;inx = 0;order = 0;
    for(i = 0;i<2*n;i++)dfn[i] = 0;
    memset(vis,0,sizeof(vis));
    for(i = 0;i<2*n;i++)if(!dfn[i])dfs(i);
}
int main()
{
    int i;
    scanf("%d",&T);
    while(T--)
    {
        scanf("%d%d",&n,&m);
        for(i = 0;i<m;i++)
          scanf("%d%d%d",&Q[i].a,&Q[i].b,&Q[i].c);
        int l = 0,r = m+1;
        int mid;
        while(l<r)
        {
            mid = (l+r)/2;
            memset(G,0,sizeof(G));
            for(i = 0;i<mid;i++)
            {
                int x = Q[i].a,y = Q[i].b;
               // if(x!=y)
               // {
                if(Q[i].c == 0)
                  G[2*x][2*y+1] = 1,G[2*y][2*x+1] = 1;
                else if(Q[i].c==2)
                  G[2*x+1][2*y] = 1,G[2*y+1][2*x] = 1;
                else
                {
                    G[2*x][2*y] = 1,G[2*y+1][2*x+1] = 1;
                    G[2*y][2*x] = 1,G[2*x+1][2*y+1] = 1;
                }
              //  }
          /*      else
                {
                    if(Q[i].c==0)G[2*x+1][2*x] = 1;
                    else if(Q[i].c==2)G[2*x][2*x+1] = 1;
                }*/
            }
            Tarjan();
            for(i = 0;i<n;i++)
              if(ID[2*i]==ID[2*i+1]){r = mid;break;}
            if(i==n)l = mid+1;
         /*   rebuild();
            toposort();
            color();
            for(i = 0;i<n;i++)
              if(col[ID[2*i]]==col[ID[2*i+1]]){r = mid;break;}
            if(i==n)l = mid+1;*/
        }
        printf("%d/n",r-1);
    }
    return 0;
}