|||
布尔可满足性问题(一)
闵应骅
这是一个计算科学里的理论问题。让我试试看能不能用通俗的语言把它说清楚。
计算机里的位变量都是布尔变量,只取值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着色记为(c20,c21)。节点i与节点j不能同色可表示为(ci0∧cj0)∨(ci1∧cj1)=0。你可以看到,对于这个简单的图,约束可以用上面的编码表达式表示,要求其为1。下面就是解。
布尔可满足性问题的扩张就是优化问题。如果变量的取值不只有0和1,目标函数的取值也不只是0和1,而是取最大或最小,而约束条件可以表示为若干个表达式。我们的问题是寻找变量的一组值,在满足约束条件下,目标函数取值最大或最小。这不就是优化问题吗?
布尔可满足性问题有许多应用,许多问题都可以归结为SAT。特别是在集成电路的设计与测试中,到处都是。例如,看两个逻辑函数f1,f2是否等价,只要判断(f1∧¬f2)∨(¬f1∧f2)是否永远不可满足。
下一篇将介绍SAT解算器。
Archiver|手机版|科学网 ( 京ICP备07017567号-12 )
GMT+8, 2024-4-26 11:29
Powered by ScienceNet.cn
Copyright © 2007- 中国科学报社