【算法】2-SAT

在进行 $2-SAT$ 问题的讲解之前,先来了解 $SAT$ 到底是个啥

所谓的 $SAT$ 问题,指的是布尔可满足性问题(Boolean satisfiability problem),或者说适定性(Satisfiability)问题
询问是否存在一组布尔变量的值使得若干个布尔公式的值均为 True

对于 $2-SAT$ 问题来说,每个布尔公式有且仅有两个变量
相应的,对于 $K-SAT$ 问题,每个布尔公式则有 $K$ 个变量

$$ \begin{matrix} F=(x_1)\land(x_2)\land\cdots\land(x_n) & 1-SAT\\ F=(x_1\lor y_1)\land(x_2\lor y_2)\land\cdots\land(x_n\lor y_n) & 2-SAT\\ \cdots\\ F=(x_1\lor y_1\lor...)\land(x_2\lor y_2\lor...)\land\cdots\land(x_n\lor y_n\lor...) & ...-SAT\\ \end{matrix} $$

其中, $x_i,y_j$ 可以指代任意一个变量

遗憾的是, $K-SAT$ 问题在 $K>2$ 时是 $NP-Complete$ 的,它也是第一个被证明为 $NP-Complete$ 的问题,在最坏复杂度下,是没有多项式时间内的算法的
至于 $1-SAT$ ,则比较白痴,是个人都会做

那么,现在开始进入正题: $2-SAT$

How to Solve

由于对于每个变量 $x$ 来说,有两个取值 True / False
那么建出两个点 $x,x'$ 分别表示该变量取 True / False

假设有关系 $x\lor y$ 那么连一条 $x'\Rightarrow y$ 的边表示如果选择 $x'$ 必然选择 $y$
同样,也要连出一条 $y'\Rightarrow x$ 的边表示如果选择 $y'$ 必然选择 $x$

那么如果出现一些其他的符号呢?

比如说 $x\land y$ ,相当于连两条边 $x'\Rightarrow x,y'\Rightarrow y$ 表示如果选 $x'$ 和 $y'$ ,必然要选 $x$ 和 $y$ 。但是这显然是不可能的,所以只能选 $x,y$ 了呗

剩下的情况请自行考虑如何连边

将图构建完成后接下来就需要判断是否有解和构造一组可行解

如果两个点 $x,x'$ 在一组强联通分量内,说明这两者在限制条件下必须同时选
显然的,这两个点并不能同时出现(薛定谔的变量?)
也就是说,这样的情况代表着无解

对于其他情况来说,将强连通分量缩点后形成的图肯定是一个 $DAG$ ,由于 $DAG$ 上的边代表着依赖关系,对于每一组变量 $x,x'$ ,选择其对应的强联通分量拓扑序较大的一个(标号较小的一个)
这样也可以有效的防止依赖问题

如果有特殊限制(字典序最小等),直接暴力染色就完事了

Problem

POJ - 3648 Wedding

有 $n$ 对夫妇,两排座位,其中第 $0$ 对夫妇为新娘新郎
一对夫妇不能坐在同一排,还有 $m$ 对关系不能坐在新娘对面
问坐在新娘对面的人有哪些

设第 $i$ 对夫妇和新娘同侧的点为 $x_i,y_i$ ,和新郎同侧的点为 $x_i',y_i'$

显然需要先连边 $x_0'\Rightarrow x_0,y_0\Rightarrow y_0'$ 保证新郎新娘的位置正确

对于一对夫妇来说,他们不能坐在同一侧,所以 $x_i\Rightarrow y_i',y_i\Rightarrow x_i',x_i'\Rightarrow y_i,y_i'\Rightarrow x_i$
保证两两不在同一侧

对于某对关系中的点 $(x_i,y_j)$ ($(x_i,x_j),(y_i,y_j)$ 啥的也行啦) ,他们不能同时出现在新娘的对面,那么连边 $x_i'\Rightarrow y_i,y_i'\Rightarrow x_i$

然后跑 $Tarjan$ 就行了呗

#include <algorithm>
#include <iostream>
#include <cstring>
#include <cstdio>
#include <cmath>

using namespace std;
const int N = 150;
struct Edge {
    int t, n;
}e[N * N];
int head[N], Etot;
int n, m;

void add(int u, int v) {
    e[++ Etot] = {v, head[u]};
    head[u] = Etot;
}

int dfn[N], low[N], DFN;
int sta[N], top;
bool vis[N];

int id[N], cnt;

void dfs(int x) {
    dfn[x] = low[x] = ++ DFN;
    sta[++ top] = x; vis[x] = 1;
    for(int i = head[x]; i; i = e[i].n) {
        int t = e[i].t;
        if(!dfn[t]) {
            dfs(t);
            low[x] = min(low[x], low[t]);
        }
        else if(vis[t])
            low[x] = min(low[x], dfn[t]);
    }
    if(low[x] == dfn[x]) {
        ++ cnt;
        while(sta[top] != x) {
            id[sta[top]] = cnt;
            vis[sta[top]] = 0;
            sta[top --] = 0;
        }
        id[sta[top]] = cnt;
        vis[sta[top]] = 0;
        sta[top --] = 0;
    }
}

void Tarjan() {
    for(int i = 1; i <= n * 4; ++ i)
        if(!dfn[i])
            dfs(i);
    int flag = 1;
    for(int i = 1; i <= n * 2 && flag; ++ i)
        if(id[i] == id[i + n * 2])
            flag = 0;
    if(!flag) puts("bad luck");
    else {
        for(int i = 1; i < n; ++ i) {
            if(id[i * 2 + 1] < id[i * 2 + 1 + n * 2])
                printf("%dw ", i);
            if(id[i * 2 + 2] < id[i * 2 + 2 + n * 2])
                printf("%dh ", i);
        }
    }
}

void clear() {
    memset(head, 0, sizeof(head));
    memset(dfn, 0, sizeof(dfn));
    memset(low, 0, sizeof(low));
    memset(id, 0, sizeof(id));
    Etot = cnt = 0;
}

int main() {
    #ifndef ONLINE_JUDGE
        freopen("in", "r", stdin);
    #endif
    while(1) {
        clear();    
        scanf("%d %d", &n, &m);
        if(!n && !m) break;
        add(1 + 2 * n, 1);
        add(2, 2 + 2 * n);
        for(int i = 0; i < n; ++ i) {
            add(i * 2 + 1, i * 2 + 2 + n * 2);
            add(i * 2 + 2 + n * 2, i * 2 + 1);
            add(i * 2 + 2, i * 2 + 1 + n * 2);
            add(i * 2 + 1 + n * 2, i * 2 + 2);
        }
        int a, b;
        char ac, bc;
        for(int i = 1; i <= m; ++ i) {
            scanf("%d%c%d%c", &a, &ac, &b, &bc);
            a = a * 2;
            if(ac == 'w') a += 1;
            else a += 2;
            b = b * 2;
            if(bc == 'w') b += 1;
            else b += 2;
            add(a + 2 * n, b);
            add(b + 2 * n, a);
        }
        Tarjan();
    }
    return 0;
}
Comments

添加新评论

已有 2 条评论

3.31还没到呢OωO

Chlience Chlience 回复 @青山

来自未来的博客(ฅ´ω`ฅ)