『算法-ACM竞赛-图论』2-SAT-详解

『算法-ACM 竞赛-图论』2-SAT-详解

图论–2-SAT–详解

问题描述：

现有一个由 N 个布尔值组成的序列 A，给出一些限制关系，比如 A[x]AND A[y]=0、A[x] OR A[y] OR A[z]=1 等，要确定 A[0..N-1]的值，使得其满足所有限制关系。这个称为 SAT 问题，特别的，若每种限制关系中最多只对两个元素进行限制，则称为 2-SAT 问题。

由于在 2-SAT 问题中，最多只对两个元素进行限制，所以可能的限制关系共有 11 种：

A[x]
NOT A[x]
A[x] AND A[y]
A[x] _ AND_ NOT A[y]
A[x] OR A[y]
A[x] OR** **_**NOT**_ A[y]
** NOT** (A[x] AND A[y])
**NOT **(A[x] OR A[y])
A[x] XOR A[y]
NOT (A[x] XOR A[y])
A[x] XOR** **_**NOT**_ A[y]

进一步，3 可以用 1 表示：A[x]，A[y]，NOT(A[x] XOR A[y]) 相当于 NOT A[x] AND NOT A[y]。狄摩根定律。只剩下了 9 中基本关系类型。

在实际问题中，2-SAT 问题在大多数时候表现成以下形式：有 N 对物品，每对物品中必须选取一个，也只能选取一个，并且它们之间存在某些限制关系（如某两个物品不能都选，某两个物品不能都不选，某两个物品必须且只能选一个，某个物品必选）等，这时，可以将每对物品当成一个布尔值（选取第一个物品相当于 0，选取第二个相当于 1），如果所有的限制关系最多只对两个物品进行限制，则它们都可以转化成 9 种基本限制关系，从而转化为 2-SAT 模型。

(引自：http://www.cnblogs.com/kuangbin/archive/2012/10/05/2712429.html)

2-SAT 模型建立:

1.我们利用一条有向边<i,j>，来表示选 i 的情况下，一定要选 j;

2.用 i 表示某个点是 true,那么 i’表示某个点是 false

3.因为限制的两两之间的关系，所以我们可以通过逻辑关系来建边：

1）如果给出 A 和 B 的限制关系，A 和 B 必须一起选，(A and B)||(!A and !B )==true 那么选 A 必须选 B，建边<i,j>和<j,i>还有<i’,j’>和<j’,i’>

2）如果给出 A 和 B 的限制关系，选 A 不能选 B，那么(A && !B)||(!A && B )==true,建边<i,j’>和<j,i’>

3）如果必须选 A,那么 A==true,建边<i’,i>

4）如果 A 一定不能选，那么!A==true.建边<i,i’>

这么建图之后，会出现一个有向图，这个有向图会导致一个连通环，导致某个点一旦选取，那么这条链上的所有点都要被选中。如果我们找到一个强连通分量，那么这个强连通分量当中的点，如果选取必须全部选取，不选取的话一定是全部不选取，所以只要满足这个有向图中连通的点不会导致 i 和 i’同时被选取，如果不存在矛盾，那么当前问题就是有解的。但是往往在求解过程中，我们要求的解会要求一些性质，所以提供以下几种解决方案。

用离散的的知识解释的话就是下面这位大佬的讲解（别人发给我的）

首先，把「2」和「SAT」拆开。SAT 是 Satisfiability 的缩写，意为可满足性。即一串布尔变量，每个变量只能为真或假。要求对这些变量进行赋值，满足布尔方程。

举个例子：教练正在讲授一个算法，代码要给教室中的多位同学阅读，代码的码风要满足所有学生。假设教室当中有三位学生：Anguei、Anfangen、Zachary_260325。现在他们每人有如下要求：

Anguei: 我要求代码当中满足下列条件之一：
1. 不写 using namespace std; （ ¬a）
2. 使用读入优化（b）
3. 大括号不换行（ ¬c）
Anfangen: 我要求代码当中满足下条件之一：
1. 写 using namespace std; （a）
2. 使用读入优化（b）
3. 大括号不换行（ $\neg ¬c$ ）
Zachary_260325：我要求代码当中满足下条件之一：
1. 不写 using namespace std; （ $\neg ¬a$ ）
2. 使用 scanf （ $\neg ¬b$ ）
3. 大括号换行（c）

我们不妨把三种要求设为 a,b,ca,b,c，变量前加 \neg¬ 表示「不」，即「假」。上述条件翻译成布尔方程即： $(\neg a\vee b\vee\neg c) \wedge (a\vee b\vee\neg c) \wedge (\neg a\vee\neg b\vee c)(¬a∨b∨¬c)∧(a∨b∨¬c)∧(¬a∨¬b∨c)$ 。其中， $\vee∨$ 表示或， $\wedge∧$ 表示与。

现在要做的是，为 ABC 三个变量赋值，满足三位学生的要求。

Q: 这可怎么赋值啊？暴力？

A: 对，这是 SAT 问题，已被证明为 NP 完全 的，只能暴力。

Q: 那么 2-SAT 是什么呢？

A: 2-SAT，即每位同学 只有两个条件（比如三位同学都对大括号是否换行不做要求，这就少了一个条件）不过，仍要使所有同学得到满足。于是，以上布尔方程当中的 c, $\neg cc$ ,¬c 没了，变成了这个样子： $(\neg a\vee b) \wedge (a\vee b) \wedge (\neg a\vee\neg b)$

公式杀招：

怎么求解 2-SAT 问题？

使用强连通分量。 对于每个变量 xx，我们建立两个点：x ,¬x 分别表示变量 xx 取 true 和取 false。所以，图的节点个数是两倍的变量个数。在存储方式上，可以给第 ii 个变量标号为 ii，其对应的反值标号为 i + ni+n。对于每个同学的要求 (a∨b)，转换为 ¬a→b∧¬b→a。对于这个式子，可以理解为：「若 aa 假则 bb 必真，若 bb 假则 aa 必真」然后按照箭头的方向建有向边就好了。综上，我们这样对上面的方程建图：

原式	建图
	a→b∧¬b→¬a
	¬a→b∧¬b→a
	a→¬b∧b→¬a

于是我们得到了这么一张图：

built

可以看到，¬a 与 b 在同一强连通分量内，a 与 ¬b 在同一强连通分量内。同一强连通分量内的变量值一定是相等的。也就是说，如果 x 与 ¬x 在同一强连通分量内部，一定无解。反之，就一定有解了。

但是，对于一组布尔方程，可能会有多组解同时成立。要怎样判断给每个布尔变量赋的值是否恰好构成一组解呢？

这个很简单，只需要 当 xx 所在的强连通分量的拓扑序在 \neg x¬x 所在的强连通分量的拓扑序之后取 xx 为真 就可以了。在使用 Tarjan 算法缩点找强连通分量的过程中，已经为每组强连通分量标记好顺序了——不过是反着的拓扑序。所以一定要写成 color[x] < color[-x] 。

代码实现：

//暴力DFS，求字典序最小的解，也是求字典序唯一的方法
#include<cstdio>
#include<cstring>
#include<vector>
using namespace std;
const int maxn=10000+10;
struct TwoSAT
{
    int n;//原始图的节点数(未翻倍)
    vector<int> G[maxn*2];//G[i]==j表示如果mark[i]=true,那么mark[j]也要=true
    bool mark[maxn*2];//标记
    int S[maxn*2],c;//S和c用来记录一次dfs遍历的所有节点编号

    void init(int n)
    {
        this->n=n;
        for(int i=0;i<2*n;i++) G[i].clear();
        memset(mark,0,sizeof(mark));
    }

    //加入(x,xval)或(y,yval)条件
    //xval=0表示假，yval=1表示真
    void add_clause(int x,int xval,int y,int yval)
    {
        x=x*2+xval;
        y=y*2+yval;
        G[x^1].push_back(y);
        G[y^1].push_back(x);
    }

    //从x执行dfs遍历,途径的所有点都标记
    //如果不能标记,那么返回false
    bool dfs(int x)
    {
        if(mark[x^1]) return false;//这两句的位置不能调换
        if(mark[x]) return true;
        mark[x]=true;
        S[c++]=x;
        for(int i=0;i<G[x].size();i++)
            if(!dfs(G[x][i])) return false;
        return true;
    }

    //判断当前2-SAT问题是否有解
    bool solve()
    {
        for(int i=0;i<2*n;i+=2)
        if(!mark[i] && !mark[i+1])
        {
            c=0;
            if(!dfs(i))
            {
                while(c>0) mark[S[--c]]=false;
                if(!dfs(i+1)) return false;
            }
        }
        return true;
    }
};


//联通分量+拓扑排序，求任意意一组解，比较快

#include <cstdio>
#include <cstring>
#include <queue>
#include <vector>
#include <stack>
#include <algorithm>
#define MAXN 2000+10
#define MAXM 400000
#define INF 1000000
using namespace std;
vector<int> G[MAXN];
int low[MAXN], dfn[MAXN];
int dfs_clock;
int sccno[MAXN], scc_cnt;
stack<int> S;
bool Instack[MAXN];
int N, M;
void init()
{
    for(int i = 0; i < 2*N; i++) G[i].clear();
}
void getMap()
{
    int a, b, c;
    char op[10];
    while(M--)
    {
        scanf("%d%d%d%s", &a, &b, &c, op);
        switch(op[0])
        {
            case 'A':
            if(c == 1)//a,b取1
            {
                G[a + N].push_back(a);
                G[b + N].push_back(b);
            }
            else//a,b至少一个不为真
            {
                G[a].push_back(b + N);
                G[b].push_back(a + N);
            }
            break;
            case 'O':
            if(c == 1)//a,b最少有一个为真
            {
                G[b + N].push_back(a);
                G[a + N].push_back(b);
            }
            else//a,b都为假
            {
                G[a].push_back(a + N);
                G[b].push_back(b + N);
            }
            break;
            case 'X':
            if(c == 1)//a b 不同值
            {
                G[a + N].push_back(b);
                G[a].push_back(b + N);
                G[b].push_back(a + N);
                G[b + N].push_back(a);
            }
            else//a b 同真同假
            {
                G[a].push_back(b);
                G[b].push_back(a);
                G[a + N].push_back(b + N);
                G[b + N].push_back(a + N);
            }
        }
    }
}
void tarjan(int u, int fa)
{
    int v;
    low[u] = dfn[u] = ++dfs_clock;
    S.push(u);
    Instack[u] = true;
    for(int i = 0; i < G[u].size(); i++)
    {
        v = G[u][i];
        if(!dfn[v])
        {
            tarjan(v, u);
            low[u] = min(low[u], low[v]);
        }
        else if(Instack[v])
        low[u] = min(low[u], dfn[v]);
    }
    if(low[u] == dfn[u])
    {
        scc_cnt++;
        for(;;)
        {
            v = S.top(); S.pop();
            Instack[v] = false;
            sccno[v] = scc_cnt;
            if(v == u) break;
        }
    }
}
void find_cut(int l, int r)
{
    memset(low, 0, sizeof(low));
    memset(dfn, 0, sizeof(dfn));
    memset(sccno, 0, sizeof(sccno));
    memset(Instack, false, sizeof(Instack));
    dfs_clock = scc_cnt = 0;
    for(int i = l; i <= r; i++)
    if(!dfn[i]) tarjan(i, -1);
}
void solve()
{
    for(int i = 0; i < N; i++)
    {
        if(sccno[i] == sccno[i + N])
        {
            printf("NO\n");
            return ;
        }
    }
    printf("YES\n");
}
int main()
{
    while(scanf("%d%d", &N, &M) != EOF)
    {
        init();
        getMap();
        find_cut(0, 2*N-1);
        solve();
    }
    return 0;
}

算法 > ACM竞赛 > 图论

『算法-ACM竞赛-图论』2-SAT-详解

https://chiamzhang.github.io/2024/06/29/『算法-ACM竞赛-图论』2-SAT-详解/

Author

Chiam

Posted on

June 29, 2024

Licensed under

『算法-ACM竞赛-图论』BFS总结 Previous

『算法-ACM竞赛-图论』2-SAT-暴力染色法求字典序最小模版 Next