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

姜咏江

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

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

图1  有200个变量的3-CNF

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

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

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

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

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

我的邮箱是：accsys@126.com

2017-5-6