問題描述：

現有一個由N個布爾值組成的序列A，給出一些限制關系，比如A[x]AND A[y]=0、A[x] OR A[y] OR A[z]=1等，要確定A[0..N-1]的值，使得其滿足所有限制關系。這個稱為SAT問題，特別的，若每種限制關系中最多只對兩個元素進行限制，則稱為2-SAT問題。

由于在2-SAT問題中，最多只對兩個元素進行限制，所以可能的限制關系共有11種：

????????A[x]

????????NOT A[x]???

????????A[x] AND A[y]

????????A[x]? AND NOT A[y]

????????A[x] OR A[y]

????????A[x] OR NOT A[y]

????????NOT (A[x] AND A[y])

????????NOT (A[x] OR A[y])

????????A[x] XOR A[y]

????????NOT (A[x] XOR A[y])

????????A[x] XOR NOT A[y]

進一步，3可以用1表示：A[x]，A[y]，NOT(A[x] XOR A[y]) 相當于 NOT A[x] AND? NOT A[y]。狄摩根定律。只剩下了9中基本關系類型。

在實際問題中，2-SAT問題在大多數時候表現成以下形式：有N對物品，每對物品中必須選取一個，也只能選取一個，并且它們之間存在某些限制關系（如某兩個物品不能都選，某兩個物品不能都不選，某兩個物品必須且只能選一個，某個物品必選）等，這時，可以將每對物品當成一個布爾值（選取第一個物品相當于0，選取第二個相當于1），如果所有的限制關系最多只對兩個物品進行限制，則它們都可以轉化成9種基本限制關系，從而轉化為2-SAT模型。

(引自：http://www.cnblogs.com/kuangbin/archive/2012/10/05/2712429.html)

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」拆開。SAT 是 Satisfiability 的縮寫，意為可滿足性。即一串布爾變量，每個變量只能為真或假。要求對這些變量進行賦值，滿足布爾方程。

舉個例子：教練正在講授一個算法，代碼要給教室中的多位同學閱讀，代碼的碼風要滿足所有學生。假設教室當中有三位學生：Anguei、Anfangen、Zachary_260325?，F在他們每人有如下要求：

• Anguei: 我要求代碼當中滿足下列條件之一：
• 不寫?using namespace std;?（ ?a）
• 使用讀入優化 （b）
• 大括號不換行 （ ?c）
• Anfangen: 我要求代碼當中滿足下條件之一：
• 寫?using namespace std;?（a）
• 使用讀入優化 （b）
• 大括號不換行 （）
• Zachary_260325：我要求代碼當中滿足下條件之一：
• 不寫?using namespace std;?（）
• 使用?scanf?（）
• 大括號換行 （c）

我們不妨把三種要求設為?a,b,ca,b,c，變量前加?\neg??表示「不」，即「假」。上述條件翻譯成布爾方程即：。其中，表示或，表示與。?

現在要做的是，為 ABC 三個變量賦值，滿足三位學生的要求。

Q: 這可怎么賦值啊？暴力？

A: 對，這是 SAT 問題，已被證明為?NP 完全?的，只能暴力。

Q: 那么 2-SAT 是什么呢？

A: 2-SAT，即每位同學?只有兩個條件（比如三位同學都對大括號是否換行不做要求，這就少了一個條件）不過，仍要使所有同學得到滿足。于是，以上布爾方程當中的?c,,?c?沒了，變成了這個樣子：

公式殺招：

?

?

怎么求解 2-SAT 問題？

使用強連通分量。?對于每個變量?xx，我們建立兩個點：x ,?x?分別表示變量?xx?取?true?和取?false。所以，圖的節點個數是兩倍的變量個數。在存儲方式上，可以給第?ii?個變量標號為?ii，其對應的反值標號為?i + ni+n。對于每個同學的要求? (a∨b)，轉換為? ?a→b∧?b→a。對于這個式子，可以理解為：「若?aa?假則?bb?必真，若?bb?假則?aa?必真」然后按照箭頭的方向建有向邊就好了。綜上，我們這樣對上面的方程建圖：

原式建圖

	?a→b∧?b→?a
	??a→b∧?b→a
	?a→?b∧b→?a

于是我們得到了這么一張圖：

可以看到，?a?與?b?在同一強連通分量內，a與 ?b?在同一強連通分量內。同一強連通分量內的變量值一定是相等的。也就是說，如果?x?與??x?在同一強連通分量內部，一定無解。反之，就一定有解了。

但是，對于一組布爾方程，可能會有多組解同時成立。要怎樣判斷給每個布爾變量賦的值是否恰好構成一組解呢？

這個很簡單，只需要?當?xx?所在的強連通分量的拓撲序在?\neg x?x?所在的強連通分量的拓撲序之后取?xx?為真?就可以了。在使用 Tarjan 算法縮點找強連通分量的過程中，已經為每組強連通分量標記好順序了——不過是反著的拓撲序。所以一定要寫成?color[x] < color[-x]?。

代碼實現：

//暴力DFS，求字典序最小的解，也是求字典序唯一的方法 #include<cstdio> #include<cstring> #include<vector> using namespace std; const int maxn=10000+10; struct TwoSAT {int n;//原始圖的節點數(未翻倍)vector<int> G[maxn*2];//G[i]==j表示如果mark[i]=true,那么mark[j]也要=truebool mark[maxn*2];//標記int S[maxn*2],c;//S和c用來記錄一次dfs遍歷的所有節點編號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);}//從x執行dfs遍歷,途徑的所有點都標記//如果不能標記,那么返回falsebool 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;}//判斷當前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;} }; //聯通分量+拓撲排序，求任意意一組解，比較快#include <cstdio> #include <cstring> #include <queue> #include <vector> #include <stack> #include <algorithm> #define MAXN 2000+10 #define MAXM 400000 #define INF 1000000 using namespace std; vector<int> G[MAXN]; int low[MAXN], dfn[MAXN]; int dfs_clock; int sccno[MAXN], scc_cnt; stack<int> S; bool Instack[MAXN]; int N, M; void init() {for(int i = 0; i < 2*N; i++) G[i].clear(); } void getMap() {int a, b, c;char op[10];while(M--){scanf("%d%d%d%s", &a, &b, &c, op);switch(op[0]){case 'A': if(c == 1)//a,b取1 {G[a + N].push_back(a);G[b + N].push_back(b);}else//a,b至少一個不為真 {G[a].push_back(b + N);G[b].push_back(a + N);}break;case 'O':if(c == 1)//a,b最少有一個為真 {G[b + N].push_back(a);G[a + N].push_back(b);}else//a,b都為假 {G[a].push_back(a + N);G[b].push_back(b + N);}break;case 'X':if(c == 1)//a b 不同值 {G[a + N].push_back(b);G[a].push_back(b + N);G[b].push_back(a + N);G[b + N].push_back(a);}else//a b 同真同假 {G[a].push_back(b);G[b].push_back(a);G[a + N].push_back(b + N);G[b + N].push_back(a + N);}}} } void tarjan(int u, int fa) {int v;low[u] = dfn[u] = ++dfs_clock;S.push(u);Instack[u] = true;for(int i = 0; i < G[u].size(); i++){v = G[u][i];if(!dfn[v]){tarjan(v, u);low[u] = min(low[u], low[v]);}else if(Instack[v])low[u] = min(low[u], dfn[v]);}if(low[u] == dfn[u]){scc_cnt++;for(;;){v = S.top(); S.pop();Instack[v] = false;sccno[v] = scc_cnt;if(v == u) break; }} } void find_cut(int l, int r) {memset(low, 0, sizeof(low));memset(dfn, 0, sizeof(dfn));memset(sccno, 0, sizeof(sccno));memset(Instack, false, sizeof(Instack));dfs_clock = scc_cnt = 0;for(int i = l; i <= r; i++)if(!dfn[i]) tarjan(i, -1); } void solve() {for(int i = 0; i < N; i++){if(sccno[i] == sccno[i + N]){printf("NO\n");return ;}}printf("YES\n"); } int main() {while(scanf("%d%d", &N, &M) != EOF){init();getMap();find_cut(0, 2*N-1);solve();}return 0; }

?

總結

以上是生活随笔為你收集整理的图论--2-SAT--详解的全部內容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。