2-SAT問題總結

2-SAT問題總結

       2-SAT問題：n個布爾型的變量，給出m個約束條件，約束條件例如：A，B不能同時為真，A，B必須同時為真等。

       看了算法入門經典中的解決辦法，關於這種解決辦法比較容易理解，並且效率也不錯。構造一張有向圖G，其中n個變量拆成n*2個變量，也就是xi用xi*2和xi*2+1表示，如果前者標記為1，那么說明xi為真，如果后者標記為1，那么說明xi為假。對於約束條件就可進行構成邊，例如xi為假或者xj為假，也就是xi為假xj必須為真，xj為假xi必須為真，這樣就得到兩條有向邊，xi*2+1 -> xj*2    xj*2+1 -> xi*2,這樣就得到了有向圖G。

       有向圖中所有的有向邊肯定組成了若干連通分量，某一連通分量中的，一點如果為1那么，這個連通分量中的所有點都要是1，反之也是，如果某一點既為1，又為0，那么m個約束條件肯定是產生矛盾了，那么這個問題就無法解決。

       模擬這個過程的時候用的是dfs，從一點開始我們先假設這個點為0，然后從這個點開始遍歷所有它能到達的點，都標記一下，如果標記過程中發現某點已經為1了，那么就以這個點為1再以這個點開始遍歷，如果這個點為1為0都會產生矛盾，那么就是出現了上面的問題，約束條件產生矛盾，問題無法得到解決。

/*********************************************2-SAT模板*********************************************/
const int maxn=10000+10;
struct TwoSAT
{
    int n;//原始圖的節點數(未翻倍)
    vector<int> G[maxn*2];//G[i].j表示如果mark[i]=true,那么mark[j]也要=true
    bool mark[maxn*2];//標記
    int S[maxn*2],c;//S和c用來記錄一次dfs遍歷的所有節點編號

    //從x執行dfs遍歷,途徑的所有點都標記
    //如果不能標記,那么返回false
    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<2*n;i++) 
            G[i].clear();
        memset(mark,0,sizeof(mark));
    }

    //加入(x,xval)或(y,yval)條件
    //xval=0表示假，yval=1表示真
    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);
    }

    //判斷當前2-SAT問題是否有解
    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[S[--c]]=false;
                if(!dfs(i+1)) return false;
            }
        }
        return true;
    }
};
/*********************************************2-SAT模板*********************************************/