2-SAT 学习笔记

定义

SAT

维基百科——Boolean_satisfiability_problem

2-SAT

SAT 的简化版本：每个等式中只有两个变量参与。
有 个 变量和 个等式，每个等式形如 ，其中 是一个位运算。
你要求出一组可行解。

求解

将每个 拆成两个点 和 表示 取值情况。
每个限制都能被转化为形如 如果 为 那么 必须为 这样的限制。对于这样的限制，我们建立一条 到 的单向边，表示选了 必须选 。
然后跑强连通分量，每个强连通分量内的点代表了这整个分量要一起选。显然如果一个点的两个状态都在一个强连通分量里那么就无解。
考虑如何构造方案：我们按照逆拓扑序依次考虑每个点，如果能选就将这个强连通分量选上，并且将选出的点的另一种状态的点所在的强连通分量都 ban 掉，这是贪心先选取对全图影响小的强连通分量。
其实在 tarjan 求强连通分量的时候有一个小性质：求出的强连通分量的编号越大，这个分量的拓扑序就越小。

建图

把常见的三种情况写一下。

1. 如果 则
   建边 ，意思是如果 是 则 必须是 成立，那么逆否命题（ 不是 则 不是 ） 也成立。
2. 或 成立
   建边 。十分显然。如果一个不满足了那么另一个必须要满足。
3. 
   建边 ，这是情况 的特殊形式（ 或 成立）。
   实际意义是如果选择了 就必须选择 ，也就无解了，所以会被强制选择 。

例题

JSOI 2010 满汉全席

题意

道菜，每道菜可以做成汉族口味和满族口味。 个评委，每个评委会对两道不同的菜有要求。要求都是某个菜要做成什么口味。问是否存在一种方案，使得每个评委至少有一个要求被满足。 ,,。

题解

满族口味为 ，汉族口味为 ，就是建图中的情况二。

/*
 * Author: RainAir
 * Time: 2019-10-12 08:44:47
 */
#include <algorithm>
#include <iostream>
#include <cstring>
#include <climits>
#include <cstdlib>
#include <cstdio>
#include <bitset>
#include <vector>
#include <cmath>
#include <ctime>
#include <queue>
#include <stack>
#include <map>
#include <set>

#define fi first
#define se second
#define U unsigned
#define P std::pair
#define LL long long
#define pb push_back
#define MP std::make_pair
#define all(x) x.begin(),x.end()
#define CLR(i,a) memset(i,a,sizeof(i))
#define FOR(i,a,b) for(int i = a;i <= b;++i)
#define ROF(i,a,b) for(int i = a;i >= b;--i)
#define DEBUG(x) std::cerr << #x << '=' << x << std::endl

const int MAXN = 200+5;
const int MAXM = 2000+5;

struct Edge{
    int to,nxt;
}e[MAXM<<1];
int cnt,head[MAXN];

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

int n,m;
int dfn[MAXN],low[MAXN],col[MAXN];
int stk[MAXN],tp,tot;
bool ins[MAXN];
char a[23],b[23];

inline void dfs(int v){
    static int ts = 0;
    dfn[v] = low[v] = ++ts;ins[v] = true;stk[++tp] = v;
    for(int i = head[v];i;i = e[i].nxt){
        if(!dfn[e[i].to]){
            dfs(e[i].to);low[v] = std::min(low[v],low[e[i].to]);
        }
        else if(ins[e[i].to]) low[v] = std::min(low[v],dfn[e[i].to]);
    }
    if(low[v] == dfn[v]){
        int t = -1;++tot;
        do{
            t = stk[tp--];
            ins[t] = false;col[t] = tot;
        }while(t != v);
    }
}

inline void clear(){
    FOR(i,0,2*n) col[i] = ins[i] = head[i] = dfn[i] = low[i] = 0;cnt = tot = 0;
}

inline void Solve(){
    // m = 0,h = 1
    scanf("%d%d",&n,&m);
    FOR(i,1,m){
        scanf("%s%s",a+1,b+1);
        int ta = a[1]=='h',tb = b[1] == 'h';
        int len = strlen(a+1);int u = 0,v = 0;
        FOR(i,2,len) u = u*10+a[i]-'0';
        len = strlen(b+1);
        FOR(i,2,len) v = v*10+b[i]-'0';
        add(u+n*(!ta),v+n*tb);add(v+n*(!tb),u+n*ta);
    }
    FOR(i,1,2*n) if(!dfn[i]) dfs(i);
    FOR(i,1,n) if(col[i] == col[n+i]){
        puts("BAD");
        clear();
        return;
    }
    puts("GOOD");
    clear();
}

int main(){
    int T;scanf("%d",&T);
    while(T--) Solve();
    return 0;
}