公布一个3－CNF-SAT函数的所有解

姜咏江

   为了证实我创造的子句消去法求解k-CNF-SAT的真实有效性，特给出一个6个逻辑变量的3-CNF-SAT函数求解实例，希望读者能够通过这个实例的全部解求出，更好地理解子句消去法的正确性。

f(x₁,..., x₆)= (x₁+x₁'+x₂')(x₂+x₃+x₄)(x₁'+x₃'+x₄')(x₁'+x₂+x₅')(x₂+x₃+x₆)(x₁+x₅+x₆')。

   这个合取范式是否有值为1的解？共有多少？都是什么？用子句消去法很快就可以求出来。

   我将这些解罗列出来，是否正确，读者可以任选一组6元二进制数进行检验，看看我给的那些二进制数是不是都是解。此外，读者可以任意给出不在其中的6位二进制数，进行验证，看看它们是否使f(x₁,..., x₆)=0。

   通过子句消去法，得到这个合取范式成立的解集合如下：

000010，000011，000100，000101，000110，

000111，001010，001011，001100，001110，

010010，010011，010100，010110，010111，

011010，011011，011100，011110，100011，

100101，100111，101001，101011，110010，

110011，110100，110110，110111，111000，

111010，111011，111100，111110。

   以上共计34个解。

验证在解集合中的数：(x6,x5,x4,x3,x2,x1) = 011110，得：

f(x₁,..., x₆)= (0+1+0)(1+1+1)(1+0+0)(1+1+0)(1+1+0)(0+1+1)=1。

验证不在解集合中的数：(x6,x5,x4,x3,x2,x1) = 011111，得:

      f(x₁,..., x₆)= (1+0+0)(1+1+1)(0+0+0)(0+1+0)(1+1+0)(1+1+1)=0。

   可见不在解集合中的6位二进制数会使某个合取范式的子句为0，因而造成无解，使此3-CNF-SAT不满足。

2015-7-8