布尔可满足性问题（二）
闵应骅
      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的中文翻译我还不知道怎么翻，我自己也不敢乱 翻。它既是一个理论问题，在软件和复杂硬件的验证，甚至社会科学研究方面有重要的应用前景。