2-sat模板

Posted on | In ,

2-sat用于解决这样一类问题：给出n个二元组，每个二元组必选出一个元素，而这些元素间可能有互斥的情况，要求给出合理方案。我们可以知道，对于二元组，如果因为被排斥而不选择某个元素，那么意味着必定选择另一个，这就使得问题可解，3-sat及以上似乎没有多项式算法……？

tarjan方法

利用tarjan算法求出每个点所属scc，如果二元组两个点位于同一个scc中则无解。输出方案时，输出两点中scc编号较小的一个即可，因为它处在这个dag的下游。上游点则会达到下游的点。

例题cf780d：n个俱乐部，两种选缩写方案，一种是俱乐部名字前三个字母，另一种是俱乐部名字前两个字母+城市首字母。

要求缩写不能有重复，且如果有俱乐部选择了方式2，那么不得有名字前三位相同的俱乐部采用方式1。求一种合法取名方案。

思路：每个俱乐部两种方案且各个方案间有互斥关系，故用2-sat解决，用这2n种方案建图，并根据规则连上对应的边。

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
82
83
84
85
86
#include<bits/stdc++.h>

using namespace std;

const int maxn=1e3+1;
struct edge{
    int to,next;
}es[maxn*maxn*4];
int cnt,n;
int head[maxn*2];
void add(int u,int v){
    es[++cnt]=(edge){v,head[u]};
    head[u]=cnt;
}

int stk[maxn*2];	//栈中存当前scc的点，可能也会存上一个scc的点
int dfn[maxn*2];//标号，dfs序
int low[maxn*2];//所属scc的最小标号
int scc[maxn*2];//某点属于哪个scc
bool in[maxn*2];//在栈中
int top,tot,ind;    //tot是强连通分量scc的个数
void tarjan(int x){
    stk[++top]=x;
    in[x]=1;
    dfn[x]=low[x]=++ind;
    for(int i=head[x];i;i=es[i].next){
        int v=es[i].to;
        if(!dfn[v]){
            tarjan(v);
            low[x]=min(low[x],low[v]);  //更新完v后回过头来用v更新x，之所以不用dfn[v]更新是因为dfn[v]大于dfn[x]
        }else if(in[v])
            low[x]=min(low[x],dfn[v]);	//如果发现可达点在栈中，说明已经和它形成环了，
    }
    if(dfn[x]==low[x]){
        tot++;
        do{
            scc[stk[top]]=tot;
            in[stk[top]]=0;
        }while(x!=stk[top--]);	//当=的时候，说明已经到逻辑栈底啦
    }
}
bool solve(){
    for(int i=1;i<=n*2;i++){
        if(!dfn[i]) tarjan(i);
    }
    for(int i=1;i<=n;i++){
        if(scc[i]==scc[i+n])
            return false;
    }
    return true;
}

inline int shift(int x){
    if(x>n) return x-n;
    return x+n;
}
string name[maxn*2];
int main(){
    cin>>n;
    string team,home;
    for(int i=1;i<=n;i++){
        cin>>team>>home;
        name[i]=team.substr(0,3);
        name[i+n]=team.substr(0,2)+home[0];
    }
    for(int i=1;i<=2*n;i++){
        for(int j=1;j<=2*n;j++){
            if(i==j) continue;
            if(name[i]==name[j]){
                add(i,shift(j));
                if(i<=n&&j<=n)
                    add(i+n,j+n);
            }
        }
    }
    if(solve()){
        printf("YES\n");
        for(int i=1;i<=n;i++){
            string res=(scc[i]<scc[i+n]?name[i]:name[i+n]);
            cout<<res<<endl;
        }
    }else{
        printf("NO\n");
    }
    return 0;
}

暴搜方法

思想类似，搜索某个点就意味着要选择某个点，那么搜进去第一步检查一下相对点是否被选择就可以了，如果选择了就直接返回false