CMP设计分享 http://blog.sciencenet.cn/u/accsys 没有逆向思维就没有科技原创。 不自信是科技创新的大敌。

博文

3-SAT求解基本方法

已有 4156 次阅读 2015-11-18 08:38 |个人分类:教学笔记|系统分类:科研笔记| 3SAT, 分段子句消去法

3-SAT求解基本方法

姜咏江

分段子句消去法的求解,最关键的是关联段求解。3SAT关联段无解只有3中情况:

1)出现有8个子句的子句块;

2)出现了只有一个变量需要确定值,却无值可选的动态块;

3)在确定了一个变量值之后,出现了42SAT子句的动态块,叫全2sat动态块。

3SAT解题中如何排除无解分支?基本方法是:先选择4个同变量值的子句块定值,随时注意避免出现全2sat动态块

下面我们以实际例子来加以说明。

1中有变量x6x84个相同的值,不选这个值就会进入到无解分支。因而选择x60x80


1  子句块变量4同值

消去相关子句,出现了有唯一解的动态块(图2中有3个子句的子句块)。


2  出现了唯一解动态子句块

选定动态块解,并消去相关子句就得到了图3,其中有唯一解的子句块2个。


3  唯一解的一个子句子句块

消去这两个唯一解子句块,得到图4图4中除了一个4子句块之外,都是有1个子句或2个子句的子句块。这有4个子句的子句块是由两对互反子句构成的,因而也是多解子句块。


4  多解的4子句子句块

对于都是多解的子句块或动态子句块都可以设定变量值得到相应的解。如图5所示,可有此3SAT的满足解为000010101*1010***01*。“*”表示可以为01


5  选择关联子句多的变量值

总结一下,当固定了一个变量之后,有一个、两个子句的子句块总有多解。有三个子句的子句块可能有唯一解或多解;有四、五和六个子句的子句块都可能出现无解或多解的情况,七个子句的子句块只有唯一解。

一般过程:

1)先寻找唯一解或可能无解的子句块,若有无解子句块则关联段无解。进而3SAT无解。

2)设定值时应避开无解情况。

3)最后处理都是多解的关联子句块,可设定关联变量值使消去的子句最多。

 

定理:变量4同值不取,则发生无解。

此定理证明留给读者如何?(参考【1】定理8

 

2015-11-18

1http://blog.sciencenet.cn/blog-340399-928224.html





https://blog.sciencenet.cn/blog-340399-936209.html

上一篇:3SAT求解什么情况下可以确定变量只有惟一值?
下一篇:3SAT解题步骤与规则
收藏 IP: 125.39.34.*| 热度|

0

该博文允许注册用户评论 请点击登录 评论 (0 个评论)

数据加载中...
扫一扫,分享此博文

Archiver|手机版|科学网 ( 京ICP备07017567号-12 )

GMT+8, 2024-3-29 14:08

Powered by ScienceNet.cn

Copyright © 2007- 中国科学报社

返回顶部