2-Sat 算法

简介

什么是2-SAT呢？就是有一些集合，每个集合中有且仅有两个元素，同时每个集合需要选择一个作为代表，集合间的元素存在一定的选择关系，求解可行性及可行方案。

关键：连边(从"一定不能"中产生出"一定能")

2-SAT算法本身并不难，关键是连边，不过只需要充分理解好边的概念：a->b即选a必选b。
（也即连单向边）

a、b不能同时选：选了a就要选b’，选了b就要选a’。
a、b必须同时选：选了a就要选b，选了b就要选a，选了a’就要选b’，选了b’就要选a’。
a、b必须选一个：选了a就要选b’，选了b就要选a’，选了a’就要选b，选了b’就要选a。

从离散数学的角度讲

就是将题给的逻辑表达式转化为以蕴涵关系为主的逻辑表达式

例如：
a V b=¬a -> b 并且 ¬b -> a
（注意这里的“或”关系是指二选一而不是任选一）

具体实现

1. 利用DFS瞎搞，复杂度稍高，但是不影响AC题，优点在于可以得到指派的结果。

2. 利用SCC缩点，判断a和¬a是否在同一个强连通分量里，这种做法一般用于判断可行性，效率较高，但不适用于得出指派的结果。

模板题目

HDOJ 1814

自己的代码

#include<cstdio>
#include<algorithm>
#include<cstdlib>
#include<cmath>
#include<cstring>
#include<cctype>
#include<string>
#include<vector>
#include<queue>
#include<set>
#include<map>
#include<iostream>
using namespace std;

int n, m, cur; //cur表示某一次dfs的元素个数
vector<int> link[20000];
bool pp[20000];
int temp[20000]; //注意一定要把某一次dfs的元素全部都给记录下来， 便于回溯的时候把记录清零

bool dfs(int k) {
    if(pp[k^1]) return 0;
    if(pp[k]) return 1;
    temp[cur++]=k;
    pp[k]=1;
    for(int i=0; i<link[k].size(); ++i) {
        if(!dfs(link[k][i])) return 0;
    }
    return 1;
}

void print() {
    for(int i=0; i<2*n; ++i) {
        if(pp[i]) printf("%d\n", i+1);
    }
}
int main() {
    ios::sync_with_stdio(false);
    while(cin>>n>>m) {
        memset(pp,0,sizeof(pp));
        for(int i=0; i<20000; ++i) link[i].clear();
        for(int i=0; i<m; ++i) {
            int a, b;
            cin>>a>>b;
            a--, b--;
            link[a].push_back(b^1);
            link[b].push_back(a^1);
        }
        int f=1;
        for(int i=0; i<n; ++i) {
            int a=2*i, b=2*i+1;
            if(pp[a]||pp[b]) continue;
            cur=0;
            if(!dfs(a)) {
                while(cur) pp[temp[--cur]]=0;
                if(!dfs(b)) {
                    f=0;
                    printf("NIE\n");
                    break;
                }
            }
        }
        if(f) print();
    }
    return 0;
}

别人的代码

#include <iostream>
#include <cstdio>
#include <cstring>
#include <algorithm>
 
using namespace std;
 
const int maxn=100000;
 
struct Edge
{
    int to,next;
}edge[maxn];
 
int Adj[maxn],Size;
 
void init()
{
    Size=0; memset(Adj,-1,sizeof(Adj));
}
 
void Add_Edge(int u,int v)
{
    edge[Size].to=v;
    edge[Size].next=Adj[u];
    Adj[u]=Size++;
}
 
bool vis[maxn];
int top,S[maxn];
 
bool dfs(int x)
{
    if(vis[x^1]) return false;
    if(vis[x]) return true;
    S[top++]=x; vis[x]=true;
    for(int i=Adj[x];~i;i=edge[i].next)
    {
        if(!dfs(edge[i].to)) return false;
    }
    return true;
}
 
bool SAT2(int n)
{
    memset(vis,false,sizeof(vis));
    for(int i=0;i<n;i+=2)
    {
        if(vis[i]||vis[i^1]) continue;
        top=0;
        if(!dfs(i))
        {
            while(top) vis[S[--top]]=false;
            if(!dfs(i^1)) return false;
        }
    }
    return true;
}
 
int main()
{
    int n,m,a,b;
    while(scanf("%d%d",&n,&m)!=EOF)
    {
        init();
        while(m--)
        {
            scanf("%d%d",&a,&b);
            a--;b--;
            Add_Edge(a,b^1);
            Add_Edge(b,a^1);
        }
        bool t=SAT2(2*n);
        if(t)
        {
            for(int i=0;i<2*n;i++)
            {
                if(vis[i])
                    printf("%d\n",i+1);
            }
        }
        else puts("NIE");
    }
    return 0;
}