[模板] 2-SAT 问题

简介

2-SAT (2-satisfiability) 问题形如:

1. 给定一些变量 \(x_i \in {true,false}\);
   
2. 给定一些一元/二元约束条件,如 \(x_i \land \lnot x_j\),利用 \(\land\) 连接;
3. 为每一个变量赋一个值,满足所有约束条件.

将第2条改为n元约束条件,即为 N-SAT 问题.

可以证明 N-SAT 问题没有多项式解法,但 2-SAT 问题有 \(O(n + m)\) 的解法.

算法

对每个变量建立两个点: \(x_i\),\(x_i'\),表示取真或假.

根据约束条件建立若干条边 \((p,q)\),表示若选 \(p\) 则必须选 \(q\). (见下)

将得到的图缩点. 若 \(x_i\) 和 \(x_i'\) 在同一个强连通分量内,则无解.

否则,若 \(x_i\) 的所在强连通分量的拓扑序大于 \(x_i'\),则选 \(x_i\); 否则选 \(x_i'\).

我们知道tarjan算法求出的强连通分量标号为强连通分量拓扑序的逆序. 因此判断 \(scc_{x_i} < scc_{x_i'}\) 即可.

建边

1. 一元逻辑
   1. \(p\): \((p',p)\);
   2. \(\lnot p\): \((p,p')\).
2. 二元逻辑 (\(p\) 和 \(\lnot p\) 是一样的,下面仅描述 \(p\) 的情况)
   1. \(p \rightarrow q\): \((p,\((q',p')\);
   2. \(p \land q\): 等价于 \(p\),\(q\);
   3. \(p \lor q\): \((p',p)\) (等价于 \(\lnot p \rightarrow q\));
   4. \(p \oplus q\): \((p,q')\),\((p',\((q,p')\),p)\). (xor)

容易发现所有二元逻辑都会建立若干对边,这称作2-SAT问题的对称性,是算法正确的关键.

代码

int chos[nsz];
int dfn[nsz*2],pd=0,low[nsz*2],inscc[nsz*2],ps=0;
int stk[nsz*2],top=0,vi[nsz*2];
void tarj(int p){
    dfn[p]=low[p]=++pd;
    stk[++top]=p,vi[p]=1;
    for(auto v:edge[p]){
        if(dfn[v]==0){
            tarj(v);
            low[p]=min(low[p],low[v]);
        }
        else if(vi[v])low[p]=min(low[p],dfn[v]);
    }
    if(low[p]==dfn[p]){//scc
        ++ps;
        int v;
        do{
            v=stk[top];
            inscc[v]=ps,vi[v]=0,--top;
        }while(v!=p);
    }
}

bool sat2(){//toefl ielts sat
    rep(i,2,n*2+1)if(dfn[i]==0)tarj(i);
    rep(i,1,n){
        if(inscc[i<<1]==inscc[i<<1|1])return 0;//no solution
        chos[i]=inscc[i<<1|1]<inscc[i<<1];
    }
    return 1;
}