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

博文

3-SAT满足解软件ZJXQF使用说明书

已有 3829 次阅读 2017-5-10 08:37 |个人分类:3SAT解法|系统分类:科研笔记| 子句消去法, 多项式时间

3-SAT满足解软件ZJXQF使用说明书

姜咏江                                         2017-5-1

直到本人发明的《子句消去法》,没有人能够肯定自己设计出了在多项式时间求出3-SAT满足解的程序。3-SAT问题的子句消去法算法时间复杂度为O(n4),这是一种完备求解的算法。对于无解的合取范式CNF,子句消去法能够直接判断。对于有解的情况,可以一次性求出满足解。

1.             系统安装

系统安装十分简单,只要在子句消去法安装文件夹下(见1),运行setup程序即可。


                     图1  子句消去法安装文件夹

程序安装在ZJXQF文件夹,执行程序名称是“子句消去法”。

2.             操作注意事项

系统操作菜单2所示


                          图2   系统菜单

(1)      SET-SAT有子菜单new3-SATexamplenew3-SAT用户输入不多于3个文字的CNF合取范式总体变量不少于3个。如果空记录不够,可以用CTR-Y追加。此有5个例子供用户演练。最长的例子,变量有200个。一般情况下,合取范式的变量越多,程序执行的时间会越长。Example4200变量CNF,程序执行时间约5分钟。

(2)      CLAUSE:用查看输入的子句。可以追加和修改,若删除记录,点黑左面小方框,然后选EDIT菜单删除。

(3)      SAVE:将自己输入的合取范式表保存。

(4)      GET:将自己保存的表取出。

(5)      EDIT:包括修改表结构和删除记录。具体操作3所示,一看便知。如果选择修改表结构,字段名称必须是以“a”加数字的形式,最后一个字段的序号是最大的,开始或中间可以不连续。


                          图3  CNF处理子菜单

(6)      RUN1:主要用于有了CNF表之后,求一个满足解。

(7)      RUN2:再来求另一个满足解(如果CNF=1有唯一解,其与RUN1运行结果会相同)。

(8)      SOLUTIONS:这是按变量顺序显示的满足解。这里以表的形式显示,避免程序执行之后的结果,哪个变量值是什么,让人难以分辨。表中“-”同“*”一样表示该变量值任意

(9)      VERIFY:检验运行结果是否满足解。

(10)   QUIT: 本软件退出只能选这一项。

3.             解检验

本软件设有满足解检验程序,选择VERIFY菜单即可检验所求结果是否是这个合取范式的满足解(见4解检验的过程,是将得到的变量值代到原合取范式,看看能不能使其结果为“真”。其实这种检验对子句消去法来说,已经没有必要了,因为程序执行中就会指出无解的情况。


                           图4  满足解验证

4.             例题操作

不选择new 3-SAT菜单,可以选择其它菜单项,然后选择CLAUSE查看例题CNFRUN1RUN2执行,再选SOLUTIONS看结果。对不对,点击VERIFY菜单立即可以让你踏实

练习:选择SET-SATnew-3-sat,然后用y回答。出现“输入合取范式变量个数:”。如果变量数量少于3,系统会自动调整为3。之后又让你“输入合取范式子句个数:”。回答之后,进入子句填写界面。

合取范式的01表示法,要求一个子句只占一行。这里是3-sat程序,一个子句的变量不能超过3个。可以允许有空行。如果行数不够,可以用ctr-y联合键增加空行(见5)。

合取范式输入完成,关闭界面,可进行其它操作。还可以先选SAVE,将你的输入保存起来,需要时用GET恢复。

如果题目多解,可以分别选择RUN1RUN2得到不同的满足解,但不是全部解。只有题目有唯一解时,两者才会有一样的结果。


                                 图5  写入子句界面

选择example能够快速地验证和领会子句消去法的运算速度。K-CNF=1的子句消去法的时间复杂度是k+1阶的多项式时间。虽然算法是多项式时间复杂度,但在变量很多的情况下,也要执行一段时间。一般情况下子句消去法较指数形式的DPLL算法,要快很多,特别是在有唯一解的时候。

6Tseytin变换的一个实际电路的CNF,共有5个解。这里用子句消去法可求出2个满足解。


                                         图6   example1

子句消去法系统操作简单,只是个人电脑资源有限,不能测试更大的3-SAT求满足解。但只要将本算法移植到大型机器上,任何3-SAT问题求满足解都不在话下。


谢谢使用测试!

欢迎联系。Accsys@126.com






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

上一篇:征求数字电路优化和基因计算等方面合作者
下一篇:P=NP后果会怎样?
收藏 IP: 118.144.20.*| 热度|

1 彭雷

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

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

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

GMT+8, 2024-3-28 16:07

Powered by ScienceNet.cn

Copyright © 2007- 中国科学报社

返回顶部