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

姜咏江                                         2017-5-1

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

1.             系统安装

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

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

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

2.             操作注意事项

系统操作菜单如图2所示：

                          图2   系统菜单

（1）      SET-SAT：有子菜单new3-SAT、example。new3-SAT用户输入不多于3个文字的CNF。合取范式总体变量不少于3个。如果空记录不够，可以用CTR-Y追加。此有5个例子供用户演练。最长的例子，变量有200个。一般情况下，合取范式的变量越多，程序执行的时间会越长。Example4的200变量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查看例题CNF。选RUN1或RUN2执行，再选SOLUTIONS看结果。对不对，点击VERIFY菜单立即可以让你踏实。

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

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

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

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

                                 图5  写入子句界面

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

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

                                         图6   example1

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

谢谢使用测试！

欢迎联系。Accsys@126.com