|||
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
Archiver|手机版|科学网 ( 京ICP备07017567号-12 )
GMT+8, 2024-9-27 09:09
Powered by ScienceNet.cn
Copyright © 2007- 中国科学报社