|||
征求数字电路优化和基因计算等方面合作者
姜咏江
布尔电路可满足性问题,即一般称为SAT问题,长时间没有多项式时间的快速算法出现。DPLL方法虽然能够完备求出满足解,但是速度较慢,特别当合取范式CNF=1有唯一解的时候,DPLL获得其可满足解,消耗的时间叫人难以忍受。
本人发明的子句消去法求3-SAT满足解,时间复杂度最坏的情况也不超过O(n4),因而计算速度较快。图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
Archiver|手机版|科学网 ( 京ICP备07017567号-12 )
GMT+8, 2024-12-5 15:03
Powered by ScienceNet.cn
Copyright © 2007- 中国科学报社