布尔可满足性问题（一）
闵应骅
      这是一个计算科学里的理论问题。让我试试看能不能用通俗的语言把它说清楚。
      计算机里的位变量都是布尔变量，只取值0或1。两个布尔变量之间的运算只有“与”“或”“非”，表示为“∧”“∨”“¬”。你能猜到 1∧0=0，1∨0=1，¬1=0。现在我有一个包含许多变量的表达式，例如：x∨y∧¬z，我问：这个表达式能等于1吗？如果能，x,y,z分别等于什 么，表达式就等于1，就说这个表达式被满足了。这就是布尔可满足性（简称SAT）问题。但是，你要允许变量个数可以任意，表达式可以任意长。这个问题是一 个计算复杂性很高的问题，已经证明它基本上是一个多项式复杂性算法不可解决的问题。这句话，我无法用通俗的语言来说明。但是没有关系，你只要知道这问题没 有一般的简单算法来彻底解决。本文要说的是：这个问题有实际意义，而且最近在算法上有进展和应用。
       一个经典的图包含节点和边，问：给每一个节点着色，使相邻节点的颜色不同，四个颜色够不够？这就是图论中著名的四色问题。这个问题可以转化为布尔可满足性问题。四个颜色可以分别编码为00，01，10，11。例如，从图1中，节点2着色记为（c₂₀,c₂₁）。节点i与节点j不能同色可表示为（ci0∧cj0）∨(ci1∧cj1)=0。你可以看到，对于这个简单的图，约束可以用上面的编码表达式表示，要求其为1。下面就是解。

      布尔可满足性问题的扩张就是优化问题。如果变量的取值不只有0和1，目标函数的取值也不只是0和1，而是取最大或最小，而约束条件可以表示为若干个表达式。我们的问题是寻找变量的一组值，在满足约束条件下，目标函数取值最大或最小。这不就是优化问题吗？
      布尔可满足性问题有许多应用，许多问题都可以归结为SAT。特别是在集成电路的设计与测试中，到处都是。例如，看两个逻辑函数f1,f2是否等价，只要判断（f1∧¬f2）∨(¬f1∧f2)是否永远不可满足。

       下一篇将介绍SAT解算器。