可满足性求解器中一种可观无关性利用方法

1、可满足性求解器中一种可观无关性利用方法    可满足性(satisfiability, SAT)问题是理论计算机和智能计算的研究热点问题.随着SAT研究所取得的突破性进展,电子设计自动化领域中等价性验证、模型检测、自动测试向量生成等许多问题都可以转化为可满足性问题加以解决.许多先进的SAT求解器如GRASP1,SATO2,Chaff3,BerkMin4都是基于合取范式(conjunctivenormal form, CNF)的,需要把电路相关的问题编码为CNF形式,才能对其进行求解.在这一变换过程中,电路的结构信息,如门的方向、逻辑路径、信号,e的可观性

2、等信息被丢掉了5,而这些信息,特别是电路可观性对解决电路相关的问题是非常有用的.目前已有不少关于电路可观性利用方法的研究,传统的ATPG算法通过J-frontier确认传播操作来动态地探测电路的活动区域;文献6把信号可观性用于电路结构描述到CNF的转换;文献7在SAT算法之上增加一个用以维护有关电路信息的附加层,以求解故障测试模式生成问题;文献8根据电路结构中变量的可观情况,对变量和子句的活动性进行标记,把不需要分支的变量和其扇入子句标记为“惰性”,从而动态地减少求解搜索空间.但是,这些方法在求解过程中都需要用到电路的结构描述.文献9根据每根线对原始输入的懒惰影响(lazy influence

3、 onprimary inputs, LIPI)进行变量决策,也利用了电路可观性.该方法的LIPI分数在预处理阶段静态计算得到,不能反映变量决策的动态影响,不能保证变量决策最优.文献10通过为子句添加可观无关条件,把电路的可观性转化为CNF表达式中子句的可观性,从而大大修剪了问题的探索空间,提高了求解器的性能.为子句添加可观无关条件的方法是一个利用电路可观性的灵活方法,但是文中所使用的静态排序方法导致总有一些可观无关条件丢失,从而限制了可以利用的可观无关条件的总数,使电路的可观性不能得到很好的利用.本文对文献10方法进行了改进.为了避免使用排序,同时又保证电路的控制唯一性,采取不对只出现在可观

4、无关条件中的变量赋值的策略.另外,由于无关条件计算时不考虑变量排序约束,减少了可观无关条件丢失.实验对比说明,本文方法可以更有效地利用电路可观性减少求解搜索空间、提高求解速度.1SAT问题一个布尔变量x可取真值1(true)或0(false).一个文字l或是变量的原始形式x,或是其否定形式x-.一个子句c( clause)是文字的析取(disjunction).一个CNF公式是子句的合取(conjunction).一个含有n个变量和m个子句的布尔公式可以表示为(x1,xn)=mi=1ci,其中ci=kij=1lj,ki0,n,文字的变量var(li)=xi,li1,0.可满足性问题SAT()是

5、指:对一个给定的CNF公式,确定是否存在一个赋值A,使得得到满足.如果存在,称是可满足的,此时A称为的一个解(满足性赋值);否则,称是不可满足的.2可观无关性及相关定义定义1.在一个电路中,如果一个变量取任何值都不影响电路的输出,那么称这个变量为可观无关(observability don t cares,ODC)变量.为了便于理解,我们也称其为不可观变量.定义2.可以使一个变量(门的输出)变为不可观变量的所有文字的集合称为该变量的可观无关条件,即不可观条件.把变量的不可观条件添加到以该变量作为输出的逻辑门所生成的子句后,形成子句的不可观条件,我们称这种子句为带有可观无关条件的子句.带有不可观

6、条件的CNF公式中,每个子句的表示形式为l+0d*011,其中,l表示常规的文字,与传统CNF中的一样,l+表示有一个或多个常规文字;d是可观无关条件文字,d*表示可能有0个或多个可观无关条件文字;0是分隔符.这种表示方法把电路中信号变量的可观属性转化为子句的可观属性,使得在进行SAT问题求解的整个过程中,都可以根据子句中的可观无关条件提供的电路可观性信息减少问题搜索空间,提高SAT求解器的效率.电路可观性信息可一次转化,多次利用.一个子句l1ln0ln+1ln+m0(其中n1, m0, l1ln为常规子句部分,ln+1ln+m为可观无关条件部分)的满足性通过c =ni=1liCon(mj=0

7、ln+j) (1)进行判别.其中,Con表示可观无关条件部分的满足情况,用于区分二者的不同.式(1)成立的条件是ni=1li=1(2)和Con(mj=0ln+j) =1(3)至少有一个成立.定义3.由于子句的常规子句部分中的文字的赋值满足而满足的子句,称为一般满足子句.定义4.由于子句的无关条件部分中的文字的赋值满足而满足的子句,称为忽略满足子句.根据定义3和定义4,若式(2)成立,则子句为一般满足子句;若式(3)成立,则子句为忽略满足子句.定义5.当一个逻辑门的一个输入变量取值“0”或“1”即可决定逻辑门的输出值,那么这个变量称为控制输入变量.该控制输入变量的赋值称为控制值.例如,一个2输入

8、AND门的输入A和B,当A=0时,决定该门的输出为0,那么变量A称为控制输入(变量),其取值“0”为控制值.一个子句的电路可观无关条件是一个文字集合,这些文字控制着该子句的可观性.当条件中有一个文字为真时,该子句变为不可观子句,并且其在后15=1,进一步得出13,14在输出15处不可观,从而使变量5,6,7,8,11均变得不可观,只有门g1,g2和g4生成的子句需要继续判断.但这时子句的不可观条件中还含有变量13和14,若仍对其进行赋值,例如令13=1,则g1,g2和g4生成的子句均满足(忽略满足),求解结束,得到的赋值12=1,13=1中被赋值变量都是中间变量,其他变量可任意取值.很明显,这

9、是错误的赋值,如对5,6均赋值“0”时,便会出现矛盾.现在,对于还要进行求解的由门g1,g2和g4生成的子句,根据定理1,对只出现这些子句的不可观条件中的变量13和14不再赋值,则问题转化为求g1,g2和g4生成的子句以及12=1的CNF的解,原问题变为部分电路的可满足问题求解,使搜索空间大大减小,且不会出现矛盾.4基于zChaff求解器的实现zChaff求解器是基于DPLL算法的,DPLL算法主要由变量决策、BCP、基于冲突的学习过程和非同步回溯构成.4.1变量决策变量决策顺序关系到搜索的规模,因此DPLL算法的效率对于决策顺序十分敏感.zChaff求解器中采用了非常有效的状态独立变量衰减和

10、(variablestate independent decaying sum, VSIDS)策略3进行变量决策.本文方法中,为了保证控制唯一属性,需要判断变量是否只出现在不可观条件中,所以每个文字需要2个计数器分别记录文字在子句中出现的总次数和只在一般子句部分出现的次数,即总VSIDS值和一般VSIDS值.在变量决策时,选取VSIDS值最高的文字,判断该文字的一般VSIDS值是否为空.如果不为空,则对该变量进行赋值;否则,不对该变量进行赋值,转为考虑下一个VSIDS值高的文字.本文中不需要记录变量的状态变化,对子句的满足情况也不需要区分其满足类型是一般满足还是忽略满足,统一用“满足”标记.4

11、.2BCPzChaff求解器中BCP过程是用两文字观察3数据结构实现的.因为两文字观察的目的是为了识别一元子句,产生相关的蕴含,而不可观条件中的文字是判断子句是否可观的,不能产生蕴含,所以一般文字和无关条件中的文字需要区别对待.只有2个观察文字被赋值时(子句满足,或产生蕴含),才对子句进行检查.对于子句的不可观条件中的文字,不需要进行观察.在BCP过程中只需对这些文字进行检查,看是否有某个文字的赋值为真.如果为真,则标记该子句为满足,在以后的计算中不再对该子句进行考虑,从而大大缩小问题求解搜索的空间.4.3冲突学习和非同步回溯冲突学习是避免对同一空间进行重复探索、提高求解器效率的重要方法,但学

12、习子句增加的同时会使求解规模增大.生成的冲突子句中可观无关条件的有效处理也可以有效地改进求解器的性能.为了使学习子句与电路的可观活动部分相关联,学习子句也要保留可观无关条件.可观无关条件的计算方法是学习子句所涉及到的消解子句的所有无关条件的并集,详见文献10.4.4无关条件的取舍本文方法可以利用的无关条件数比文献10方法多,但由于无关条件长度增加,占用的内存也随之增加,为了提高算法的有效性,需要限制无关条件的长度,可采取对无关条件进行裁剪或者限制计算无关条件传递的层数的方法,本文采用前一种方法.为了避免裁剪掉重要的无关项文字,在裁剪之前首先根据不可观条件中文字出现次数的多少保留影响大的文字,去

13、掉影响比较小的文字.5实验及结果分析我们在zChaff(2007.3.12版本)求解器的基础上,实现了本文提出的含有可观无关条件的CNF的求解器zChaff*.实验环境是SunBlade 2500工作站,1.6GHz CPU,8GB RAM,Solaris系统.为了应用电路的结构信息,采用自行开发的工具把基准电路的.bench描述转化为含有不可观条件的CNF描述.实验电路选择了文献10所用的ISCAS85系列组合基准电路和ITC99系列顺序基准电路.为了验证求解器zChaff*的有效性,把该工具应用于电路的等价验证,对组合基准电路和顺序基准电路的miter电路进行了实验.miter电路建立按照

14、文献11方法,用2个电路的结构描述(.bench),并将2个电路相对应的原始输出连接到一个异或门;然后把miter电路的结构描述分别转化为本文实验所需的传统CNF、带可观无关条件的CNF11和本文方法的CNF描述.实验结果如表2所示.表2实例中的b14-b14-opt和b15-b15-opt是顺序电路b14和b15与各自的优化电路所构成的miter电路,其他实例是由2个相同的电路构成的miter电路;最后一列为启发式静态排序方法与本文方法所需的时间比值.从实验结果可以看出,除c6288电路外,本文方法比基于启发式静态排序方法在速度上有进一步提高,有的可以提高几倍.对无关条件的长度,我们采用了文

15、献10中的参数,长度约束为正常文字长度的一半.假设一个含有控制输入的门有n个输入,采用静态排序的方法,这n个输入的不可观条件的长度为0,1,n-1,总长度为n×(n-1)/2;采用本文的方法,这n个输入的不可观条件的长度均为n-1,总长度为n×(n-1),在不对可观无关条件进行裁减的情况下,是固定排序方法的2倍.在约束条件一样的情况下,本文方法中可观无关条件占用空间会小于该值.所以,可观无关条件所带来的存储空间实际需求不会有太大增加,本文方法可用很小的存储空间换取更快的求解速度.c6288电路是16位乘法器,是一个难解电路,3种方法不能在限制时间(45 000 s)内给出对该电路的求解结果.本文实验直接对miter电路建立CNF公式,得到的问题规模比