命题可满足性问题(简称SAT问题)是计算机科学领域的重要研究问题之一,作为第一个被证明为NP完全的问题[1],许多实际问题如电路设计、自动定理证明、限界模型检验、等价性检查都可以在多项式时间内转为SAT问题进行求解.但由于SAT问题以命题逻辑公式为处理对象,制约了其描述能力和抽象层次,同时也限制了SAT问题的应用.例如在RTL电路中,由于SAT求解器的抽象层次较低,用位级信息描述问题将丢失大量的逻辑信息同时增加问题的规模和复杂性,从而导致结果不准确并且增加求解的空间与时间开销[2].针对以上问题,以一阶逻辑公式为处理对象的可满足性模理论(简称SMT问题)获得了广泛的关注.由于其采用字级建模语言,其描述能力更强,可以提供一个更灵活的描述问题的框架,而且能够更加准确地反映系统模型的理论,因此,SMT问题具有更加广阔的应用前景.目前,SMT问题已经广泛应用于软件和硬件验证、类型推断、扩展静态检查、测试用例生成、调度、规划等问题中.例如:Intel和AMD公司利用SMT求解器验证其设计的芯片的有效性;微软已经把SMT求解技术应用在其代码分析工具中[3, 4, 5, 6, 7].
SMT问题的一种泛化问题是计数SMT问题(简称#SMT问题),该问题不只需要找到一组解满足给定的一阶逻辑公式,还需要计算满足给定的一阶逻辑公式所有解的个数,因此,#SMT问题的难度也难于SMT问题,其计算复杂性是#P的.高效地解决#SMT问题对人工智能、软件工程等很多领域都有着深远的影响.例如:在软件测试中,计算数据满足路径的个数问题可以转换成#SMT问题进行求解;在电路设计上,可以利用#SMT求解出使用较为频繁的电路,针对这些电路进行冗余设计,不仅可以省钱还会减少电路的体积.近年来,#SMT问题的研究已经开始得到研究学者的重视,例如,马菲菲等人给出了一种精确求解#SMT的方法,但该求解器只能求解小规模的线性问题[8].因此,如何求解较大规模的#SMT问题、如何更准确地给出#SMT问题的近似解的研究还处于空白.
本文设计了一种求解较大规模的#SMT问题的近似求解器.我们在现有的#SMT精确求解算法的基础上加入差分进化算法,提出了一种新的局部搜索算法VolComputeWithLocalSearch,通过调用体积计算工具qhull,进而给出#SMT问题的近似解.算法采用群体规则减少体积计算的次数,差分进化方法快速地枚举各个有解的区域.我们从理论上证明了VolComputeWithLocalSearch算法得到的#SMT近似解是精确解的下界.实验结果表明,VolComputeWithLocalSearch算法在高维问题上具有很好的表现.
本文第1节介绍基本的定义.第2节给出基于差分进化的#SMT问题求解算法.第3节给出实验结果并分析.最后给出全文的总结和未来的相关工作.
1 相关概念为了方便理解,这部分给出与本文相关的基本概念.从本节起,如无特殊声明,将使用xi(i>0)表示布尔变量,vi(i>0)和y表示数值变量,a表示真值赋值.另外说明,本文只研究包含线性算术理论的#SMT问题,即:一阶逻辑公式中的函数变元和谓词变元的类型集合只包含整数、实数和布尔类型,变量之间的操作符只有逻辑运算符(例如析取、合取)和算术运算符(例如加、减)的#SMT实例.
定义1. 设X={x1,x2,…,xn}是布尔变量集合,定义在X上的真值赋值是函数m:X{true,false}.每个真值赋值可以用n元布尔向量表示,那么在X上存在2n个不同的真值赋值.
定义2. 设x是一个布尔变量,则称x或x是文字,其中,称x是正文字,x是负文字.文字x的真值为true当且仅当布尔变量x赋值为true;文字x的真值为true当且仅当布尔变量x赋值为false.
定义3. 子句C=l1∨l2∨…∨lk,其中,l1,l2,…,lk是文字.子句C可满足当且仅当至少有一个文字li(1≤i≤k)赋值为true.
定义4. 合取范式(简称CNF范式)F=C1C2…Ci,其中,C1,C2,…,Ci是子句.CNF范式F可满足当且仅当每一个子句都可满足.
定义5. 给定CNF范式F,计算F可满足的真值赋值个数的问题称为模型计数问题.
定义6. 一阶逻辑公式j是指由个体常量与个体变量、函数常量与函数变量、命题常量与命题变量、谓词常量与谓词变量以及逻辑连接符组成的公式.
定义7. 给定一阶逻辑公式j,可满足性模理论问题(简称SMT问题)是指判断给定的一阶逻辑公式j是否存在可满足解的问题.
定义8. 给定一阶逻辑公式j,#SMT问题是指计算一阶逻辑公式j可满足解的个数的问题.
在本文中,我们只研究包含线性算术理论的#SMT问题,即,一阶逻辑公式中的函数变元和谓词变元的类型集合只包含整数、实数和布尔类型,变量之间的操作符只有逻辑运算符(例如析取、合取)和算术运算符(例如加、减)的#SMT实例.另外,对于只包含线性算术理论的#SMT实例,它可以被表示为一个CNF范式:X(x1,x2,x3,…,xn),其中,布尔变量xi=expri1 op expri2(i=1,…,n).expri1和expri2是线性算术表达式,op是运算符,例如“<”,“=”等.
例1:给定#SMT实例j=(((y+2v<1)(20<y))(v<50))((20<y)(v>4)(v<50)),通过引入布尔变量x1=(y+2v<1),其中,expr11=y+2v,expr12=1,op为<.其他变量如下所示:
$\left\{ \begin{array}{*{35}{l}} {{x}_{1}}=(y+2v<1); \\ {{x}_{2}}=(20<y);\ \ \ \ \\ {{x}_{3}}=(v>4);\ \ \ \ \ \ \\ {{x}_{4}}=(v<50);\ \ \ \ \ \\ \end{array} \right.$ |
可以将#SMT实例表示为CNF范式,首先得到F=((x1x2)x4)(x2x3x4),化简后得到CNF范式:
F=(x1x2x4)(x2x3)(x2x4).
定义9. 如果一个几何体上任意两点所连的线段都在该几何体的内部,则该几何体被称作凸面体.
定理1. 线性公式所围成的几何体要么不存在,要么是凸面体.
对于以线性算术为背景理论的#SMT问题,它实际上是计算一阶逻辑公式所形成的凸面体的体积,显然,这个问题包括模型计数问题和经典的凸面体体积计算问题.
定义10. 设X={x1,x2,…,xn}是一个布尔变量集合,全赋值是指对X上的所有布尔变量都进行一次真值指派(即赋值为true或false),部分赋值是指对X上的部分布尔变量赋值为true或false.我们用向量a={l1,l2,l3,…}表示一个真值赋值,a或者是一个全赋值,或者是一个部分赋值,其中,向量 a中的任意元素li的真值都为true.
定义11. 给定一阶逻辑公式j和其对应的CNF范式F,F的可满足赋值是指满足CNF范式F,同时满足j的背景理论的真值赋值.
从第2节起,如无特殊说明,我们称CNF范式F的可满足赋值是指既满足CNF范式F又满足j的背景理论的真值赋值.另外,对于CNF范式F的任意一个真值赋值都对应一个线性约束公式,见例2.
例2:考虑例1中的#SMT实例j=(((y+2v<1)(20<y))(v<50))((20<y)(v>4)(v<50)),其被表示为CNF范式F=(x1x2x4)(x2x3)(x2x4).我们可以得到一个真值赋值a={x1,x2,x3,x4},其中,
$\left\{ \begin{array}{*{35}{l}} {{x}_{1}}=(y+2v<1); \\ {{x}_{2}}=(20<y);\ \ \ \ \\ {{x}_{3}}=(v>4);\ \ \ \ \ \ \\ {{x}_{4}}=(v<50);\ \ \ \ \\ \end{array} \right.$ |
其对应的线性约束公式为
$\left\{ \begin{array}{*{35}{l}} {{x}_{1}}=(y+2v\ge 1); \\ {{x}_{2}}=(20\ge y);\ \ \ \ \\ {{x}_{3}}=(v\le 4);\ \ \ \ \ \ \\ {{x}_{4}}=(v\ge 50);\ \ \ \ \\ \end{array} \right.$ |
另外,我们可以看出:a可以满足CNF范式F,但由于x3和x4存在冲突,其不满足j的背景理论,故a不是F的可满足赋值.
2 基于差分进化的#SMT问题求解算法#SMT问题是求解SMT实例的可满足解个数的问题,对于一个具有连续问题的解空间,该问题实际上是一个计算体积的问题.而体积计算是一项耗时的过程,这个过程被Dyer和Frieze证明是#P-hard的[9, 10].因此,如何减少体积计算的次数,对提高算法效率具有重要作用.另外,对于#SMT问题的近似求解,如何能够快速地枚举各个有解的区域,对提高算法的精确性具有重要的作用.本文给出的基于差分进化的#SMT问题求解算法VolComputeWithLocalSearch即采用群体规则来减少体积计算的次数、差分进化方法来快速地枚举各个有解的区域.
图 1给出了基于差分进化的#SMT问题求解算法VolComputeWithLocalSearch的整体框架.
算法是在DPLL(T)[11, 12]基础上的,首先初始化实例的体积Vφ=0,并把一阶逻辑公式转换为CNF范式(第1行、第2行);然后,算法进入布尔约束传播过程(简称BCP,即,运用单文字规则传播的全过程).如果布尔约束传播过程出现冲突,则进行冲突分析并产生新子句,然后判断新产生的子句的决策层(backtrack_level)是否小于0.如果是,则算法结束返回体积Vφ;否则回退到新子句所对应的决策层(即,新子句中的变量在DPLL(T)搜索树中所对应节点的层数)(第4行~第8行).如果布尔约束传播过程不出现冲突,则把当前真值赋值赋给a(第10行).算法进入考察当前真值赋值a是否满足CNF范式F的过程:
· 如果当前真值赋值a不满足CNF范式F,则选择一个未赋值的布尔变量扩展当前的赋值(第24行);
· 否则,判断a在背景理论上是否一致(第12行~第22行):如果不一致,则回溯到上一个决策层(第12行、第13行);否则,a即为CNF范式F的可满足赋值.此时,考察a中的文字是否可以从a中删除(第15行~第19行),以此获得尽可能小的部分赋值.这实际上就是群体规则的思想,这部分内容将在第2.1节中进行详细介绍.
最后,重复调用差分进化(DE)子过程获得m个满足#SMT公式φ的解,即凸面体的顶点(第20行),这部分内容将在第2.2节介绍.顶点集合求出来以后,就把顶点集合放到体积计算工具中,将该线性公式φ的体积下界求解出来(第21行).在计算凸面体的体积上,我们调用一种体积计算工具qhull,这是因为qhull是一种非常实用的工具,它可以计算凸包、delaunay三角网、voronoi图、交汇于一点的半空间、最远位置的delaunay三角网、最远位置的voronoi图.另外,qhull也可以计算2维、3维、4维甚至高维空间的凸面体的体积.
定理2. 基于差分进化的#SMT问题求解算法VolComputeWithLocalSearch给出的解是#SMT实例的下界,即,给出的体积是凸面体体积的下界.
证明:反证法.假设算法得出的解不是#SMT的下界,即,算法给出的体积是有包含在凸面体外的体积的.因此,在差分进化过程中所给的顶点中,有一个或多个顶点在凸面体的外边;或者有顶点是满足一阶逻辑公式的,但顶点间连线在凸面体外边或者部分在外边.对于第1种情况,如果顶点在凸面体外边,则该顶点不满足一阶逻辑公式,这与顶点满足一阶逻辑公式是矛盾的;对于第2种情况,顶点满足一阶逻辑公式而顶点间连线全部或部分在凸面体外边,这与凸面体的定义是冲突的.如果给出的体积不包含在凸面体外部的部分,这时只有凸面体内部的部分,因此,基于差分进化的#SMT问题求解算法VolComputeWithLocalSearch给出的解是#SMT实例的下界,即,给出的体积是凸面体的体积的下界. □
2.1 群体规则基于差分进化的#SMT问题求解算法VolComputeWithLocalSearch采用群体规则[8]减少体积计算的次数,以提高算法的效率.接下来,首先给出群体的定义.
定义12[8]. 给定CNF范式F,F的全赋值集合S被称为一个群体,当且仅当存在一个部分赋值ac,使得集合中的任意一个全赋值a满足aSaca.
对于一个群体,计算它们体积将会简化.如下命题所示:
命题1 [8]. 对一个具有部分赋值ac的群体S,一定有$\sum\limits_{\alpha \in s}{volume(\alpha )}=volume({{\alpha }_{c}})$,见例3.
例3:同样考虑例1中的#SMT实例φ=(((y+2v<1)$\vee $(20<y))∧(v<50))$\wedge $((20<y)→(v>4)$\wedge $(v<50)),φ可以被表示为对应的CNF范式F=(x1$\vee $x2∨x4)$\wedge $(x2$\vee $x3)$\wedge $(x2$\vee $x4),其中,
$\left\{ \begin{array}{*{35}{l}} {{x}_{1}}=(y+2v<1); \\ {{x}_{2}}=(20<y);\ \ \ \ \\ {{x}_{3}}=(v>4);\ \ \ \ \ \ \\ {{x}_{4}}=(v<50);\ \ \ \ \\ \end{array} \right.$ |
用SMT求解器很容易找到7个CNF范式F的可满足赋值,因此在直接求解方式中,需要调用7次体积计算工具计算体积,然后,把计算的体积加起来才能得到公式总的体积.这里,我们仅列举7个可满足赋值中的3个.
$\begin{align} &{{\alpha }_{1}}=\{\neg {{x}_{1}},\neg {{x}_{2}},{{x}_{3}},\neg {{x}_{4}}\}, \\ &{{\alpha }_{2}}=\{\neg {{x}_{1}},\neg {{x}_{2}},\neg {{x}_{3}},{{x}_{4}}\}, \\ &{{\alpha }_{3}}=\{\neg {{x}_{1}},\neg {{x}_{2}},{{x}_{3}},{{x}_{4}}\}. \\ \end{align}$ |
接下来,在这3个可满足赋值的基础上再添加一个真值赋值a4={x1,x2,x3,x4},很容易校验出,这个赋值可以使CNF范式F为真.但由于a4的背景理论谓词之间存在冲突关系,所以对应的线性公式组成的区域是不存在的,即volume(a4)=0.根据群体的定义,以上4个真值赋值可以组成一个群体,与之对应的部分赋值是{x1,x2}.根据命题1,有:
volume(a1)+volume(a2)+volume(a3)=volume(a1)+volume(a2)+volume(a3)+volume(a4)=volume({x1,x2}).
因此,我们只需要调用体积计算工具计算一次就可以得到体积.显然:即使赋值会造成谓词冲突,也不会影响体积计算的值.
2.2 差分进化方法差分进化(differential evolution,简称DE)是一种基于群体进化的算法,它首先产生#SMT问题的初始种群,然后,通过适应度计算,再对每个个体进行变异、交叉和选择操作更新种群.新的种群再重新进行适应度计算、变异、交叉和选择操作,反复迭代,直到种群收敛或满足最大进化次数Max_Gen为止[13, 14, 15, 16, 17].图 2给出了差分进化子过程的框架.
子过程首先进入初始化阶段,在#SMT求解的迭代过程可以得到一个CNF范式F的可满足赋值a,将其表示为对应的线性约束公式;然后,在公式的变量取值域中随机初始化变量的值,得到个体(也称为候选解或解):
Ie=(ie1,...,iei,...,ien).
其中,1≤i≤n,n是#SMT实例的维数.以这种方式形成NP个个体,形成种群E(E={I1,I2,…,INP})(第1行).根据适应度函数计算NP个个体的适应度,把适应度最好的个体作为全局最优解gbest的初始值(第2行).如例3中F的可满足赋值a1={x1,x2,x3,x4},其所对应的线性约束公式为
$\left\{ \begin{array}{*{35}{l}} \neg {{x}_{1}}=(y+2v\ge 1); \\ \neg {{x}_{2}}=(20\ge y);\ \ \ \ \\ {{x}_{3}}=(v>4);\ \ \ \ \\ \neg {{x}_{4}}=(v\ge 50);\ \ \ \ \\ \end{array} \right.$ |
在变量取值域中随机初始化变量取值v=51.50,y=20.23后,可以得到个体Ie=(51.50,20.23)(其中,n=2).以这种方式形成NP个个体,形成种群E.最后,算法进入一个迭代过程,对种群E中的每一个个体Ie进行更新(第3行~第18行).在考虑个体Ie时,在种群E中随机地选择3个其 他候选解Ia,Ib和Ic(其中,abce),并且随机地选择一个整数R(其中,1≤R<n,n是#SMT实例的维数)(第5行、第6行),然后进行变异操作(第7行).该操作是形成新个体的第1步,目的是形成中间解,为交叉操作提供一个用于操作的解.它首先用候选解Ib和Ic相减得到差分因子,然后差分因子会与缩放因子F相乘后再经过与候选解Ia相加得到新解Iy,即Iy=Ia+F(Ib-Ic).算法进行交叉操作(第8行~第14行),该操作在变异的基础上形成下一代的准个体.交叉操作可以用数学公式描述如下:
${{I}_{zi}}=\left\{ \begin{array}{*{35}{l}} {{I}_{ei}}rand(0,1)>CR\text{ or }i\ne rand(0,NP) \\ {{I}_{yi}}rand(0,1)\le CR\text{ or }i=rand(0,NP) \\ \end{array} \right.$ |
其中,Iei和Iyi表示变异操作生成中间解的第i维变量;rand(0,1)是一个生成区间位于[0,1)随机实数的函数; rand(0,NP)是一个生成区间位于[0,NP)随机整数的函数,NP是种群中个体的数量,NP一般大于等于4;CR是取值范围为[0,1]的交叉概率.交叉概率决定着整个种群的变异大小,变异大,有利于局部搜索和加速收敛速度;变异小,有利于保持种群多样性和全局搜索.最后,算法进行选择操作(第15行~第18行).经过交叉和变异操作后,生成的中间解Iz将与种群中的个体Ie进行竞争.只有当解Iz的适应度比解Ie的适应度好时,才能用解Iz替代解Ie,否则,Ie仍会留在种群中.以最小优化为例,选择操作可以用数学公式描述如下:
${{I}_{e}}=\left\{ \begin{array}{*{35}{l}} {{I}_{z}}\text{, }f({{I}_{z}})<f({{I}_{e}}) \\ {{I}_{e}}\text{, }f({{I}_{z}})\ge f({{I}_{e}}) \\ \end{array} \right.$ |
其中,f:RnR表示适应度函数.适应度函数可以是代价最小化函数,也可以是适应度最大的函数.该函数把候选解以实数向量的形式作为输入产生一个实数,该数表示候选解的适应度.在本文中,我们采用的适应度函数如下所示:
$f({{I}_{e}})=\sum\limits_{j=1}^{l}{distance(j,{{I}_{e}})}$ |
其中,
$distance(j,{{I}_{e}})=\left\{ \begin{array}{*{35}{l}} 0,\text{ if }{{A}_{j}}{{I}_{e}}\le {{w}_{j}} \\ |{{A}_{j}}{{I}_{e}}-{{w}_{j}}|,\text{ otherwise} \\ \end{array} \right.$ |
Aj表示lxd矩阵A的第j行,w是d维列向量,wj表示向量的第j个元素,Ie是一个解.该公式在数学上的含义是解Ie到不满足约束的距离.若以例1中的约束为例,则Ie就是一个解,l取值为4,表示有4个约束,d取值为2,表示有2个变量,则A是一个4x2的矩阵,w是一个2维列向量.我们用Ie(p,q)表示解,用aij表示矩阵A第i行第j列的数,用wi表示列向量w的第i个数.对于这个几何体,点Ie(p,q) 到第1根直线的距离可以用如下公式计算:
$d=\frac{|{{a}_{00}}p+{{a}_{01}}q-{{w}_{0}}|}{\sqrt{a_{00}^{2}+a_{01}^{2}}}$ |
因为在矩阵A不变的情况下需要重复计算$\sqrt{a_{00}^{2}+a_{01}^{2}}$,为了提高计算性能,我们在算法中去掉$\sqrt{a_{00}^{2}+a_{01}^{2}}$.采
取这种方法对适应度的影响较小,同时可以提高计算速度.注意:根据本文的变异方案可以得知,种群所有个体不一定都会参与变异操作,但所有的个体均会参与交叉操作,并且只会进行一次交叉操作.另外,为了在快速收敛过程中避免算法陷入局部最优,我们在每一代进化过程后,当前最好的个体会被重新随机初始化.
3 实验比较我们在Linux环境下,用C++实现了基于差分进化的#SMT问题求解算法VolComputeWithLocalSearch.为了测试VolComputeWithLocalSearch求解器的性能,我们下载了文献[8]所设计的精确求解器VolComputeBunches和一种基于蒙特卡罗的体积估算器DirectMonteCarloMethod.所有的实验在一台DELL OPTIPLEX 990上运行,实验的运行环境如下:操作系统为Ubuntu 11.10 x64;编译器为GCC4.6(在编译时使用的优化选项是O2);处理器为Intel(R) Core(TM) i7-2600 CPU@3.40GHz(8CPUs);内存为8GB DDR3.在差分进化子过程中,我们选择缩放因子F的值为 2,交叉概率CR取值0.5,种群中个体数量NP的值为500,最大进化次数Max_ Gen取值为100.本实验总共有4个,这4个实验分别从不同的角度验证算法的计算能力、精确度以及稳定性.
3.1 VolComputeWithLocalSearch算法与精确算法的比较本实验的主要目的是通过对比实验,考察VolComputeWithLocalSearch算法的计算能力和验证算法求得的结果是精确值的下界.在实验中,将会与文献[8]提出的#SMT精确算法VolComputeBunches进行比较,实验中用的所有实例均来自于文献[8].表 1给出了VolComputeWithLocalSearch算法与精确算法的比较结果.在表中,实验结果以科学计数法表示,cnf表示实例CNF公式的子句数,v表示实例的维数.从表中的数据可以看出,精确算法VolComputeBunches只能求解八维以内的实例和部分八维实例.与精确算法VolComputeBunches比较,VolComputeWithLocalSearch算法表现最好的实例可以达到精确值的80%左右.另外,VolComputeWith LocalSearch算法的计算结果均小于精确算法VolComputeBunches,这也在一定程度上说明了VolComputeWith LocalSearch算法求出的结果是精确值的下界.
3.2 VolComputeWithLocalSearch算法的计算性能实验
本实验的目的主要是验证VolComputeWithLocalSearch算法的计算能力以及影响算法性能的因素.因为在求解#SMT问题时需要计算#SMT实例所对应的CNF范式F的可满足赋值,CNF范式的难度对求解#SMT问题有一定影响,因此在本实验中,我们选择CNF范式中子句和变量的比值在4~5之间的相变区域[18, 19, 20, 21, 22, 23, 24, 25].本实验共分为6组,表 2~表 8给出了实验的结果.在表中,instance表示实例名称,P表示实例所对应的CNF范式中变量个数,cls表示实例所对应的CNF范式中子句个数,V表示实例的维数,LB表示VolComputeWithLocalSearch算法的计算结果(科学计数法表示),Time表示VolComputeWithLocalSearch算法的计算耗时(单位是秒),r表示子句个数和变量个数的比值.在表 2~表 5的数据中,各表内子句个数和变量个数的比值不变,实例的维数增加,各表间子句个数和变量个数的比值增加.在各表中,前7个实例的维数即V值逐个增加1,剩余的9个实例的维数即V值逐个增加5.在表 7的数据中,子句个数和变量个数的比值和实例的维数不变,CNF范式的规模将不断扩大.在表 8的数据中,子句个数和变量个数的比值和实例的规模不变,实例的维数将不断增加.
表 2给出了VolComputeWithLocalSearch算法在r=4时的计算结果.从表中的计算结果即LB的数据上看,我们可以得出VolComputeWithLocalSearch算法已经可以计算出当r=4维数是55的#SMT问题.从表中的计算时间上我们可以看出,VolComputeWithLocalSearch算法的计算时间与维数基本上成正比关系.
表 3给出了VolComputeWithLocalSearch算法在r=4.33时的计算结果.表中的计算结果即LB的数据上看,我们可以得出当r=4.33时,VolComputeWithLocalSearch算法已经可以计算出维数是55的#SMT问题.从表中的计算时间上我们可以看出,VolComputeWithLocalSearch算法在计算时间上具有递增趋势.
表 4给出了VolComputeWithLocalSearch算法在r=4.67时的计算结果.从表中的计算结果即LB的数据上看,我们可以得出当r=4.67时,VolComputeWithLocalSearch算法也可以计算出维数是55的#SMT问题.从表中的计算时间上我们可以看出,VolComputeWithLocalSearch算法在计算时间上也具有递增趋势.
表 5给出了VolComputeWithLocalSearch算法在r=5时的计算结果.从表中的计算结果即LB的数据上看,我们可以得出当r=5时,VolComputeWithLocalSearch算法也可以计算出维数是55的#SMT问题.从表中的计算时间上我们可以看出,VolComputeWithLocalSearch算法在计算时间上也具有递增趋势.
从表中可以看出:当实例的维数为9时,VolComputeWithLocalSearch算法的执行时间产生了较大的波动.从整体上看,VolComputeWithLocalSearch算法在r=4时执行时间最长,在某种程度上也说明了#SMT问题在r=4时较难求解.表 7给出了当V=50时,VolComputeWithLocalSearch算法的计算结果.从表中可以看出:随着实例规模的增加,算法的执行时间出现了递减-不变-递增的趋势.同时也可以发现,算法可以计算出维数为50的实例.
表 8给出了当P=15,r=4.27时,VolComputeWithLocalSearch算法的计算结果.在表中所有实例的维数即V值逐个增加5.从表中的计算结果即LB的数据上看,我们可以得出VolComputeWithLocalSearch算法已经可以计算出维数是50的#SMT问题.从表中的计算时间上可以看出,VolComputeWithLocalSearch算法的计算时间与维数基本上成正比关系.
综上所述,VolComputeWithLocalSearch算法能够处理较大规模的问题,且算法的计算耗时与实例的维数具有较强的关系,与子句数和变量个数关系不大.通过表 2~表 5中的数据可以初步得出,算法的计算耗时与实例的维数相关的.表 7中数据则在很大程度上排除了与实例的子句数和变量个数的关系.表 8中数据进一步验证了算法的计算耗时与实例的维数具有较强的关系,与子句数和变量个数关系不大.
从计算结果上,VolComputeWithLocalSearch算法的计算能力是可以到55维的.
3.3 VolComputeWithLocalSearch算法的精确度实验本实验的目的是考察VolComputeWithLocalSearch算法的精确度.在实验中,将进行基于蒙特卡罗的体积估算算法DirectMonteCarloMethod的对比实验[26].基于蒙特卡罗的体积估算算法DirectMonteCarloMethod是一种经典的体积计算算法,该算法利用蒙特卡洛法随机均匀地在约束范围内生成顶点,然后随机取一定数量的单位球体,在球体计算顶点的密度,再利用密度估算体积.我们在实验中所用到的实例均出自于文献[26],表 9给出了VolComputeWithLocalSearch算法与DirectMonteCarloMethod算法的比较结果.在表中,Vol表示实例的实际体积(采用数学方法计算),Time表示计算耗时,Ratio表示精确度(算法计算的结果与精确体积的比值).从表中可以看出,VolComputeWithLocalSearch算法的精确度都达到了95%以上.
在与算法DirectMonteCarloMethod精确度的比较上,VolComputeWithLocalSearch算法除了在Sample1,Sample5,Sample6略低于算法DirectMonteCarloMethod,在其他实例上均有较大幅度的提高.尤其对于实例Sample3,精确度从原来的0.01777提高到0.95321.在计算耗时方面,VolComputeWithLocalSearch算法则全面优胜于DirectMonteCarloMethod算法,最大的提高幅度约达95.8%(实例Sample8).
3.4 VolComputeWithLocalSearch算法的稳定性实验本实验的目的是考察VolComputeWithLocalSearch算法的稳定性.在实验中,同样与基于蒙特卡罗的体积估算算法DirectMonteCarloMethod[26]进行比较.我们在实验中所用到的实例均出自于文献[26],每个实例进行10次重复实验,分别记录VolComputeWithLocalSearch算法和DirectMonteCarloMethod算法的计算结果和执行时间.表 10、表 11给出了VolComputeWithLocalSearch算法与DirectMonteCarloMethod算法的稳定性实验结果,其中,Ratio为算法的精确度(计算结果与真实值的比值),Time表示耗时,Average是精确度的平均值,Variance是精确度的方差.
可以看出:
· 在算法精确度的平均值上,相较于DirectMonteCarloMethod算法,VolComputeWithLocalSearch算法计算用时均较短;
· 从算法精确度的方差来看,VolComputeWithLocalSearch算法除了在实例Sample3和Sample7的精确度的方差较大以外,其他实例不论在精确度还是在时间上都全面优于DirectMonteCarloMethod算法.
综上所述,VolComputeWithLocalSearch算法在收敛速度上变化不大,算法在迭代次数上是稳定的,因此,VolComputeWithLocalSearch算法是稳定的.
综合以上数据分析,VolComputeWithLocalSearch算法在小规模问题上精确度和计算能力上是有保证的;在大规模问题上,由于目前还没有精确算法能够与之相比较,故在精确度等方面有待考证.通过实验,我们的算法计算耗时与维数成不严格的正比例关系,与实例的子句数和变量个数关系不大.由此可见,#SMT的求解效率的瓶颈并不是SAT求解器,而是在于体积计算过程.
4 结论和展望本文设计了一种求解SMT计数问题的近似求解器,在现有的#SMT精确求解算法的基础上加入差分进化算法,提出了一种新的局部搜索算法VolComputeWithLocalSearch,通过调用体积计算工具qhull,进而给出#SMT问题的近似解.我们从理论上证明了VolComputeWithLocalSearch算法可以得到精确解的下界.实验结果表明:VolComputeWithLocalSearch算法是稳定的,具有快速的求解能力,并在高维问题上具有很好的表现.
对于基于线性公式的背景理论的#SMT问题且只要求下界的问题应用中,本文的研究可以提供很大的帮助,但VolComputeWithLocalSearch算法仅可以求解基于线性公式的背景理论的#SMT实例,对于其他背景理论如非线性公式、位向量、指针等理论的求解则还有待突破.
[1] | Cook SA. The complexity of theorem-proving procedures.In:Proc.of the 3rd Annual ACM Symp. on Theory of Computing.ACM Press, 1971 :151–158. [doi:10.1145/800157.805047] |
[2] | Li J, Liu WF. A survey on theoretical combination techniques of SMT solvers. Computer Engineering&Science, 2011, 33 (10) :111–119(in Chinese with English abstract). http://www.cnki.com.cn/Article/CJFDTOTAL-JSJK201110024.htm |
[3] | Bozzano M, Bruttomesso R, Cimatti A, Junttila T, Ranise S, van Rossum P, Sebastiani R. Efficient satisfiability modulo theories via delayed theory combination.In:Proc.of the Computer Aided Verification. Berlin Heidelberg:Springer-Valag, 2005, 335 (349) . [doi:10.1007/11513988_34] |
[4] | Nieuwenhuis R, Oliveras A, Tinelli C. Solving SAT and SAT modulo theories:From an abstract davis-putnam-logemann-loveland procedure to DPLL (T). Journal of the ACM, 2006, 53 (6) :937–977. [doi:10.1145/1217856.1217859] |
[5] | Jha S, Limaye R, Seshia SA. Engineering an efficient smt solver for bit-vector arithmetic.In:Proc.of the Computer Aided Verification. Berlin,Heidelberg:Springer-Verlag, 2009 :668–674. [doi:10.1007/978-3-642-02658-4_53] |
[6] | Zhou J, Su WH, Wang JY. New worst-case upper bound for counting exact satisfiability. Int'l Journal of Foundations of Computer Science, 2014, 25 (6) :667–678. [doi:10.1142/S0129054114500270] |
[7] | Huang P, Yin MH, Xu K. Exact phase transitions and approximate algorithm of#CSP. In:Proc.of the AAAI, 2011 . http://cn.bing.com/academic/profile?id=2405727752&encoded=0&v=paper_preview&mkt=zh-cn |
[8] | Ma FF, Liu S, Zhang J. Volume computation for boolean combination of linear arithmetic constraints.In:Proc.of the Automated Deduction. Springer-Verlag, 2009 :453–468. [doi:10.1007/978-3-642-02959-2_33] |
[9] | Gomes CP, Hoffmann J, Sabharwal A, Selman B. From sampling to model counting.In:Proc.of the 20th Int'l Joint Conf.. on ArtificialIntelligence, 2007 :2293–2299. http://cn.bing.com/academic/profile?id=2171960770&encoded=0&v=paper_preview&mkt=zh-cn |
[10] | Dyer ME, Frieze AM. On the complexity of computing the volume of a polyhedron. SIAM Journal on Computing, 1988, 17 (5) :967–974. [doi:10.1137/0217060] |
[11] | Davis M, Putnam H. A computing procedure for quantification theory. Journal of the ACM, 1960, 7 (3) :201–215. [doi:10.1145/321033.321034] |
[12] | Davis M, Logemann G, Loveland D. A machine program for theorem-proving. Communications of the ACM, 1962, 5 (7) :394–397. [doi:10.1145/368273.368557] |
[13] | Storn R, Price K. Differential evolution-A simple and efficient heuristic for global optimization over continuous spaces. Journal of Global Optimization, 1997, 11 (4) :341–359. [doi:10.1023/A:1008202821328] |
[14] | Storn R. On the usage of differential evolution for function optimization.In:Proc.of the'96 Biennial Conf. of the North American Fuzzy Information Processing Society (NAFIPS).IEEE, 1996 :519–523. [doi:10.1109/NAFIPS.1996.534789] |
[15] | Storn R, Price K. Minimizing the real functions of the ICEC'96 contest by differential evolution.of the Int'l Conf.. on Evolutionary Computation, 1996 :842–844. [doi:10.1109/ICEC.1996.542711] |
[16] | Li XT, Yin MH. Application of differential evolution algorithm on self-potential data. PloS one, 2012, 7 (12) . [doi:10.1371/journal.pone.0051199] |
[17] | Li XT, Yin MH. An opposition-based differential evolution algorithm for permutation flow shop scheduling based on diversity measure. Advances in Engineering Software, 2013, 55 :10–31. [doi:10.1016/j.advengsoft.2012.09.003] |
[18] | Zhou JP, Yin MH, Zhou CG. New worst-case upper bound for#2-SAT and#3-SAT with the number of clauses as the parameter.In:Proc.of the 24th AAAI Conf.. on Artificial Intelligence, 2010 :217–222. http://cn.bing.com/academic/profile?id=1542171562&encoded=0&v=paper_preview&mkt=zh-cn |
[19] | Gao J, Wang JN, Yin MH. Experimental analyses on phase transitions in compiling satisfiability problems. Science China Information Sciences, 2015, 58 (3) :1–11. [doi:10.1007/s11432-014-5154-0] |
[20] | Huang P, Yin MH. An upper (lower) bound for max (min) CSP. Science China Information Sciences, 2014, 57 (7) :1–9. [doi:10.1007/s11432-013-5052-x] |
[21] | Zhou JP, Yin MH, Gu WX, Sun JG. Research on decreasing observation variables for strong planning under partial observation. Ruan Jian Xue Bao/Journal of Software, 2009, 20 (2) :290–304(in Chinese with English abstract). [doi:10.3724/SP.J.1001.2009.03152] |
[22] | Yin MH, Sun JG, Lin H, Wu X. Possibilistic extension rules for reasoning and knowledge compilation. Ruan Jian Xue Bao/Journal of Software, 2010, 21 (11) :2826–2837(in Chinese with English abstract). [doi:10.3724/SP.J.1001.2010.03690] |
[23] | Yin MH, Zhou JP, Sun JG, Gu WX. Heuristic survey propagation algorithm for solving QBF problem. Ruan Jian Xue Bao/Journal of Software, 2011, 22 (7) :1538–1550(in Chinese with English abstract). [doi:10.3724/SP.J.1001.2011.03859] |
[24] | Yin MH, Lin H, Sun JG. Solving#SAT using extension rules. Ruan Jian Xue Bao/Journal of Software, 2009, 20 (7) :1714–1725(in Chinese with English abstract). [doi:10.3724/SP.J.1001.2009.03320] |
[25] | Xu L. Improved SMT-Based Bounded Model Checking for Real-Time Systems. Ruan Jian Xue Bao/Journal of Software, 2010, 21 (7) :1491–1502. [doi:10.3724/SP.J.1001.2010.00585] |
[26] | Liu S, Zhang J, Zhu B. Volume computation using a direct Monte Carlo method.In:Proc.of the Computing and Combinatorics.. Springer-Verlag, 2007 :198–209. [doi:10.1007/978-3-540-73545-8_21] |
[2] | 李婧, 刘万伟. SMT求解器理论组合技术研究. 计算机工程与科学, 2011,33 (10) :111–119. http://www.cnki.com.cn/Article/CJFDTOTAL-JSJK201110024.htm |
[21] | 周俊萍, 殷明浩, 谷文祥, 孙吉贵. 部分可观察强规划中约减观察变量的研究. 软件学报, 2009,20 (2) :290–304. [doi:10.3724/SP.J.1001.2009.03152] |
[22] | 殷明浩, 孙吉贵, 林海, 吴瑕. 可能性扩展规则的推理和知识编译. 软件学报, 2010,21 (11) :2826–2837. [doi:10.3724/SP.J.1001.2010.03690] |
[23] | 殷明浩, 周俊萍, 孙吉贵, 谷文祥. 求解QBF问题的启发式调查传播算法. 软件学报, 2011,22 (7) :1538–1550. [doi:10.3724/SP.J.1001.2011.03859] |
[24] | 殷明浩, 林海, 孙吉贵. 一种基于扩展规则的#SAT求解系统. 软件学报, 2009,20 (7) :1714–1725. [doi:10.3724/SP.J.1001.2009.03320] |