|||
布尔可满足性问题(二)
闵应骅
SAT的计算复杂性很高,但实际中又有需求。怎么办?公司已经开发了许多SAT解算器,我国还举办过SAT解算器的比赛。设法限制算法的运行次数或时间,实在算不出来时,只能告诉你失败了。但是,大多数情况下能够成功。
一般先把待满足的逻辑表达式变成和之积的形式CNF,即每一项都是“或”,所有的项“与”起来,可称“或与式”。例如, (¬x2∨x3)∧(¬x1∨x3)∧(x1∨x2∨¬x3)。可以证明,任何逻辑函数都可以或与式表示。要让它为1,只要让所有项(子句)皆为1就可以 了。而要让某一项为1,只要其中一个文字为1就可以了。首个变量赋值的基本方法当然是随机,再加上推理、学习、回溯等等功能,可以比较有效地使表达式为 1。但一般要考虑表达式的特殊性,才能使算法更有效。
在上世纪,人们对SAT可以说是望而生畏。进入新世纪,这方面的研究活跃起来。评价算法的改进是用一些公用的实例。一般是由软件和硬件设计中碰到的,变量个数大概是100-7500,而子句数在6-10万。近年来的进展如图4所示。
从图可以看出,2007年的算法比2000年的工作至少加快了500倍。这方面的工作应该首推CMU(美国卡内基-梅隆大学)的Randal E. Bryant教授和他的研究团队。
和线性方程求解器、数学规划工具一样,SAT解算器现在也可以进入工业应用了。在EDA工业界,用于设计验证和测试产生、等价性检验和性质检验,以及微处理器验证、软件验证和调试。
SAT问题的推广是SMT(satisfiability modulo theories)。如果SAT中的逻辑表达式的变量是涉及非二值变量的谓词,例如这些非二值变量也许是一个线性不等式定义的,也许是实数、整数或某一种 数据结构,像表、数组、位向量等等。这时,SMT实质上是判断满足若干理论之间某种逻辑关系是否存在。SMT的中文翻译我还不知道怎么翻,我自己也不敢乱 翻。它既是一个理论问题,在软件和复杂硬件的验证,甚至社会科学研究方面有重要的应用前景。
Archiver|手机版|科学网 ( 京ICP备07017567号-12 )
GMT+8, 2024-8-17 21:15
Powered by ScienceNet.cn
Copyright © 2007- 中国科学报社