博文
SAT问题满足解详解求解例题
||||
SAT问题满足解详解求解例题
姜咏江
从一开始接触SAT问题求解，我就说过：“科学网是我科研的地方。”两年，我在科学网上经历了与别人不一样的研究历程，当然，也收获了与别人不一样的成果。我以3-SAT问题求解的实例，来详细告诉感兴趣的人们，如何在多项式时间内求出这类SAT问题满足解。这是对以往阅读过我那些不成熟博文人们的辛苦的回报。
消去块中唯一解，
不然找一可选解，
解多暂时一边放，
全多选解可得解。
这四句是我总结出求SAT满足解的口诀，在下面的实例中我会一一地解释。
例题：
3-CNF=(x1+x2’ +x20’) (x1’ +x2+x20’) (x1+x4’ +x6’) (x1’ +x4’ +x6) (x1+x4’ +x6) (x1+x4+x6’) (x1+x2+x4') (x1’+x2+x4) (x2’+x9+x15’) (x2+x9’+x15’) (x2’+x9+x15’) (x2’ +x4+x6) (x2+x4’+x6) (x2+x4+x6) (x2’ +x4’+x6) (x2’+x4’+x6’) (x3’+x4’+x5’) (x3+x4+x5’) (x3’+x4’+x5) (x4+x12+x14) (x4’+x12’ +x14’) (x4+x5’ +x6’) (x4+x5+x6’) (x5’+x6’+x8’) (x5+x6+x8’) (x5+x6’+x8) (x5+x6’ +x10) (x5+x6+x10) (x5’+x6+x10) (x5+x6’ +x10’) (x5’ +x6’ +x9’) (x5+x6’+x9’) (x5+x6+x9’) (x5’+x6+x9) (x5+x6’+x9) (x6+x8’+x11) (x6’+x8+x11) (x7+x14+x18) (x7+x14’+x18’) (x7+x8’+x11’) (x7+x8+x11) (x1’ +x9’ +x12) (x1’ +x9+x12’) (x1+x9+x12’) (x1+x9’ +x12) (x11’ +x12’ +x14) (x11+x12’ +x14’) (x11+x12+x14) (x13’ +x15’ +x17’) (x13’ +x15+x17) (x13+x15’ +x17) (x13+x15+x17’) (x16’ +x17’ +x18’) (x16+x17+x18) (x17’ +x18’ +x19’) (x17+x18’ +x19’) (x18’ +x19’ +x20’) (x18+x19+x20)
这61个子句用表的形式表示出来如表1所示，1代表变量本身，0表示变量的非形式。
表1 3-SAT
x1 | x2 | x3 | x4 | x5 | x6 | x7 | x8 | x9 | x10 | x11 | x12 | x13 | x14 | x15 | x16 | x17 | x18 | x19 | x20 |
1 | 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 |
0 | 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 |
1 |
|
| 0 |
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
0 |
|
| 0 |
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
1 |
|
| 0 |
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
1 |
|
| 1 |
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
1 | 1 |
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
0 | 1 |
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 |
|
|
|
|
|
| 1 |
|
|
|
|
| 0 |
|
|
|
|
|
| 1 |
|
|
|
|
|
| 0 |
|
|
|
|
| 0 |
|
|
|
|
|
| 1 |
|
|
|
|
|
| 0 |
|
|
|
|
| 1 |
|
|
|
|
|
| 0 |
| 1 |
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
| 0 |
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
| 1 |
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 |
| 0 |
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 |
| 0 |
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 | 0 | 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 1 | 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 | 0 | 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
|
|
|
|
|
|
| 1 |
| 1 |
|
|
|
|
|
|
|
|
| 0 |
|
|
|
|
|
|
| 0 |
| 0 |
|
|
|
|
|
|
|
|
| 1 | 0 | 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 1 | 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 | 0 |
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 1 |
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 0 |
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 0 |
|
|
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 1 |
|
|
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 | 1 |
|
|
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 0 |
|
|
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 | 0 |
|
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 0 |
|
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 1 |
|
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 | 1 |
|
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 0 |
|
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
| 0 |
|
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 |
| 1 |
|
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
|
|
|
|
|
| 1 |
|
|
| 1 |
|
|
|
|
|
|
|
| 1 |
|
|
|
|
|
| 0 |
|
|
| 0 |
|
|
|
|
|
|
|
| 1 | 0 |
|
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 1 |
|
| 1 |
|
|
|
|
|
|
|
|
|
0 |
|
|
|
|
|
|
| 0 |
|
| 1 |
|
|
|
|
|
|
|
|
0 |
|
|
|
|
|
|
| 1 |
|
| 0 |
|
|
|
|
|
|
|
|
1 |
|
|
|
|
|
|
| 1 |
|
| 0 |
|
|
|
|
|
|
|
|
1 |
|
|
|
|
|
|
| 0 |
|
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 | 0 |
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 0 |
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 1 |
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 |
| 0 |
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 |
| 1 |
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
| 0 |
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
| 1 |
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 | 0 | 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 1 | 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 | 0 | 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 0 | 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 | 0 | 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 1 | 1 |
1. 消去块中唯一解
判断变量有唯一解的条件是k阶子句块的变量x有2k-1个“0”或“1”，如果同时有2k-1个“0”和“1”，则SAT无满足解。
子句块x2x4x6有唯一解x6=1，消去x6=1的所有子句。发现剩余2阶子句块的变量有唯一解（见表2中黄色底纹所示）。
表2 消去x6=1的所有子句的剩余
|
|
|
|
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
x1 | x2 | x3 | x4 | x5 | x6 | x7 | x8 | x9 | x10 | x11 | x12 | x13 | x14 | x15 | x16 | x17 | x18 | x19 | x20 |
1 | 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 |
0 | 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 |
1 |
|
| 0 |
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
1 |
|
| 1 |
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
1 | 1 |
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
0 | 1 |
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 |
|
|
|
|
|
| 1 |
|
|
|
|
| 0 |
|
|
|
|
|
| 1 |
|
|
|
|
|
| 0 |
|
|
|
|
| 0 |
|
|
|
|
|
| 1 |
|
|
|
|
|
| 0 |
|
|
|
|
| 1 |
|
|
|
|
|
| 0 |
| 0 |
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 | 0 | 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 1 | 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 | 0 | 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
|
|
|
|
|
|
| 1 |
| 1 |
|
|
|
|
|
|
|
|
| 0 |
|
|
|
|
|
|
| 0 |
| 0 |
|
|
|
|
|
|
|
|
| 1 | 0 | 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 1 | 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 | 0 |
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 0 |
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 0 |
|
|
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 0 |
|
|
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 | 0 |
|
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 0 |
|
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 0 |
|
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 |
| 1 |
|
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
|
|
|
|
|
| 1 |
|
|
| 1 |
|
|
|
|
|
|
|
| 1 |
|
|
|
|
|
| 0 |
|
|
| 0 |
|
|
|
|
|
|
|
| 1 | 0 |
|
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 1 |
|
| 1 |
|
|
|
|
|
|
|
|
|
0 |
|
|
|
|
|
|
| 0 |
|
| 1 |
|
|
|
|
|
|
|
|
0 |
|
|
|
|
|
|
| 1 |
|
| 0 |
|
|
|
|
|
|
|
|
1 |
|
|
|
|
|
|
| 1 |
|
| 0 |
|
|
|
|
|
|
|
|
1 |
|
|
|
|
|
|
| 0 |
|
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 | 0 |
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 0 |
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 1 |
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 |
| 0 |
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 |
| 1 |
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
| 0 |
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
| 1 |
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 | 0 | 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 1 | 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 | 0 | 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 0 | 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 | 0 | 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 1 | 1 |
表3 出现一阶剩余子句块
1 |
|
| 1 | 1 | 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
x1 | x2 | x3 | x4 | x5 | x6 | x7 | x8 | x9 | x10 | x11 | x12 | x13 | x14 | x15 | x16 | x17 | x18 | x19 | x20 |
0 | 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 |
| 0 |
|
|
|
|
|
| 1 |
|
|
|
|
| 0 |
|
|
|
|
|
| 1 |
|
|
|
|
|
| 0 |
|
|
|
|
| 0 |
|
|
|
|
|
| 1 |
|
|
|
|
|
| 0 |
|
|
|
|
| 1 |
|
|
|
|
|
| 0 |
| 0 |
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 | 0 | 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 |
|
|
|
|
|
|
| 0 |
| 0 |
|
|
|
|
|
|
|
|
|
| 0 | 0 |
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 | 0 |
|
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 |
| 1 |
|
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
|
|
|
|
|
| 1 |
|
|
| 1 |
|
|
|
|
|
|
|
| 1 |
|
|
|
|
|
| 0 |
|
|
| 0 |
|
|
|
|
|
|
|
| 1 | 0 |
|
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 1 |
|
| 1 |
|
|
|
|
|
|
|
|
|
0 |
|
|
|
|
|
|
| 0 |
|
| 1 |
|
|
|
|
|
|
|
|
0 |
|
|
|
|
|
|
| 1 |
|
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 | 0 |
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 0 |
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 1 |
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 |
| 0 |
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 |
| 1 |
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
| 0 |
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
| 1 |
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 | 0 | 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 1 | 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 | 0 | 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 0 | 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 | 0 | 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 1 | 1 |
表4 又出现一阶剩余子句块
1 | 0 | 0 | 1 | 1 | 1 |
| 0 | 0 |
|
|
|
|
|
|
|
|
|
|
|
x1 | x2 | x3 | x4 | x5 | x6 | x7 | x8 | x9 | x10 | x11 | x12 | x13 | x14 | x15 | x16 | x17 | x18 | x19 | x20 |
0 | 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 |
|
|
| 0 |
|
|
|
|
|
|
| 0 |
| 0 |
|
|
|
|
|
|
|
|
|
|
| 0 |
| 1 |
|
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
|
|
|
|
|
| 1 |
|
|
| 1 |
|
|
|
|
|
|
|
| 1 |
|
|
|
|
|
| 0 |
|
|
| 0 |
|
|
|
|
|
|
|
| 1 | 1 |
|
| 1 |
|
|
|
|
|
|
|
|
|
0 |
|
|
|
|
|
|
| 1 |
|
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 | 0 |
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 0 |
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 1 |
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 |
| 0 |
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 |
| 1 |
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
| 0 |
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
| 1 |
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 | 0 | 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 1 | 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 | 0 | 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 0 | 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 | 0 | 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 1 | 1 |
表5 变量x7=1可以消去子句
1 | 0 | 0 | 1 | 1 | 1 |
| 0 | 0 |
| 1 | 0 |
|
|
|
|
|
|
| 0 |
x1 | x2 | x3 | x4 | x5 | x6 | x7 | x8 | x9 | x10 | x11 | x12 | x13 | x14 | x15 | x16 | x17 | x18 | x19 | x20 |
|
|
|
|
|
| 1 |
|
|
|
|
|
| 1 |
|
|
| 1 |
|
|
|
|
|
|
|
| 1 |
|
|
|
|
|
| 0 |
|
|
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 |
| 0 |
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 |
| 1 |
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
| 0 |
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
| 1 |
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 | 0 | 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 1 | 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 | 0 | 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 0 | 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 1 | 1 |
表6 可以取任意值的变量和多解子句块
1 | 0 | 0 | 1 | 1 | 1 | 1 | 0 | 0 | * | 1 | 0 |
| * |
|
|
|
|
| 0 |
x1 | x2 | x3 | x4 | x5 | x6 | x7 | x8 | x9 | x10 | x11 | x12 | x13 | x14 | x15 | x16 | x17 | x18 | x19 | x20 |
|
|
|
|
|
|
|
|
|
|
|
| 0 |
| 0 |
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 |
| 1 |
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
| 0 |
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
| 1 |
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 | 0 | 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 1 | 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 | 0 | 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 0 | 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 1 | 1 |
2. 不然找一可选解
子句块全多解的情况，可以证明非关联变量一定有2个可选解。所以只需要对关联变量分别设定0和1值，然后施行子句消去法，碰到剩余子句块无解时，说明所设定的值不是这个变量的可选解。如果0和1都不是这个变量的可选解，那么SAT无解。如果判定只有一个0或1是可选解，那么就设定该变量的这个值，消去子句，然后从剩余的子句块中继续求解。
经过表7的判断操作，不巧其中无有唯一可选解的变量，知道此题剩余的这些变量都有2个可选解。
表7 判断变量可选解（纵向看）
|
|
| 0 |
|
|
|
|
|
|
| 0 | 1 |
|
|
|
|
| 1 | 0 |
x13 | x15 | x16 | x17 | x18 | x19 |
| x13 | x15 | x16 | x17 | x18 | x19 |
| x13 | x15 | x16 | x17 | x18 | x19 |
0 | 0 |
| 0 |
|
|
| 0 | 0 |
| 0 |
|
|
| 0 | 0 |
| 0 |
|
|
0 | 1 |
| 1 |
|
|
| 0 | 1 |
| 1 |
|
|
| 0 | 1 |
| 1 |
|
|
1 | 0 |
| 1 |
|
|
| 1 | 0 |
| 1 |
|
|
| 1 | 0 |
| 1 |
|
|
1 | 1 |
| 0 |
|
|
| 1 | 1 |
| 0 |
|
|
| 1 | 1 |
| 0 |
|
|
|
| 0 | 0 | 0 |
|
|
|
| 0 | 0 | 0 |
|
|
|
| 0 | 0 | 0 |
|
|
| 1 | 1 | 1 |
|
|
|
| 1 | 1 | 1 |
|
|
|
| 1 | 1 | 1 |
|
|
|
| 0 | 0 | 0 |
|
|
|
| 0 | 0 | 0 |
|
|
|
| 0 | 0 | 0 |
|
|
| 1 | 0 | 0 |
|
|
|
| 1 | 0 | 0 |
|
|
|
| 1 | 0 | 0 |
|
|
|
| 1 | 1 |
|
|
|
|
| 1 | 1 |
|
|
|
|
| 1 | 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
|
|
|
|
|
|
| 1 | 0 |
|
|
|
|
| 0 | 1 |
x13 | x15 | x16 | x17 | x18 | x19 |
| x13 | x15 | x16 | x17 | x18 | x19 |
| x13 | x15 | x16 | x17 | x18 | x19 |
0 | 0 |
| 0 |
|
|
| 0 | 0 |
| 0 |
|
|
| 0 | 0 |
| 0 |
|
|
0 | 1 |
| 1 |
|
|
| 0 | 1 |
| 1 |
|
|
| 0 | 1 |
| 1 |
|
|
1 | 0 |
| 1 |
|
|
| 1 | 0 |
| 1 |
|
|
| 1 | 0 |
| 1 |
|
|
1 | 1 |
| 0 |
|
|
| 1 | 1 |
| 0 |
|
|
| 1 | 1 |
| 0 |
|
|
|
| 0 | 0 | 0 |
|
|
|
| 0 | 0 | 0 |
|
|
|
| 0 | 0 | 0 |
|
|
| 1 | 1 | 1 |
|
|
|
| 1 | 1 | 1 |
|
|
|
| 1 | 1 | 1 |
|
|
|
| 0 | 0 | 0 |
|
|
|
| 0 | 0 | 0 |
|
|
|
| 0 | 0 | 0 |
|
|
| 1 | 0 | 0 |
|
|
|
| 1 | 0 | 0 |
|
|
|
| 1 | 0 | 0 |
|
|
|
| 1 | 1 |
|
|
|
|
| 1 | 1 |
|
|
|
|
| 1 | 1 |
3. 解多暂时一边放
如果测定变量有多个可选解，就标记它，到全部剩余变量都是多可选解时定值。
4. 全多选解可得解
如果变量都有2个可选解的时侯，只要任意选定一个变量的值施行子句消去法，那么一定能够得到满足解（这是有定理保证的）。
这里先后选x13＝0，x15＝0，x17＝0，x18＝1，x19＝0，就可以将剩余子句全部消去了（表8中设定x18＝1，x19＝0后没有消去子句）。
表8 全多可选解
1 | 0 | 0 | 1 | 1 | 1 | 1 | 0 | 0 | * | 1 | 0 | 0 | * | 0 | * | 0 | 1 | 0 | 0 |
x1 | x2 | x3 | x4 | x5 | x6 | x7 | x8 | x9 | x10 | x11 | x12 | x13 | x14 | x15 | x16 | x17 | x18 | x19 | x20 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 1 | 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 0 | 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 1 | 1 |
5. 验证满足解
一般验证满足解是把解的值带入上面的逻辑表达式，看看结果是否是1。用0和1表格式表示的SAT，验证更方便。方法如表9所示，从上到下看看每个子句中有没有顶端变量的解值，有就可以认定这个子句的值是1，全部通过就说明所求出的n位二进制数是SAT的满足解。
表9 验证满足解
1 | 0 | 0 | 1 | 1 | 1 | 1 | 0 | 0 |
| 1 | 0 | 0 |
| 0 |
| 0 | 1 | 0 | 0 |
x1 | x2 | x3 | x4 | x5 | x6 | x7 | x8 | x9 | x10 | x11 | x12 | x13 | x14 | x15 | x16 | x17 | x18 | x19 | x20 |
1 | 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 |
0 | 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 |
1 |
|
| 0 |
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
0 |
|
| 0 |
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
1 |
|
| 0 |
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
1 |
|
| 1 |
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
1 | 1 |
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
0 | 1 |
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 |
|
|
|
|
|
| 1 |
|
|
|
|
| 0 |
|
|
|
|
|
| 1 |
|
|
|
|
|
| 0 |
|
|
|
|
| 0 |
|
|
|
|
|
| 1 |
|
|
|
|
|
| 0 |
|
|
|
|
| 1 |
|
|
|
|
|
| 0 |
| 1 |
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
| 0 |
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
| 1 |
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 |
| 0 |
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 |
| 0 |
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 | 0 | 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 1 | 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 | 0 | 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
|
|
|
|
|
|
| 1 |
| 1 |
|
|
|
|
|
|
|
|
| 0 |
|
|
|
|
|
|
| 0 |
| 0 |
|
|
|
|
|
|
|
|
| 1 | 0 | 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 1 | 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 | 0 |
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 1 |
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 0 |
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 0 |
|
|
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 1 |
|
|
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 | 1 |
|
|
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 0 |
|
|
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 | 0 |
|
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 0 |
|
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 1 |
|
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 | 1 |
|
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 0 |
|
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
| 0 |
|
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 |
| 1 |
|
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
|
|
|
|
|
| 1 |
|
|
| 1 |
|
|
|
|
|
|
|
| 1 |
|
|
|
|
|
| 0 |
|
|
| 0 |
|
|
|
|
|
|
|
| 1 | 0 |
|
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 1 |
|
| 1 |
|
|
|
|
|
|
|
|
|
0 |
|
|
|
|
|
|
| 0 |
|
| 1 |
|
|
|
|
|
|
|
|
0 |
|
|
|
|
|
|
| 1 |
|
| 0 |
|
|
|
|
|
|
|
|
1 |
|
|
|
|
|
|
| 1 |
|
| 0 |
|
|
|
|
|
|
|
|
1 |
|
|
|
|
|
|
| 0 |
|
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 | 0 |
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 0 |
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 1 |
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 |
| 0 |
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 |
| 1 |
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
| 0 |
| 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
| 1 |
| 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 | 0 | 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 1 | 1 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 | 0 | 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 0 | 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 0 | 0 | 0 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 | 1 | 1 |
为了方便练习，附上excel 文档，有兴趣可以在上面直接操作。
2016-11-10
https://m.sciencenet.cn/blog-340399-1013911.html
上一篇：SAT问题去重复子句的时间复杂度是怎样算出来的？
下一篇：SAT求满足解详解例题文档
