2-SAT

ACM

主要积累2-SAT的模板，以及相应的思想

2-SAT

现在有这样的逻辑表达式:
\(x_i为假或者x_j为假，\)，我们进行相应的推测：
当\(x_i\)为真的时候，那么\(x_j\)必为假.这两个节点之间连一条边
同理：当\(x_j\)为真的时候，那么\(x_i\)必为假。这两个节点连一条边。
因为当其中的一个节点成立的时候，另外的一个节点必然也成立。

现在我们进行相应的拆点：
将逻辑节点i，拆成2i与2i+1:

mark[2i]表示节点i为假，mark[2i+1]表示节点i为真。

连完相应的边之后，使用dfs进行相应的判断，若产生冲突，那么就要进行相应的新的尝试。

题目

1146 - Now or later

题意

每一架飞机都有早降落和晚降落的选择，并且都要进行相应的选择。
我们现在就要决策每一架的飞机的降落时间，使得每一架飞机降落的时间的间隔的最小值，最大。

题解

二分降落时间，然后用2-SAT进行相应的判断。

AC代码

其中有这样的一行代码：

1
if(abs(T[i][a]-T[j][b])<diff) solver.add_clause(i, a, j, b);

注意判断其中添加语句的巧妙性。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
#include <bits/stdc++.h>
using namespace std;
const int maxn = 2e3+10;
int n;
struct TwoSAT{
    //int n;
    vector<int> G[maxn*2];
    bool mark[maxn*2];
    int sta[maxn*2], c;
    void init(){
        //this->n = n;
        for(int i=0; i<n*2; i++) G[i].clear();
        memset(mark, 0, sizeof(mark));
        this->c = 0;
    }
    bool dfs(int x){
        if(mark[x^1]) return false;
        if(mark[x]) return true;
        mark[x] = true;
        sta[c++] = x;
        for(int i=0; i<G[x].size(); i++){
            if(!dfs(G[x][i])) return false;
        }
        return true;
    }
    void add_clause(int x, int xval, int y, int yval){
        x = 2*x+xval;
        y = 2*y+yval;
        G[x^1].push_back(y);
        G[y^1].push_back(x);
    }
    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[sta[--c]] = false;
                    //第一个假设不成立，再进行第二个假设成立。
                    //若两个假设都不成立,那么这个逻辑式将不成立，直接退出搜索
                    if(!dfs(i+1)) return false;
                }
            }
        }
        return true;
    }
};
TwoSAT solver;
int T[maxn][3];
bool judge(int diff){
    for(int i=0; i<n; i++)
        for(int a=0; a<2; a++)
            for(int j=i+1; j<n; j++)
                for(int b=0; b<2; b++)
                    if(abs(T[i][a]-T[j][b])<diff) solver.add_clause(i, a, j, b);
        return solver.solve();
}
int main()
{
    while(~scanf("%d", &n)){
        int L = 0, R = -1;
        for(int i=0; i<n; i++){
            for(int j=0; j<2; j++){
                scanf("%d", &T[i][j]);
                R = max(R, T[i][j]);
            }
        }
        while(L<R){
            solver.init();
            int M = L+(R-L+1)/2;//M是向右靠近的
            if(judge(M)) L = M;
            else R = M-1;
            //cout<<R<<endl;
        }
        cout<<L<<endl;
    }
    return 0;
}

未解决的问题

本文标题:2-SAT

文章作者:Babydragon

发布时间:2018-03-13, 10:03:30

最后更新:2018-03-23, 13:30:48

原始链接:http://baolintian.github.io/2018/03/13/2-SAT/

许可协议: "署名-非商用-相同方式共享 4.0" 转载请保留原文链接及作者。

文章目录
  1. 1. 2-SAT
  2. 2. 题目
  3. 3. 题意
  4. 4. 题解
  5. 5. AC代码
  6. 6. 未解决的问题
{{ live2d() }}