【算法】2-sat問題【模板】

什么是2-sat問題

 有n個布爾型變量xi，另外m個需要滿足的條件。每個條件都是“xi為真/假或者xj為真/假”。這句話中的“或者”意味着兩個條件中至少有一個正確。2-sat問題的目標是給每個變量賦值，使得所有的條件得到滿足。

 算法的大致過程是這樣的：

  構造一張有向圖G，其中每個變量拆成兩個結點2i和2i+1，分別表示xi為假和xi為真。最后要為每個變量選其中一個結點標記。

  對於每個“xi為假或者xj為假"這樣的條件，我們連兩條對稱的有向邊。我們上面說過，或者意味着兩個中間至少有一個正確。所以如果xi為真的話，那么xj一定為假，所以我們從2*i+1向2*j連一條有向邊。同樣的道理，我們也從2*j+1向2*i連一條有向邊。

  接下來我們逐一考慮每個沒有賦值的變量，設為xi。我們先假定它為假，然后標記結點2i，並且沿着有向邊標記所有能標記的結點。如果標記的過程中發現某個變量對應的兩個結點都被標記，則xi假這個假定不成立，需要改為xi為真，然后重新標記。

  模板代碼如下

  code from LRJ

  

/*
將每個變量拆成兩個點2i和2i+1，分別表示xi為假和xi和真
對於每個條件，連兩條對稱的有向邊。
逐一考慮沒有賦值的變量，先假定它為假，然后標記結點2i，然后沿着有向邊標記所有能標記的結點
如果標記的過程中 發現某個變量對應的兩個結點都被標記，則xi為假這個假定不成立，需要改xi為真
然后重新標記
*/
#include <cstdio>
#include <cstring>
#include <algorithm>
#include <iostream>
#include <vector>

using namespace std;
const int maxn=100+10;
struct TwoSAT{
    int n;
    vector<int>G[2*maxn];
    bool mark[maxn*2];
    int S[maxn*2],c;
    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;
    }
    void init(int n){
        this->n=n;
        for(int i=0;i<n*2;i++)G[i].clear();
        memset(mark,0,sizeof(mark));
    }
    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);
    }

    bool solve(){
        for(int i=0;i<n*2;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;
    }
};
int main(){
return 0;
}