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

博文

征求数字电路优化和基因计算等方面合作者

已有 3624 次阅读 2017-5-6 13:27 |个人分类:SAT问题|系统分类:科研笔记| 子句消去法, 多项式时间

征求数字电路优化和基因计算等方面合作者

姜咏江

布尔电路可满足性问题,即一般称为SAT问题,长时间没有多项式时间的快速算法出现。DPLL方法虽然能够完备求出满足解,但是速度较慢,特别当合取范式CNF=1有唯一解的时候,DPLL获得其可满足解,消耗的时间叫人难以忍受。

本人发明的子句消去法求3-SAT满足解,时间复杂度最坏的情况也不超过O(n4),因而计算速度较快。1是具有200个逻辑变量的3-CNF


1  200个变量的3-CNF

200个变量500个子句的3-CNF,用子句消去法在个人笔记本电脑上,求出结果为“真”满足解用了443秒(见图2,解数码串中那个些*,表示该位变量可以取值0或1)。这个求解的时间比起指数时间复杂度算法,同样的问题肯定是快得很多。有求3-SAT问题满足解的朋友,一定会从此实例中体会到子句消去法的多项式时间复杂度的特性。


2   3-CNF=1的满足解和运行时间

子句消去法是完备的算法,即任何的SAT问题都可以得到确切的满足解,或者指出那些不满足的合取范式CNF。与DPLL算法相反,SAT的满足解越少,子句消去法的求解速度越快。依据子句消去法理论,我们不仅能够求出SAT的满足解,而且能够依据CNF的结构明确判断出其无解,或者有几个解。

我所研究的是SAT问题满足解和全部解的计算方法。如何将这种快速的计算方法应用于实际领域,这还是些复杂而具体的问题。需要进一步地研究。

我设计完成了3-SAT求满足解和求全部解的计算机软件。如果有朋友愿意了解或进行相关的测试,请给我写信,以便我们建立联系,奉送测试软件。匿名需求,恕不接待。

我的邮箱是:accsys@126.com

2017-5-6




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

上一篇:科研需要坚韧不拔的意志和无所畏惧的精神
下一篇:3-SAT满足解软件ZJXQF使用说明书
收藏 IP: 118.144.20.*| 热度|

3 张云 彭雷 crossludo

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

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

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

GMT+8, 2024-12-5 15:03

Powered by ScienceNet.cn

Copyright © 2007- 中国科学报社

返回顶部