-------------------------------------------------對於2-sat問題的描述-------------------------------------------------

給出一個序列，每個數是一個bool值，給出一些限制關係，得到最終的可行解的問題叫做適應性問題，也就是sat問題，2-sat問題就是給出的限制最多是兩兩元素之間的限制。

這種適應性問題的解決，同樣是能夠抽象為我們已知的圖論模型的。

--------------------------------------------------2-sat問題的建圖方法--------------------------------------------------

1.我們利用一條有向邊<i,j>，來表示選i的情況下，一定要選j;

2.用i表示某個點是true,那麼i'表示某個點是false

3.因為限制的兩兩之間的關係，所以我們可以通過邏輯關係來建邊：

          1）如果給出A和B的限制關係，A和B必須一起選，(A and B)||(!A and !B )==true 那麼選A必須選B，建邊<i,j>和<j,i>還有<i',j'>和<j',i'>

          2）如果給出A和B的限制關係，選A不能選B，那麼(A && !B)||(!A && B )==true,建邊<i,j'>和<j,i'>

          3）如果必須選A,那麼A==true,建邊<i',i>

          4）如果A一定不能選，那麼!A==true.建邊<i,i'>

這麼建圖之後，會出現一個有向圖，這個有向圖會導致一個連通環，導致某個點一旦選取，那麼這條鏈上的所有點都要被選中。如果我們找到一個強連通分量，那麼這個強連通分量當中的點，如果選取必須全部選取，不選取的話一定是全部不選取，所以只要滿足這個有向圖中連通的點不會導致i和i'同時被選取，如果不存在矛盾，那麼當前問題就是有解的。但是往往在求解過程中，我們要求的解會要求一些性質，所以提供以下幾種解決方案。

------------------------------------------------2-sat問題的解決方案--------------------------------------------------------

1.求字典序最小的解的方法：

暴力dfs求解（複雜度O(N*M)）

2.判斷當前的2-sa問題t是否有解

tarjan強連通縮點，加判斷（複雜度O(N+M)）

3.求出當前的2-sat問題的任意一組解

tarjan強連通縮點+拓撲排序+構建一組解（複雜度O（N+M)）

------------------------------------------------求字典序最小的解的暴力方法---------------------------------------------

演算法思想：

1.首先定義我們需要用到的陣列，mark陣列用來標記某個點是否被選取，對於序列中的一個數我們會拆成兩個點i和i'，所以我們在利用mark陣列進行標記的時候，採用如下這種標記方法：

mark[i<<1]表示i,而mark[i<<1|1]表示i'

一個用來存本次標記過的點的一個佇列s

2.列舉每個點，然後判斷當前點拆出的兩個點是否已經有其中一個被選取，如果有的話，那麼繼續列舉下一個點，如果沒有被標記，那麼轉到操作3

3.如果某一點拆出的兩個點都沒有被標記，那麼我們先嚐試標記第一個點，因為如果標記第一個點會導致一些點必須被標記，所以要進行dfs,然後判斷過程中會不會出現矛盾的情況，如果出現了，那麼將本次標記的點全部還原，然後就剩下第二個點一種情況，所以我們檢視第二種情況，判斷會不會出現，，如果出現矛盾，那麼問題無解，結束演算法如果當前成功標記，那麼繼續像2那樣列舉，直至列舉過所有的點演算法結束。

4.因為每次dfs的過程會把所有當前點可達的點都進行標記，所以之後每次標記的過程中，因為已經標記的點，有一個不選的話，那麼代表所有的點均不選，且會導致與它同源的那個點一定被選，所以一旦被選中，不能導致出現有解的情況，那麼當前情況一定無解，因為每次做的操作只可能會導致圖上的點不變或者整體顏色反轉，所以只需要讓新染色的點兩種選擇即可，因為得到的結果只有兩種，而且同時做反轉操作與沒做的效果是一樣的。

5.因為是按照深搜序做的，所以得到解一定是字典序最小的。

程式碼如下：

這個程式碼是我測過的，我保證。。。。。。

struct TwoSat  
{  
    int n;  
    vector<int> e[MAX<<1];  
    int s[MAX<<1],c;  
    bool mark[MAX<<1];  
    //mark[i<<1]陣列等於1，表示點i被選擇  
    //mark[i<<1|1]陣列等於1，表示點i沒有被選擇  
    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 <e[x].size() ; i++ )  
            if ( !dfs( e[x][i] ))  
                return false;  
        return true;  
    }  
  
    void init ( int n )  
    {  
        this->n = n;  
        for ( int i = 0 ; i < 2*n ; i++ )  
            e[i].clear();  
        memset ( mark , 0 , sizeof ( mark ));  
    }  
  
    void add ( int x , int y )  
    {  
        e[x].push_back ( y^1 ); //建邊操作考慮實際情況修改
        e[y].push_back ( x^1 );  
    }  
  
    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問題是否有解-----------------------------------------------

演算法思想：

1.利用強連通縮點得到一個DAG（有向無環圖）;

2.然後對於每個強連通分量當中，所有點都是選就一起選，不選就一起不選的，所以如果i和i'同時存在一個強連通分量裡，就一定無解

3.如果強連通分量內部不出現矛盾，那麼剩下的就是這個有向無環圖，因為有向無環圖，可以進行拓撲排序，所以只需要交替的染不同的顏色，就能夠得到一個解，所以只要強連通分量內部不出現矛盾，那麼久一定有解

主體程式碼如下：

 for ( int i = 0 ; i < 2*n ; i++ )  
        if ( !mark[i] ) tarjan ( i );  
  
    for ( int i = 0 ; i < n ; i++ )  
        if ( belong[i<<1] == belong[i<<1|1] )  
            return false;  
    return true;  

void tarjan ( int u )  
{  
    dfn[u] = low[u] = ++times;  
    mark[u] = 1;  
    s.push ( u );  
    int len = e[u].size();  
    for ( int i= 0 ; i < len ; i++ )  
    {  
        int v = e[u][i];  
        if ( !mark[v] )  
        {  
            tarjan ( v );  
            low[u] = min ( low[u] , low[v] );  
        }  
        if ( mark[v] == 1 )  
            low[u] = min ( low[u] , dfn[v] );  
    }  
    if ( dfn[u] == low[u] )  
    {  
        int temp;  
        do  
        {  
            temp = s.top();  
            belong[temp] = cnt;  
            mark[temp] = 2;  
            s.pop();  
        }while ( temp != u );  
        cnt++;  
    }  
}  

1.首先依舊要進行強連通縮點，我們得到一個DAG

2.然後我們要得到新得到的圖中的矛盾關係，也就是i和i'所在的強連通分量是矛盾的。

3.然後我們對DAG進行染色，在拓撲排序的過程中進行染色，如果某個點沒有染色，那麼染為1，並且將與他矛盾的點染為2，因為矛盾關係是兩兩之間的，所以不會與其他點出現矛盾。

4.那麼在拓撲排序結束之後就對所有點進行完染色了。拓撲只是在有向無環圖中的一種很好的遍歷方式

程式碼如下：

void topsort ( )  
{  
    int i,j;  
    queue<int> q;  
    for ( int i = 1 ; i < t ; i++ )  
    {  
        if (!in[i])  
            q.push ( i );  
    }  
    while (!q.empty())  
    {  
        int u = q.front();  
        q.pop();  
        if ( !col[u] )  
        {  
            col[u] = 1;  
            col[conflict[u]] = 2;  
        }  
        for ( int i = 0 ; i < g[u].size(); i++ )  
        {  
            int v = g[u][i];  
            in[v]--;  
            if ( !in[v] ) q.push ( v );  
        }  
    }  
}