2-SAT

Posted 2021-03-14 lhm-

(2-SAT)是一种特殊的逻辑判定问题

其为一串布尔变量，每个变量只能为真或假。要求对这些变量进行赋值，满足布尔方程

对每个变量，规定(x)为其(0)状态，(x+n)为其(1)状态

从(x)向(y)连一条有向边表示选了(x)后必须选(y)

缩点后，若存在(x)和(x^prime)在同一个强连通分量中，则无解

(x)存在后,(y)必须存在：(x ightarrow y , y^prime ightarrow x^prime)

(x)和(y)不能同时存在：(x ightarrow y^prime , y ightarrow x^prime)

(x)和(y)必须同时存在：(x ightarrow y , x^prime ightarrow y^prime)

(x)和(y)必须只存在其中一个：(x^prime ightarrow y , y^prime ightarrow x)

(x)不能存在：(x ightarrow x^prime)

(x)必须存在：(x^prime ightarrow x)

最终确定方案时，对于一个点的两个状态，保留拓扑序大的那一个，因为在(Tarjan)缩点的过程中已经处理好拓扑序了，所以不用再拓扑排序，强联通分量编号是拓扑序的逆序

输出字典序最小的方案时，从(1)到(2n)枚举点，若该点能选，则将与其相连的点都选上，若该点不能选（另一个状态选了），则与其相连的点都不能选

(code:)

void tarjan(int x)
{
    dfn[x]=low[x]=++dfn_cnt;
    st[++top]=x;
    vis[x]=true;
    for(int i=head[x];i;i=e[i].nxt)
    {
        int y=e[i].to;
        if(!dfn[y])
        {
            tarjan(y);
            low[x]=min(low[x],low[y]);
        }
        else if(vis[y])
            low[x]=min(low[x],dfn[y]);
    }
    if(low[x]==dfn[x])
    {
        co_cnt++;
        int now;
        do
        {
            now=st[top--];
            vis[now]=false;
            co[now]=co_cnt;
        }while(now!=x);
    }
}
bool check()
{
    for(int i=1;i<=2*n;++i)
        if(!dfn[i])
            tarjan(i);
    for(int i=1;i<=n;++i)
        if(co[i]==co[i+n])
            return false;
    return true;
}

......

add(x+(a^1)*n,y+b*n),add(y+(b^1)*n,x+a*n);