本篇文章主要是根据上届一个东大学长谢文艳写的一篇《给定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:12:0 //x2:03:0 //x3:04:1 //x4:15:0 //x5:0
点击这里下载完整代码
若有问题欢迎发邮件给我：chen-hongqin@163.com
