题解 P4782 【【模板】2-SAT 问题】

Piwry · 2021-02-06 11:13:31 · 题解

貌似少有题解解释 “取拓扑序较大者” 这步的正确性，于是这里就补充个简短的证明

另外在我查阅资料时，还发现有以 wiki 为代表的另一种 2-sat 做法，主要区别在最后一步；由于没什么实现价值，这里就不展开了。有兴趣可以参考 “2-SAT 解法浅析”, wiki(en)

解析

Part 0 - 导入

一般我们求解 2-sat 的过程为：

建图（具体略）
对图求出强联通分量，并求出缩点后的拓扑序
若存在对应同一个变量的两个结点在同一个分量内，即无解
否则一定有解；对每个变量取所在分量拓扑序较大的那个对应结点，一定能构造出一组合法解

其中不太显然的地方主要在 \text{4.}

Part 1 - 引理

设变量 x_i 对应的结点为 u_{i, p}, p\in \{0, 1\}

先考虑这样一个引理：

引理 1. 若存在边 (u_{i, p}, u_{j, q})，那么一定对应地存在边 (u_{j, q\text{ xor }1}, u_{i, p\text{ xor }1})

考虑我们建图的连边规则，这是显然的（即若有要求「x_i=b_1 或 x_j=b_2」，那么 x_i 对应的不满足要求的结点（u_{i, b_1\text{ xor }1}）就会向 x_j 对应的满足要求的结点（u_{j, b_2}）连一条有向边；另一条边亦然）

更进一步地，有如下引理：

引理 2. 若存在路径（单向）p(u_{i, p}, u_{j, q})，那么一定对应地存在路径 p(u_{j, q\text{ xor }1}, u_{i, p\text{ xor }1})

对路径上每一条边运用 \text{引理 1.} 即可得到

Part 2 - 证明

再考虑我们算法的 \text{4.}；不妨用反证法证明其正确性

记 f(u_{i, p}) 表示 u_{i, p} 所在分量的（缩点后的）拓扑序

设有 f(u_{i, p})<f(u_{i, p\text{ xor }1}) [1], f(u_{j, q})>f(u_{j, q\text{ xor }1}) [2]，且存在路径（单向）P_1=p(u_{j, q}, u_{i, p})。显然这由我们的算法会得到一个非法的结果

考虑 \text{引理 2.}，得出也存在路径 P_2=p(u_{i, p\text{ xor }1}, u_{j, q\text{ xor }1})。由 P_1 可推出 f(u_{j, q})<f(u_{i, p}) [3]，由 P_2 可推出 f(u_{i, p\text{ xor }1})<f(u_{j, q\text{ xor }1}) [4]。联立 [1], [3], [4] 可得 f(u_{j, q})<f(u_{j, q\text{ xor }1})，这和作为前提的 [2] 是矛盾的；由此可推得算法的 \text{4.} 是正确的

（这部分作图可能会更直观w）

CODE

仅供参考

#include <cstdio>
#include <algorithm>
using std::min;

/*------------------------------IO------------------------------*/

namespace IO_number{
    int read(){
        int x =0; char c =getchar(); bool f =0;
        while(c < '0' || c > '9') (c == '-') ? f =1, c =getchar() : c =getchar();
        while(c >= '0' && c <= '9') x =(x<<1)+(x<<3)+(48^c), c =getchar();
        return (f) ? -x : x;
    }

    void write(const int &x){
        if(x/10)
            write(x/10);
        putchar('0'+x%10);
    }
}
using namespace IO_number;

/*------------------------------Graph------------------------------*/

const int MAXN =1e6+20;

int first[MAXN<<1], tote;
struct edge{
    int to, nxt;
}e[MAXN<<1];

inline void addedge(const int &u, const int &v){
    ++tote, e[tote].to =v, e[tote].nxt =first[u], first[u] =tote;
}

/*------------------------------Tarjan------------------------------*/

int scc_id[MAXN<<1], Scc_id;

int dfn[MAXN<<1], low[MAXN<<1], Dfn;
int stk[MAXN<<1], stk_top;
bool instk[MAXN<<1];

void tarjan(const int &u){
    low[u] =dfn[u] =++Dfn;
    stk[stk_top++] =u;
    instk[u] =1;
    for(int l =first[u]; l; l =e[l].nxt){
        if(!dfn[e[l].to]){
            tarjan(e[l].to);
            low[u] =min(low[u], low[e[l].to]);
        }
        else if(instk[e[l].to])
            low[u] =min(low[u], dfn[e[l].to]);
    }
    if(low[u] == dfn[u]){
        ++Scc_id;
        while(stk[stk_top] != u){
            scc_id[stk[stk_top-1]] =Scc_id;
            instk[stk[stk_top-1]] =0;
            --stk_top;
        }
    }
}

/*------------------------------Main------------------------------*/

int main(){
    int n =read(), m =read();
    for(int t =0; t < m; ++t){
        int i =read(), a =read(), j =read(), b =read();
        /* [1, n] -> false, [n+1, 2n] -> true */
        // x_i, x_j 均不满足不能同时成立 //
        addedge(i+(a^1)*n, j+b*n);
        addedge(j+(b^1)*n, i+a*n);
    }

    for(int i =1; i <= 2*n; ++i){
        if(!dfn[i])
            tarjan(i);
        if(i <= n && scc_id[i] == scc_id[i+n])
            return puts("IMPOSSIBLE") && 0;
    }
    puts("POSSIBLE");
    for(int i =1; i <= n; ++i)
        write((scc_id[i+n] < scc_id[i])), putchar(' ');
}