2018, Vol. 29
表 1(Table 1)
基于扩展规则的启发式#SAT求解算法
引用本文
王强, 刘磊, 吕帅. 基于扩展规则的启发式#SAT求解算法[J]. 软件学报, 2018, 29(11): 3517-3527.http://www.jos.org.cn/1000-9825/5298.htm
Wang Q, Liu L, Lü S. #SAT Solving Algorithms Based on Extension Rule Using Heuristic Strategies[J]. Journal of Software, 2018, 29(11): 3517-3527(in Chinese).http://www.jos.org.cn/1000-9825/5298.htm
基于扩展规则的启发式#SAT求解算法
1. 吉林大学 计算机科学与技术学院, 吉林 长春 130012;
2. 符号计算与知识工程教育部重点实验室(吉林大学), 吉林 长春 130012
2. 符号计算与知识工程教育部重点实验室(吉林大学), 吉林 长春 130012
摘要:
#SAT在人工智能领域取得了广泛应用，很多现实问题可以规约成#SAT进行求解，得到命题理论的模型个数.通过对基于扩展规则的#SAT求解器的深入研究，发现选择规约子句的顺序对极大项空间的大小有着较大的影响，因此提出两种加速#SAT求解的启发式策略：MW和LC&MW.MW每次选择具有最大权值的子句作为规约子句；LC&MW每次选择最长子句作为规约子句，若最长子句存在多个，则在多个最长子句中选择具有最大权值的子句作为规约子句.利用MW策略设计了算法CER_MW，利用LC&MW策略设计了算法CER_LC&MW.实验结果表明，CER_MW和CER_LC&MW相对于先前的#SAT求解算法在求解效率和求解能力上都有显著的提高.在求解效率方面，CER_MW和CER_LC&MW的求解速度是其他算法的1.4倍~100倍.在求解能力方面，CER_MW和CER_LC&MW在限定时间内可解的测试用例更多.
关键词:
扩展规则
模型计数
启发式算法
极大项空间
规约子句
#SAT Solving Algorithms Based on Extension Rule Using Heuristic Strategies
1. College of Computer Science and Technology, Jilin University, Changchun 130012, China;
2. Key Laboratory of Symbolic Computation and Knowledge Engineering(Jilin University), Ministry of Education, Changchun 130012, China
2. Key Laboratory of Symbolic Computation and Knowledge Engineering(Jilin University), Ministry of Education, Changchun 130012, China
Foundation item: National Natural Science Foundation of China (61300049, 61402195, 61502197, 61503044); Specialized Research Fund for the Doctoral Program of Higher Education of China (20120061120059); Natural Science Research Foundation of Jilin Province (20180101053JC); Natural Science Research Foundation of Jilin Province for Young Scholars (20140520069JH, 20150520058JH)
Abstract:
#SAT is used widely in the field of artificial intelligence, and many real-world problems can be reduced to #SAT to get the number of models of a propositional theory. By an in-depth study of #SAT solvers using extension rule, this paper finds that the order of reduction clause has great impact on the size of maxterm space. Thus, in this paper two heuristic strategies, MW and LC&MW are proposed to enhance the efficiency of solving #SAT. MW chooses the clause with maximum weight as reduction clause in every calling procedure; LC&MW chooses the longest clause as reduction clause in every calling procedure and takes the clause with maximum weight as tie breaker. The algorithm CER_MW is designed by using MW, and the algorithm CER_LC&MW is designed by using LC&MW. According to the experimental results, CER_MW and CER_LC&MW show a significant improvement over previous #SAT algorithms. Comparing the new #SAT solvers with other state-of-the-art #SAT solvers using extension rule also shows that CER_MW and CER_LC&MW are significantly improved over the previous #SAT algorithms in solving efficiency and solving capacity. In terms of efficiency, the speed of CER_MW and CER_LC&MW is 1.4~100 times that of other algorithms. In terms of capacity, CER_MW and CER_LC&MW can solve more instances in a time limit.
Key words:
extension rule
model counting
heuristic strategy
maxterm space
reduction clause
可满足性问题(SAT问题)是逻辑学中的一个经典问题, 也是目前计算机科学和人工智能研究的核心问题, 无论在理论研究还是在实际应用方面, 都起着至关重要的作用[1].SAT问题是判断一个给定的命题公式是否存在可满足的指派, 它是第1个被证明的NP完全问题[2], 很多其他NP完全问题都可以在多项式时间内转化成SAT问题进行求解.每年一届的SAT比赛, 使得SAT问题求解技术日益成熟, 求解效率和求解能力都得到了显著提高.SAT问题的求解算法主要包括完备算法和不完备算法:完备算法求解准确, 但是效率较低; 不完备算法求解效率较高, 但是不一定能找到解.
伴随着SAT技术的发展, 其扩展问题的研究也取得了一定的进展.SAT问题的扩展问题主要包括:
● MAXSAT问题[3, 4], 主要是求得一个可满足的指派, 使子句集中可满足的子句数最多.
● #SAT问题, 又称模型计数, 用来计算给定命题公式的可满足指派的个数, 也就是模型的个数.
● SMT问题[5, 6], 是SAT问题在一阶逻辑方面的应用, 能处理更加复杂的问题, 针对不同的理论, 发展出了不同的研究分支.
● #SMT问题[7], 用来求解SMT问题可满足空间的大小.
SAT问题的可满足空间是离散的, 所以#SAT可以求解得到具体的模型数; 而SMT问题的可满足空间是连续的, 所以#SMT问题相当于求解SMT问题的可满足空间的体积大小.
#SAT问题的主要目的是计算给定命题公式的可满足指派的个数, 目前的主流#SAT求解器主要分为两类:直接求解器(direct model counter)和基于编译的求解器(compilation-based model counter).直接求解器的输入为CNF公式或子句集, 直接调用算法进行求解; 基于编译的求解器首先将输入的CNF公式或子句集编译成其他范式的形式, 再调用相应的方法求解, 求解过程是间接的.一般来讲, 基于编译的求解器的求解能力较强, 通常用于求解规模较大或求解较为困难的问题, 但其在求解效率方面低于直接求解器[8].而在实际问题的应用中, 通常对求解效率的要求较高, 因此直接求解器的应用范围更加广泛, 本文所讨论的求解方法是直接求解的方法.
直接求解主要包括精确求解和近似求解:精确求解是在可满足空间中调用算法进行精确的计数, 最终得到的模型数是精确的, 是一种完备的算法; 而近似求解是先精确求解某个子空间的模型数, 通过子空间占整体解空间的比例大小和子空间的精确模型数来估算整体解空间的近似模型数, 是一种不完备的算法, 通常用来求解规模较大的问题.Birnbaum等人直接将DP过程扩展到#SAT求解中, 提出了一个#SAT求解器CDP[9], 为#SAT求解器的发展奠定了基础, 现有的#SAT求解器大多基于CDP进行改进实现.Bayardo等人基于CDP提出了连接组件分析策略, 提高了relsat在模型计数方面的求解能力[10].Sang等人使用组件缓存技术和子句学习技术提出了著名的Cachet求解器[11, 12], 该求解器调用了SAT求解器zChaff[13], 通过记录冲突和子公式模型个数, 极大地简化了求解过程, 该求解器也是目前应用范围最广泛的#SAT求解器之一.Thurley提出了sharpSAT求解器[14], 引入了BCP策略与新的缓冲管理模式, 求解效率相比Cachet有了进一步的提高.Davies等人利用附加的推理机制减小了#SAT求解器的搜索空间, 提出了#2csleq求解器[15], 在部分benchmark上的求解速度优于sharpSAT.
2003年, Lin等人提出了扩展规则推理方法(extension rule, 简称ER)[16, 17], 被著名人工智能专家Davis称为与归结方法互补的方法.与归结方法相反, 扩展规则推理方法通过扩展出所有极大项组成的集合判定子句集的可满足性.殷明浩等人将扩展规则应用到#SAT问题中, 通过将问题求解沿着归结的反方向进行, 并利用容斥原理解决由此带来的空间复杂性问题, 提出了一种基于扩展规则的#SAT求解算法CER[18], 其主要思想是, 对于子句集T, 利用容斥原理求得T能够扩展出的所有极大项个数; 然后用极大项空间的大小减去T能扩展出的所有极大项个数, 就得到了模型数.CER直接将扩展规则应用到#SAT问题中, 其空间消耗过大, 求解效率较低.赖永等人设计了不同于#DPLL的#SAT求解算法#ER[19], 该算法能够选择具有不同特征的子句进行递归求解, 并且在递归调用的同时使用单文字规则对问题进行化简, 结合#DPLL和#ER的求解能力提出了混合#SAT求解算法#CDE[19].该算法结合前两种算法的优点, 较#ER表现出了更高的求解效率, 在互补因子较低的子句也有很好的表现.贾凤雨等人先后提出了重用极大项相交集计算结果的增量求解算法RCER[20]和结合互补度求解算法CDCER[21], 这两种算法都减少了CER算法的冗余计算, 在互补因子较低的测试用例中, 求解效率较CER提升显著.Wang等人将扩展规则方法推广到了近似模型计数中, 提出了ULBApprox和SampleApprox[22], ULBApporx将CER算法中的极大项个数的下界或上界作为近似的模型数, 而SampleApprox是在SampleSat算法[23]的基础上引入扩展规则来计算近似模型数, 这两种算法也是扩展规则应用于近似模型计数的首次尝试.
为了提高基于扩展规则的#SAT求解器的求解效率, 本文提出了两种启发式策略:MW(maximum weight)策略和LC&MW(longest clause with maximum weight), 用于指导规约子句的选择, 使极大项空间规模显著减小.实验结果表明, 两种启发式策略都能够显著地提高算法的求解效率和求解能力.
本文第1节对扩展规则推理方法以及符号定义进行简要阐述, 详细介绍两种基于扩展规则的模型计数算法:CER和#ER, 并分析二者在求解过程中存在的不足.第2节给出启发式策略MW和LC&MW, 分别给出基于这两种的策略的求解框架.第3节对比分析各种算法在不同测试用例中的求解效率和求解能力.最后总结全文, 并对下一步工作进行展望.
1 扩展规则本节给出符号定义以及扩展规则相关的基础知识.
我们对符号进行约定, 令T={C1, …, Cn}, X={x1, …, xm}, 其中, T表示一个子句集或CNF公式; Ci(i∈{1, …, n})表示一个非重言式子句; X表示出现在子句集T中的所有变量的集合; xi(i∈{1, …, m})表示一个变量; l表示一个文字, ¬l表示该文字的否定, 每个文字在子句中至多出现一次, 一个子句被称为极大项当且仅当它包含变量集X的所有变量; Max(T)表示子句集T所扩展出的所有极大项个数; Max(C)表示子句C所扩展出的所有极大项个数; M(T)表示子句集T的模型个数.
定义1(扩展规则(extension rule))[16]. 给定一个子句C和一个变量集X, x是X中的一个元素, D={C∨x, C∨¬x}, 其中, a∈X并且x和¬x都不在C中出现, 将C到D的推导过程称为扩展规则, D为C使用扩展规则得到的结果, 并且C与D在可满足性上等价.
由定义1可以看出, 扩展规则与归结规则是互补的推理方法; 同时, 定义1应用扩展规则后得到的子句集与原子句集等价.因此, 扩展规则可以被看作是一条新的推理规则.该推理规则的基本思想是, 将子句集中的所有子句全部扩展成极大项的形式, 通过极大项的个数来判定子句集的可满足性, 利用容斥原理可以很方便地计算极大项的个数[16].
下面简要介绍基于扩展规则的#SAT求解方法的基本思想.给定子句集T={C1, …, Cn}和变量集X={x1, …, xm}, CER[18]的主要思想是, 利用容斥原理求得T能扩展出的所有极大项个数Max(T), 然后用极大项空间的大小2m减去T能扩展出的所有极大项个数, 就得到了模型数, 即M(T)=2m−Max(T).CER直接在极大项空间上进行计数, 内存消耗较大, 因此求解能力与求解效率较低.
#ER[19]的主要思想是, 在子句集中随机选择规约子句C', 令T'=T−{C'}, 根据CER的思想可知:
| $ \text{Max}(T)-\text{Max}({T}')=M({T}')-M(T) $ | (1) |
因为对于子句集T和T'而言, 二者能够扩展出的极大项个数与其模型数之和都为2m.由式(1)有如下公式成立.
| $ M(T)=M({T}')-(\text{Max}(T)-\text{Max}({T}'))~ $ | (2) |
| $ M(T)=M({T}')-M({T}'\wedge \neg {C}') $ | (3) |
式(2)由式(1)进行变换得到, 而Max(T)−Max(T')与M(T'∧¬C')等价[19], 故公式(3)成立.由此可知, #ER可以利用规约子句C'来进行递归求解, 并且在递归求解的过程中, 由于¬C'的使用, 产生了大量的单文字, 因此, 该算法还能利用单文字规则对所要求解的问题进行化简, 在递归的同时, 也压缩了极大项空间的大小, 提高了求解效率.
2 MW策略和LC&MW策略在算法#ER[19]中, 每次选择规约子句对极大项空间进行规约时, 没有考虑子句之间的相互关系, 机械地采用顺序选择策略, 没有考虑启发式信息.针对同一子句集而言, 选择不同的子句作为规约子句会对极大项空间的规模产生较大的影响, 若极大项空间不能快速地进行规约, 会造成空间消耗过大、递归调用次数多等问题, 导致算法的时空效率降低.
例1:给定子句集T={x1∨x2, ¬x1∨x2∨x3, x1∨¬x3}, 变量集X={x1, x2, x3}.假设选择x1∨x2作为规约子句, 则T'= {¬x1∨x2∨x3, x1∨¬x3}, #ER算法的输入为子句集和变量集, 此时的返回结果为M(T, X)=M(T', X)−M(T', X−{x1, x2}); 假设选择¬x1∨x2∨x3作为规约子句, 则T'={¬x1∨x2∨x3, x1∨¬x3}, 此时的返回结果为M(T, X)=M(T', X)−M(T', X−{x1, x2, x3}).
观察例1中两种情况的返回结果, M(T', X−{x1, x2, x3}明显较M(T', X−{x1, x2}更容易进行计算, 前者的极大项空间为20, 而后者的极大项空间为21.选择¬x1∨x2∨x3作为规约子句所产生的单文字是3个, 而选择x1∨x2作为规约子句产生的单文字是2个, 子句和变量规模较大时, 产生的单文字个数越多, 越有利于单文字规则的使用, 极大项空间的规模也能迅速降低.尤其当子句和变量规模较大时, 选择规约子句的顺序会对算法的执行效率造成较大影响.因此, 本文设计了两种启发式策略MW和LC&MW, 并基于这两种策略分别设计了算法CER_MW和CER_ LC&MW来指导选择合适的规约子句, 从而显著地减小极大项空间的规模, 减少递归调用次数, 提高求解效率.
在介绍MW策略和LC&MW策略之前, 首先给出变量权值和子句权值的定义, 以此来确定选择规约子句时的优先顺序.
定义2(变量权值). 给定子句集T={C1, …, Cn}和变量集X={x1, …, xm}, x为变量集X中的任意一个变量, 记变量xi的权值为w(xi), w(xi)的大小为变量xi在子句集T中出现的次数.
定义3(子句权值). 给定子句集T={C1, …, Cn}和变量集X={x1, …, xm}, C为子句集X中的任意一个子句, 记子句C的权值为w(C), w(C)的大小为子句C包含的所有变量的权值之和, 即
| $ w(C) = \sum\limits_{i = 1}^k {w({x_i})} ,{\text{ }}k = |C| $ | (4) |
定义4(单文字规则). 若一个子句集中包含单文字l, 则可将l指派为真, 对除l外的任意子句C:
1) 若C包含l, 则从子句集中删除C;
2) 若C包含¬l, 则将¬l从C中删除;
3) 若C不包含l或¬l, 则不作处理.
2.1 MW策略MW策略的主要思想:在基于扩展规则的#SAT求解算法中, 每次选择规约子句来规约极大项空间时, 优先选择子句权值最大的子句作为规约子句.若存在两个子句的权值相同, 则随机地进行选择.
直观来讲, MW策略具有明显优势, 因为MW策略在选择规约子句时主要倾向于选择以下两种情况的子句:
1) 子句长度较大, 包含的变量数多;
2) 子句不一定是最长的, 但是所包含的变量在子句集中出现的次数较为频繁.
下面我们对这两种情况的子句进行分析.
● 针对情况1), 长度较大的子句所包含的变量数较多, 因此计算M(T'∧¬Ci)时所获得的单文字个数就越多, 使用单文字规则的次数可能会增加, 进而减少了计算M(T'∧¬Ci)的过程中的递归调用次数, 同时使得极大项空间的规模减小;
● 针对情况2), 规约子句所包含的变量在子句集中出现的次数较为频繁, 这样在使用单文字规则时, 可能会有更多的子句的长度减小, 进而有利于子句集产生更多的单文字或短子句, 也减小了极大项空间的规模, 可能会使求解效率提高.
下面描述MW策略的实现框架.
算法1. Init(T).
1) 初始化变量权值数组wv、子句权值数组wc
2) for (C∈T)
3) for (x∈C)
4) wv(x)+=1;
5) for (C∈T)
6) for (x∈C)
7) wc(C)+=wv(x).
算法1用于完成变量权值数组和子句权值数组的初始化工作, 在整体算法执行前完成.数组wv用来保存每一个变量的权值大小, 数组wc用来保存每一个子句的权值大小.算法1首先对数组wv和wc进行初始化为0, 随后依次遍历每个子句中的每一个变量, 完成变量权值的计算过程, 最后通过累加变量权值得到每一个子句的权值大小.
算法2. MW(T).
输入:子句集T.
输出:规约子句.
1) for (C∈T)
2) if (wc(C)＞Max) then
3) Max=wc(C);
4) C'=C;
5) return C'.
算法1已经得到了每个子句的权值数组, 算法2在算法1的基础上执行, 遍历子句集中的每一个子句, 返回具有最大子句权值的子句C'.
下面对基于MW策略的#SAT求解算法CER_MW进行描述.
算法3. CER_MW(T, X).
输入:子句集T、变量集X.
输出:子句集T的模型数.
1) if (T=∅) then
2) return 2|X|;
3) if (∅∈T) then
4) return 0;
5) if (T包含单元子句{l}, x是l的变量) then
6) return CER_MW({C−{¬l}|C∈T, l∉C}, X−{x});
7) C'=MW(T), x1, …, xk都是子句C'中的变量;
8) T'=T;
9) for (C∈T')
10) if (C'与C互补) then
11) 将C从T'中删除;
12) else if (C'≠C) then
13) 删除子句C中与C'相同的文字;
14) return CER_MW(T−{C'}, X)−CER_MW(T', X−{x1, …, xk}).
算法3的基本过程如下.
对子句集进行必要的判定操作:若子句集为空, 则直接返回模型数为2|X|; 若子句集包含空, 则直接返回模型数为0;若子句集中存在单文字, 使用单文字规则对子句集进行一定的规约, 递归调用规约后的子句集作为返回值.利用MW策略选择出规约子句C', 复制一个子句集T的副本T', 利用规约子句将T'的极大项空间进行规约.对T'中的任一子句C, 若C'与C互补, 将C从T'中删除; 否则, 删除子句C中与C'相同的文字.该过程相当于对¬C'所产生的单文字全部使用了单文字规则.利用公式(3)的特性进行递归计算, 得到子句集T的模型数.
2.2 LC&MW策略我们考虑到在选择规约子句时, 选择长度较大的子句作为规约子句可能更为重要, 因为子句长度越长, 相当于一次规约所减少的变量数越多.利用这一特征规约极大项空间更为稳定, 而考虑规约子句长度的同时, 也应尽可能的考虑变量出现的频率, 一旦可以使用单文字规则, 考虑这一因素有可能会使得子句集获得更多的单文字或短子句来减小极大项空间.因此, 本文提出了LC&MW策略.
LC&MW策略的主要思想:在基于扩展规则的#SAT求解算法中, 每次选择规约子句来规约极大项空间时, 优先选择子句长度最长的子句作为规约子句.一般情况下, 子句长度的取值范围较小, 所选择的最长子句一般存在多个.若存在多个最长子句, 在其中选择权值最大的子句作为规约子句.
下面描述LC&MW策略的实现框架.
算法4. LC&MW(T).
输入:子句集T.
输出:规约子句.
1) Σ={C|C∈T, ¬∃(C'∈T)L(C')＞L(C)};
2) return MW(Σ).
算法4中, 用L(C)表示任一子句C的长度.对子句集T中的任一子句C, 若不存在T中的其他子句C', 使得L(C')＞L(C), 则将子句C加入集合Σ.此时, Σ为长度最大的一个或多个子句的集合.再将子句集Σ调用算法2来选择规约子句.通过该算法选择的规约子句在首先保证子句长度的同时, 也尽可能地使得权值更大.
下面对基于LC&MW策略的#SAT求解算法CER_LC&MW进行描述.
算法5. CER_LC&MW(T, X).
输入:子句集T、变量集X.
输出:子句集T的模型数.
1) if (T=∅) then
2) return 2|X|;
3) if (∅∈T) then
4) return 0;
5) if (T包含单元子句{l}, x是l的变量) then
6) return CER_LC&MW({C−{¬l}|C∈T, l∉C}, X−{x});
7) C'=LC&MW(T), x1, …, xk都是子句C’中的变量;
8) T'=T;
9) for (C∈T')
10) if (C'与C互补) then
11) 将C从T'中删除;
12) else if (C'≠C) then
13) 删除子句C中与C'相同的文字;
14) return CER_LC&MW(T−{C'}, X)−CER_LC&MW(T', X−{x1, …, xk}).
算法5的执行流程与算法3基本相同, 仅在第7)行选择规约子句时改变了启发式策略, 利用LC&MW策略来选择规约子句.
3 实验部分在本节中, 将本文的CER_MW算法、CER_LC&MW算法与目前最优的几个基于扩展规则的#SAT求解算法进行了对比, 主要包括#ER[19], RCER[20]和CDCER[21].实验第1部分测试长度随机的SAT测试用例, 第2部分测试长度固定的SAT测试用例.本文的实验平台如下:Windows 8.1操作系统, CPU Intel(R) Core(TM) i7-4790 3.60GHz, RAM 8GB.
3.1 随机子句长度的SAT用例测试本文用随机产生器生成了子句长度不固定的测试用例, 随机产生器的结果为包含3个参数〈m, n, e〉的子句集, 其中, m为变量个数, n为子句个数, e为每个子句的最大长度.m个变量对应2×m个文字, 为了保证所生成测试集的质量, 随机产生器在生成每个文字时, 2×m个文字出现的概率是相同的, 同时控制生成过程, 避免生成重言式.为增加子句集的求解难度, 我们将子句的最小长度设定为3.目前, 基于扩展规则的求解方法都不能解决规模大的问题, 表 1~表 3中分别给出了〈20, n, 10〉, 〈30, n, 10〉和〈40, n, 10〉这3种变量数固定、子句数不同的随机测试用例的实验结果.实验结果为10次实验的平均值, time表示运行时间(单位为s), “−”表示在1 000s内无法对问题进行求解.
|
Table 1 Experimental results on random instances 〈20, n, 10〉 表 1 随机用例〈20, n, 10〉的实验结果 |
|
|
Table 2 Experimental results on random instances 〈30, n, 10〉 表 2 随机用例〈30, n, 10〉的实验结果 |
|
|
Table 3 Experimental results on random instances 〈40, n, 10〉 表 3 随机用例〈40, n, 10〉的实验结果 |
在表 1、表 2中, CER_MW和CER_LC&MW求解速度都快于RCER, CDCER和#ER, 其中, CER_MW比RCER快4倍~64.7倍, 比CDCER快5.5倍~93.5倍, 比#ER快1.4倍~4.3倍; CER_LC&MW比RCER快4倍~69倍, 比CDCER快5.5倍~100.2倍, 比#ER快1.4倍~4.5倍.表 1中, 二者求解速度相当, 其原因可能是因为子句集本身的规模较小, 求解时间相差不大, 也可能是因为每次使用MW策略所选择的最大权值子句同时也是最长子句; 表 2中, CER_LC&MW比CER_MW求解速度更快, 说明在选择规约子句的过程中, 子句长度这一因素发挥了更重要的作用.在表 3中, RCER和CDCER的求解已经非常吃力, 大部分问题已经无法求解, 因此我们仅给出了#ER, CER_MW和CER_LC&MW的对比结果.在表 3的9个测试用例中, #ER仅能求解前5个测试用例, 而CER_MW和CER_LC&MW可以求解所有测试用例, 在求解能力上较RCER, CDCER和#ER有较大的提高.
#ER, CER_MW和CER_LC&MW都是采用递归调用的方式来求解问题, MW和LC&MW策略能找到合适的规约子句, 使得极大项空间的规模快速减小, 进而使得递归调用次数减少, 提高了算法求解效率.下面我们给出#ER, CER_MW和CER_LC&MW的递归调用次数对比图, 图 1~图 3中分别给出了在〈20, n, 10〉, 〈30, n, 10〉和〈40, n, 10〉这3种变量数固定、子句数不同的随机测试用例中, #ER, CER_MW和CER_LC&MW的递归调用次数.
|
Fig. 1 Recursive times of algorithms on random instances 〈20, n, 10〉 图 1 随机用例〈20, n, 10〉的算法递归调用次数 |
|
Fig. 2 Recursive times of algorithms on random instances 〈30, n, 10〉 图 2 随机用例〈30, n, 10〉的算法递归调用次数 |
|
Fig. 3 Recursive times of algorithms on random instances 〈40, n, 10〉 图 3 随机用例〈40, n, 10〉的算法递归调用次数 |
从图 1~图 3可以看出, CER_MW和CER_LC&MW的递归调用次数要远小于#ER的递归调用次数.这是由于MW和LC&MW策略在选择规约子句时能选择到合适的规约子句, 使算法充分发挥扩展规则和单文字规则的优势, 迅速规约极大项空间, 进而加速求解过程.
3.2 长度固定的SAT用例测试本节针对长度固定的测试用例进行测试, 其生成方法与上节相同, 但限定子句的最大长度与最小长度都为n, 表 4、表 5中分别给出了〈30, 100, n〉和〈40, 200, n〉这两种变量数固定、子句长度不同的测试用例的实验结果, 表中参数与上节保持一致.
|
|
Table 4 Experimental results on random instances 〈30, 100, n〉 表 4 随机用例〈30, 100, n〉的实验结果 |
|
|
Table 5 Experimental results on random instances 〈40, 200, n〉 表 5 随机用例〈40, 200, n〉的实验结果 |
在本节的测试用例中, LC&MW策略不再适用, 因为测试用例中的子句长度都相等, LC&MW与MW策略选择的规约子句一定相同.因此, 我们仅给出了RCER, CDCER, #ER和CER_MW的对比结果.
在表 4、表 5中, 对于固定长度的测试用例, 其子句长度对该子句集的互补因子有着一定的影响, 子句长度相对越大, 子句两两之间互补的可能性就越大.从表中可以看出, 子句长度与子句集的互补因子是正相关的, 扩展规则推理方法擅长求解互补因子较高的测试用例, 因此当互补因子较高时, 4种算法的求解速度较快; 而随着互补因子的减小, 受扩展规则方法本身的影响, 算法的求解速度会变慢.从表中的数据可以看出, 无论在互补因子较高的测试用例, 还是在互补因子较低的测试用例中, CER_MW的求解效率都高于RCER、CDCER和#ER.
4 总结与展望选择规约子句的顺序对极大项空间的大小有着较大的影响, 为此, 本文提出了两种启发式策略:MW策略和LC&MW策略.MW每次选择具有最大权值的子句作为规约子句; LC&MW每次优先选择最长子句作为规约子句来减小极大项空间, 若最长子句存在多个, 则在多个最长子句中选择具有最大权值的子句作为规约子句.本文根据MW策略和LC&MW策略分别设计了#SAT求解算法CER_MW和CER_LC&MW, 实验结果表明, CER_MW和CER_LC&MW相对于先前的#SAT求解算法在求解效率和求解能力上都有显著的提高.在求解效率方面, CER_MW和CER_LC&MW的求解速度是其他算法的1.4倍~100倍; 在求解能力方面, CER_MW和CER_LC&MW在限定时间内可解的测试用例更多.
目前, 虽然基于扩展规则的求解算法在互补因子较高的测试用例上优势明显, 但受扩展规则本身的特性所限, 其求解能力并不高, 对于变量和子句规模较大的测试用例求解较为困难.未来将进一步研究如何通过启发式策略或局部搜索的思想来提升#SAT求解算法的求解能力, 使得基于扩展规则的方法适用于大规模的测试用例.
参考文献
| [1] |
Biere A, Heule M, Maaren HV, Walsh T. Handbook of Satisfiability. IOS Press, 2009: 195-203.
|
| [2] |
Cook SA. The complexity of theorem-proving procedures. In: Proc. of the 3rd Annual ACM Symp. on Theory of Computing. New York: ACM Press, 1971. 151-158.https://www.mendeley.com/catalogue/complexity-theoremproving-procedures/ |
| [3] |
Cai S, Luo C, Lin J, Su K. New local search methods for partial MaxSAT. Artificial Intelligence, 2016, 240: 1–18.
[doi:10.1016/j.artint.2016.07.006] |
| [4] |
Ansótegui C, Gabàs J, Malitsky Y, Sellmann M. MaxSAT by improved instance-specific algorithm configuration. Artificial Intelligence, 2016, 235: 26–39.
[doi:10.1016/j.artint.2015.12.006] |
| [5] |
Frohlich A, Biere A, Wintersteiger CM, Hamadi AY. Stochastic local search for satisfiability modulo theories. In: Proc. of the 29th AAAI Conf. on Artificial Intelligence. Menlo Park: AAAI, 2015. 1136-1143.http://www.aaai.org/ocs/index.php/AAAI/AAAI15/paper/view/9896 |
| [6] |
Zhang HT. An experiment with satisfiability modulo SAT. Journal of Automated Reasoning, 2016, 56(2): 143–154.
[doi:10.1007/s10817-015-9354-0] |
| [7] |
Chakraborty S, Meel KS, Mistry R, Vardi MY. Approximate probabilistic inference via word-level counting. In: Proc. of the 30th AAAI Conf. on Artificial Intelligence. Menlo Park: AAAI, 2016. 3218-3224.http://cn.arxiv.org/abs/1511.07663 |
| [8] |
Lagniez JM, Marquis P. On preprocessing techniques and their impact on propositional model counting. Journal of Automated Reasoning, 2017, 58(4): 413–481.
[doi:10.1007/s10817-016-9370-8] |
| [9] |
Birnbaum E, Lozinskii EL. The good old Davis-Putnam procedure helps counting models. Journal of Artificial Intelligence Research, 1999, 10(1): 457–477.
http://d.old.wanfangdata.com.cn/OAPaper/oai_arXiv.org_1106.0218 |
| [10] |
Bayardo RJ, Pehoushek JD. Counting models using connected components. In: Proc. of the 17th National Conf. on Artificial Intelligence and 20th Conf. on Innovative Applications of Artificial Intelligence. Menlo Park: AAAI, 2000. 157-162.https://www.mendeley.com/catalogue/counting-models-using-connected-components/ |
| [11] |
Sang T, Beame P, Kautz H. Heuristics for fast exact model counting. In: Proc. of the Int'l Conf. on Theory and Applications of Satisfiability Testing. Berlin: Springer-Verlag, 2005. 226-240.https://link.springer.com/chapter/10.1007%2F11499107_17 |
| [12] |
Sang T, Bacchus F, Beame P, Kautz H, Pitassi T. Combining component caching and clause learning for effective model counting. In: Proc. of the Int'l Conf. on Theory and Applications of Satisfiability Testing. Berlin: Springer-Verlag, 2004. 20-28. |
| [13] |
Zhang L, Madigan CF, Moskewicz MH, Mailk S. Efficient conflict driven learning in a Boolean satisfiability solver. In: Proc. of the IEEE/ACM Int'l Conf. on Computer-Aided Design. New York: IEEE, 2001. 279-285.http://ieeexplore.ieee.org/xpls/icp.jsp?arnumber=968634 |
| [14] |
Thurley M. sharpSAT: Counting models with advanced component caching and implicit BCP. In: Proc. of the Int'l Conf. on Theory and Applications of Satisfiability Testing. Berlin: Springer-Verlag, 2006. 424-429.https://link.springer.com/chapter/10.1007%2F11814948_38 |
| [15] |
Davies J, Bacchus F. Using more reasoning to improve #SAT solving. In: Proc. of the 22nd AAAI Conf. on Artificial Intelligence. Vancouver: AAAI, 2007. 185-190.https://www.mendeley.com/catalogue/using-more-reasoning-improve-sat-solving/ |
| [16] |
Lin H, Sun JG, Zhang YM. Theorem proving based on the extension rule. Journal of Automated Reasoning, 2003, 31(1): 11–21.
[doi:10.1023/A:1027339205632] |
| [17] |
Lin H, Sun JG. Knowledge compilation using the extension rule. Journal of Automated Reasoning, 2004, 32(2): 93–102.
[doi:10.1023/B:JARS.0000029959.45572.44] |
| [18] |
Yin MH, Lin H, Sun JG. Solving #SAT using extension rule. Ruan Jian Xue Bao/Journal of Software, 2009, 20(7): 1714–1725(in Chinese with English abstract).
http://www.jos.org.cn/jos/ch/reader/view_abstract.aspx?flag=1&file_no=3320&journal_id=jos [doi:10.3724/SP.J.1001.2009.03320] |
| [19] |
Lai Y, Ouyang DT, Cai DB, Lü S. Model counting and planning using extension rule. Journal of Computer Research and Development, 2009, 46(3): 459–469(in Chinese with English abstract).
http://d.old.wanfangdata.com.cn/Periodical/jsjyjyfz200903014 |
| [20] |
Jia FY, Ouyang DT, Zhang LM, Liu SG. Reconstructive algorithm based on extension rule for solving #SAT incrementally. Ruan Jian Xue Bao/Journal of Software, 2015, 26(12): 3117–3129(in Chinese with English abstract).
http://www.jos.org.cn/jos/ch/reader/view_abstract.aspx?flag=1&file_no=4827&journal_id=jos [doi:10.13328/j.cnki.jos.004827] |
| [21] |
Ouyang DT, Jia FY, Liu SG, Zhang LM. An algorithm based on extension rule for solving #SAT using complementary degree. Journal of Computer Research and Development, 2016, 53(7): 1596–1604(in Chinese with English abstract).
http://d.old.wanfangdata.com.cn/Periodical/jsjyjyfz201607017 |
| [22] |
Wang J, Yin M, Wu J. Two approximate algorithms for model counting. Theoretical Computer Science, 2017, 657: 28–37.
[doi:10.1016/j.tcs.2016.04.047] |
| [23] |
Wei W, Erenrich J, Selman B. Towards efficient sampling: Exploiting random walk strategies. In: Proc. of the 19th National Conf. on Artificial Intelligence. AAAI, 2004. 670-676. |
| [18] |
殷明浩, 林海, 孙吉贵. 一种基于扩展规则的#SAT求解系统. 软件学报, 2009, 20(7): 1714–1725.
http://www.jos.org.cn/jos/ch/reader/view_abstract.aspx?flag=1&file_no=3320&journal_id=jos [doi:10.3724/SP.J.1001.2009.03320]
|
| [19] |
赖永, 欧阳丹彤, 蔡敦波, 吕帅. 基于扩展规则的模型计数与智能规划方法. 计算机研究与发展, 2009, 46(3): 459–469.
http://d.old.wanfangdata.com.cn/Periodical/jsjyjyfz200903014
|
| [20] |
贾凤雨, 欧阳丹彤, 张立明, 刘思光. 结合扩展规则重构的#SAT问题增量求解方法. 软件学报, 2015, 26(12): 3117–3129.
http://www.jos.org.cn/jos/ch/reader/view_abstract.aspx?flag=1&file_no=4827&journal_id=jos [doi:10.13328/j.cnki.jos.004827]
|
| [21] |
欧阳丹彤, 贾凤雨, 刘思光, 张立明. 结合互补度的基于扩展规则#SAT问题求解方法. 计算机研究与发展, 2016, 53(7): 1596–1604.
http://d.old.wanfangdata.com.cn/Periodical/jsjyjyfz201607017
|