本篇文章主要是根據上屆一個東大學長謝文豔寫的一篇《給定2CNF可滿足性問題》自己重新總結了一下，然後把所有的程式碼都除錯了一遍，不過有一點要注意的是，文章中的方法能夠判斷問題是有具有解,能給出該問題的一種可行解，但並不能給出所有的解。

我自己總結為兩個部分，圖論問題和演算法的詳解。

一、將問題轉換為圖論問題 

首先，將2CNF的問題轉換為圖論問題。

下面的規則說明了如何把一個2CNF轉化為一個有向圖G=<V,E>：

u把2CNF的每個變數及這個變數的非都作為圖G的頂點。顯然若這個2CNF有3個變數，那麼將有6個頂點。

u   

第一步：首先為那些有到自己的非的有向路徑的變數賦值，即如果圖G

中有從x到的有向路徑，那麼將變數x賦值為false。如果圖G中有從到x的有向路徑，則將變數x賦值為true。將在這個步驟中被賦了值的變數稱為一級變數。

如下所示：

第二步：依次從與每一個一級變數對應的節點出發(如果一級變數x被賦值為true，則從與x對應的節點出發；如果x被賦值為false, 則從與對應的節點出發)，將所有能到達的、還沒有被賦值的節點賦值為true(如果該節點對應於y,則將y賦值為true；如果該節點對應於,則將y賦值為false)。將在這個步驟中被賦了值的變數稱為二級變數。

如下所示：

第三步：依次檢查還沒有被賦值的變數，如s，如果與s對應的頂點出度不為0(

有指向其它節點的有向邊)，則將s賦值為true，然後從與s對應的頂點出發，將所有能到達的、還沒有被賦值的節點賦值為true；如果與s對應的頂點出度為0，則將s賦值為false，從與s對應的頂點出發，將所有能到達的、還沒有被賦值的節點賦值為true。將在這個步驟中被賦了值的變數稱為三級變數。

如下所示：

    

二、演算法的詳解

1.先構圖，並將圖表示為鄰接矩陣。思想主要是將每一個字句用鄰接矩陣edges表示,如字句xUy，輸入的時候表示為：1 1。然後，將該字句表示 在資料結構中表示為edges[n+1][2]=1以及edges[2][n+1]=1

2.並找出一級變數。主要思想是呼叫

isSatisfiable函式，利用廣度優先從頂點i到頂點n+i看看是否能走通，同時，也判斷從頂點n+i到頂點i,如果都走通了，說明誤解，否則判定這n個點後，不存在兩個條件都滿足的情況，則表示有解了。同時，在判斷的過程中，找出一級變數。

 Boolean isSatisfiable() { for (int i = 0; i < varCount; i++) { boolean iToNegi = hasPathTo(i, varCount + i); boolean negiToi = hasPathTo(varCount + i, i); if (iToNegi && negiToi) { return false; } if (iToNegi) { // there is a path from i to negative i,in this case, we can // only assign false to variable i // use 4 to indicate that i is LEVEL 1 variable and its value is // false assignments[i] = 4; determinedCount++; // It also means y and negative y can't both appear in the // reachable vertices of negative i. } else if (negiToi) { // there is a path from negative i to i,in this case, we can // only assign // true to variable i // use 5 to indicate that i is LEVEL 1 variable and its value is // true assignments[i] = 5; determinedCount++; // It also means y and negative y can't both appear in the // reachable vertices of i. } } return true; }

3.找出二級變數和三級變數。從每一個一級變量出發，根據原則，利用廣度優先的演算法，把所有能達到的變數變為true，這些變數就是二級變量了。然後再獲取三級變數，通過一個迴圈，將沒有訪問過的變數，利用的原則來將所有的所能達到的置為true。

 public int[] getAssignments() { if (determinedCount == varCount) { // all the variables' value have been pre-determined in // isSatisfiable() function. normalizeValues(); return assignments; } // to determine the values of LEVEL 2 variables. for (int i = 0; i < varCount; i++) { if (assignments[i] == 4) { // start from vertex -i. // use 2 (3) to indicate the variables is in LEVEL 2 and // its value is false (true) boolean finished = toDetermineOtherVar(varCount + i, 2, 3); if (finished) { normalizeValues(); return assignments; } } else if (assignments[i] == 5) { // start from vertex i. boolean finished = toDetermineOtherVar(i, 2, 3); if (finished) { normalizeValues(); return assignments; } } }

4.自此，演算法結束，輸出所有變數的值。（注意：該演算法只能獲得一組可行解，但不能獲得所有的解）

 

如果輸入：  

格式如下：

4 3//第一個引數是行數第二個是變數個數

//記下來是字句輸入如表示為-1 2

-1 2

-2 3

1 -3

3 2

得出結果：

有可行解

1:1

2:1

3:1

又例如輸入：

得出結果：

1:1 //X1:1
2:0 //x2:0
3:0 //x3:0
4:1 //x4:1
5:0 //x5:0