2019, Vol. 40
SAT问题是判断给定命题公式是否存在可满足指派的过程, 而#SAT问题计算给定布尔公式的可满足指派的个数, 也就是模型计数.目前, #SAT求解器主要分为直接求解器和基于编译的求解器.基于编译的求解器在求解能力方面表现更突出, 但是求解效率不如直接求解器[1].
直接求解主要包括精确求解和近似求解.目前, 精确求解算法主要包括:1)Birnbaum和Lozinskii提出的基于DP的#SAT求解算法CDP(counting models using Davis-Putnam procedure)[2], 该算法基于归结原理实现, 归结原理的主要思想是通过推出空子句来判定给定子句集的不可满足性; 2)Sang等结合组件缓存和子句学习策略开发的Cachet求解器[3-4], 该系统调用了SAT求解器zChaff, 通过记录出现冲突和子公式模型个数来简化计算, 从而加快求解效率; 3)Thurley提出的sharpSAT求解器[5], 它与Cachet求解器相比加入了BCP策略, 并且修改了缓冲管理模式, 较Cachet在求解效率上有了较大的提高.此外, 近似求解算法主要包括SampleCount, ApproxCount等；基于编译的求解器包括C2D, Dsharp, SDD, cnf2obdd等.
扩展规则[6]是归结原理的一种补方法，殷明浩等[7]首次将扩展规则应用到#SAT问题中, 提出了一种基于扩展规则的#SAT求解算法CER, 但其存在空间消耗过大、求解速度慢等问题.为此, 在CER的基础上，赖永等[8]设计了不同于#DPLL的#SAT求解算法#ER, 之后融合#DPLL和#ER的求解能力提出了混合#SAT求解算法#CDE, 该算法结合前两种算法的优点, 较#ER表现出了更高的求解效率.贾凤雨等[9-10]先后提出了重用极大项相交集计算结果的增量求解算法RCER和结合互补度求解算法CDCER, 这两种算法都是通过加入启发式策略避免了CER的重复计算, 弥补了CER在互补因子较低时求解效率不足的问题.Wang等[11]将CER扩展到了近似求解算法中, 提出两种用于近似模型计数的算法ULBApprox和SampleApprox, 展现了良好的求解效率.
本文结合现有的#SAT求解器, 设计了一种新的基于扩展规则的#SAT求解算法NCER(novel algorithm for counting models using extension rule), 在#ER的基础上加入启发式策略.将NCER和CDP的优点相结合, 提出混合#SAT求解算法NCDPER(novel algorithm for counting models using Davis-Putnam procedure and extension rule), 克服了扩展规则在互补因子较低的样例中效率低的问题.
1 扩展规则给定子句集T={C1, …, Cn}和变量集X={x1, …, xm}.一个文字是一个变量x或者它的否定¬x, 一个子句是文字的析取形式.一个CNF公式由若干子句合取组成, 可以将其看成子句集.
定义1 (扩展规则, extension rule)[12].对于子句集T中的子句C和变量集X, D={C∨x, C∨¬x}, 其中x是X中的元素且x与¬x都不在C中出现, 则D是C使用扩展规则得到的结果.
扩展规则用于#SAT求解时, 一般与容斥原理结合使用, 直接通过计数方法来计算模型数, 而互补的子句对在计数时扩展出的极大项不会相交, 在容斥原理的计数过程中直接返回0.因此基于扩展规则的#SAT求解算法在互补因子较高的子句集上较为高效.
定义2 (极大项, maxterm).一个子句被称为极大项, 当且仅当它包含变量集X的所有变量.
对任意给定的非极大项子句C, 都可以利用扩展规则得到一个由C扩展出的极大项集.
定义3 (PCNF, principle conjunctive normal form).PCNF公式是CNF公式, 且PCNF公式中的每一个子句都是极大项.
每一个CNF公式, 都有一个PCNF公式与其一一对应, CER就是利用扩展规则将所要求解的CNF公式扩展成PCNF公式, 再用极大项空间大小2|X|减去PCNF公式中的极大项个数, 得到模型数.
定义4[13]子句集T所扩展出的极大项是指其扩展出的PCNF公式包含的极大项, 用MC(T)表示.
特别地, 对于一个子句C, 用MC(C)表示其覆盖的极大项.给定子句集T, 则有
|
推论1 给定子句集T, 变量集X, M(T)表示模型的集合, 则T的模型数为|M(T)|=2|X|－|MC(T)|, 称MC(T)与M(T)在变量集X上互补.
根据利用扩展规则求解#SAT问题的性质, 容易得出MC(T)∪M(T)即为全部极大项的集合, 因此上述推论成立.
2 新的#SAT求解算法NCER给定子句集T和变量集X.令T′=T－{Ci}(i∈{1, …, n}), 根据推论1, MC(T)与M(T)在变量集X上互补, 因此|MC(T)－MC(T′)|=|M(T′)－M(T)|.
由|MC(T)－MC(T′)|=|MC(T′∨Ci)|=|M(T′∧¬Ci)|[8]知:|M(T′)－M(T)|=|M(T′∧¬Ci)|.由于M(T)和M(T′)都是极大项集, 有|M(T′)|－|M(T)|=|M(T′∧¬Ci)|成立, 即
|
(1) |
#ER根据式(1)设计, 每次随机选择子句Ci来进行递归求解, 一方面减少了极大项的空间, 另一方面使用单文字规则对问题进行化简, 提高了求解的效率.递归调用最终得到的结果是子句集T的模型数.
尽管#ER已经通过单文字规则对问题进行了化简, 但是由于选择子句C是随机选择的, 子句集规模不一定是以最快的速度减小的, 导致递归调用的次数未必是最少的.
为了解决#ER递归调用次数过多问题, 在#ER的基础上加入了一种启发式策略, 每次选择子句Ci时, 都选取当前子句集中长度最长的子句, 因为最长的子句包含的变量个数多, 能保证子句集规模以最快速度减小.根据式(1)可知, 若子句Ci的长度越长, 公式T′∧¬Ci中的单文字就越多, T′ 的变量集变得更小, 会大幅度地减少递归调用的次数.下面给出NCER的算法描述.
| 算法1.NCER(T, X). |
| 输入:子句集T、变量集X; 输出:子句集T的模型数. |
|
①if (T=Ø) then ② return 2|X|; ③if (Ø∈T) then ④ return 0; ⑤if(T包含单元子句{l}, x是l的变量)then ⑥ return NCER ({C－{¬l}|C∈T, l∉C}, X－{x}); ⑦在T中选择长度最长的子句Ci, x1, …, xk都是子句Ci中的变量; ⑧T′=T; ⑨for (C′∈T′) ⑩ if (C′与C互补)then B11 将C′从T′中删除; B12 else if(C≠C′)then B13 删除子句C′中与C相同的文字; B14 return NCER(T－{Ci}, X)－NCER(T′, X－{x1, …, xk}). |
NCER在#ER的基础上, 增加了一种启发式策略, 从而改变选择子句Ci的顺序, 因此NCER是正确的[8].#ER在递归调用时使用单文字规则来减小子句集规模, 加快了求解效率.NCER与#ER相比, 在选择子句Ci时优先选择子句长度较长的子句, 若最大长度的子句存在多个, 则随机选择其中一个.由⑦行可知, x1, …, xk是出现在子句Ci中的变量, 那么子句Ci的长度越长, B14行变量集合X－{x1, …, xk}的元素数就越少, 每一次都选择最长子句会使得T′的规模最大幅度地减小, 调用递归的次数也大幅度减少, 求解效率提高.
3 混合#SAT求解算法NCDPER为了弥补基于扩展规则的#SAT求解算法在互补因子较低的子句集上的不良表现, 设计了结合CDP和NCER优点的混合#SAT求解算法NCDPER, 该算法将子句集划分成互补因子较低的部分和互补因子较高的部分, 分别调用CDP和NCER进行求解, 增加基于扩展规则的#SAT求解算法在互补因子较低的测试用例上的竞争力.
定理1[11]对于公式T1∧T2, 有|M(T1∧T2)|=|M(T1)|－|M(T1∧¬T2)|.
#CDE根据定理1设计, 将原有的子句集T拆分成T1和T2两部分：T1中的子句全部为长度小于等于3的子句；T2为剩余部分.在子句个数和变量个数一定的情况下, 子句的最大长度越小, 子句集的互补因子相对就越低, 若子句集中的子句长度与变量集的大小相差过大, 子句之间两两互补的概率相解, 将互补因子较高的部分T2调用#ER求解可以充分发挥扩展规则和归结原理的优势.
NCDPER与#CDE同理, 对互补因子较低的部分T1调用CDP来求解, 而互补因子较高的部分T2则调用NCER求解.对子句集进行划分时, 通过子句的长度来进行划分是一种通常的做法.在#CDE中, SelectClause函数选择子句长度小于等于3的子句加入到T1中, 在随机SAT测试用例上对划分长度的标准进行了实验, 若SelectClause函数选择长度小于等于4的子句, 在绝大多数测试用例中执行效率会更高.因此, 在NCDPER中, SelectClause(T)函数选取长度小于等于4的子句加入T1.
| 算法2.NCDPER(T, X). |
| 输入:子句集T、变量集X; 输出:子句集T的模型数. |
| ①if(T=Ø)then ② return 2|X|; ③if (Ø∈T)then ④ return 0; ⑤if (T包含单元子句{l}, x是l的变量)then ⑥ return NCDPER ({C－{¬l}|C∈T, l∉C}, X－{x}); ⑦T1=SelectClause(T); T2=T－T1; number =0; ⑧将T2中的子句按长度从大到小排序; ⑨for (C∈T2) ⑩ x1, …, xk都是子句C中的变量; B11 T′ = T1; B12 for (C′∈T′) B13 if(C′与C互补)then B14 将C′从T′中删除; B15 else if(C≠C′)then B16 删除子句C′中与C相同的文字; B17 number+=NCDPER(T′, X－ {x1, …, xk}); B18 T1=T1∪{C′}; B19 return CDP(T－T2, X)－number. |
当SelectClause(T)返回空集时, NCDPER与NCER等价; 当SelectClause(T)返回T时, NCDPER与CDP等价.
4 实验与结果本节给出NCER和NCDPER与目前基于扩展规则的#SAT求解器比较结果, 并给出NCER与#ER的递归调用次数比较.实验采用子句个数为100、变量个数为30的随机SAT测试用例[13].测试环境为:Windows 8.1操作系统, CPU Intel (R) Core (TM) i7-4790 3.60 GHz, RAM 8 GB.
4.1 随机SAT测试用例实验结果为了说明NCER的高效性, 在随机SAT测试用例上进行了实验, 将NCER和NCDPER与目前最为高效的几个基于扩展规则的#SAT求解算法进行了对比.测试用例根据最大子句长度的设定来控制互补因子的大小, 互补因子取值均匀地分布在0.1至0.9之间.表 1和表 2给出了RCER, CDCER, #ER, NCER, #CDE和NCDPER在这些随机SAT测试用例上的部分实验结果.结果中给出了每一个测试用例的互补因子大小、模型数和各类算法的10次实验平均求解时间.
|
表 1 随机SAT用例实验结果(互补因子 < 0.5) Table 1 Experimental results of random SAT instances(complementary factor < 0.5) |
|
|
表 2 随机SAT用例实验结果(互补因子>0.5) Table 2 Experimental results of random SAT instances(complementary factor>0.5) |
从表 1和表 2的实验结果可以看出, NCER几乎在所有的随机SAT样例中的效果均要好于#ER, 而NCDPER与#CDE相比, 也在绝大多数的样例中占有优势.在互补因子小于0.5的测试用例中, NCER的效率虽然低于#CDE和NCDPER, 但是较#ER已经有了很大提高, 已经最大程度地降低了递归调用的次数.在互补因子大于0.5的测试用例中, NCER充分发挥了扩展规则的优势, 单文字规则在每次递归过程中的使用使得子句集的规模迅速减小, 同时每次调用递归过程的时候利用启发式策略选择最长子句极大降低了递归调用的次数, 在所有的85个求解样例中求解效率最高.
4.2 #ER与NCER递归调用次数对比图 1, 图 2给出了#ER与NCER在随机SAT测试用例上的递归调用次数的对比图, 其中图 1为互补因子小于0.5的测试用例两种算法的递归调用次数对比图, 图 2为互补因子大于0.5的测试用例两种算法的递归调用次数对比图.
|
图 1 表 1测试用例#ER与NCER递归次数比较图 Fig.1 Comparison of numbers of recursive invocation of #ER and NCER on the instances of Table 1 |
|
图 2 表 2测试用例#ER与NCER递归次数比较图 Fig.2 Comparison of numbers of recursive invocation of #ER and NCER on the instances of Table 2 |
通过图 1可以看出, 对表 1的测试用例而言, #ER递归调用次数非常高, 而NCER优先选取最长子句减小极大项空间的启发式策略, 最大程度地减少了计算过程, 使得递归调用次数锐减, 从而
加快了求解速率.图 1中NCER的递归调用次数全部小于#ER的递归调用次数, 其中最大差值为24 569 456次, 最小差值为644 969次.
通过图 2可以看出, 首先#ER和NCER的递归调用次数相比于图 1中的调用次数有了大幅度减小, 这是因为表 2的测试用例互补因子较高, 利用了扩展规则的优势, 且NCER使用的启发式策略在每次调用时优先选择最长子句, 最大程度地减小了极大项空间, 从而使得递归调用的次数较少.图 2中NCER的递归调用次数均小于#ER的递归调用次数, 其中最大差值为542 518次.
5 结论本文提出了一种基于扩展规则的新型#SAT求解算法NCER.相比于传统的基于扩展规则的#SAT求解算法, 能更有效地减小每次调用算法时的子句集规模, 减少冗余计算, 提高求解效率.NCER在#ER的基础上, 加入了启发式策略, 每次选择当前子句集的最长子句来减小极大项空间, 使得递归调用的次数减少.利用子句集在不同划分情况下的实验结果, 提出了NCDPER, NCDPER在#CDE的基础上修改了拆分子句集时的参数, 将互补因子较低的子句集用CDP算法来求解, 而互补因子较高的子句集用NCER来求解, 克服了基于扩展规则的求解算法在互补因子较低的子句集中求解效率低下的问题.实验结果表明, 本文提出的NCER与NCDPER算法在绝大多数测试用例中的求解效率优于现有的基于扩展规则的#SAT求解算法.
| [1] |
Lagniez J M, Marquis P.
On preprocessing techniques and their impact on propositional model counting[J]. Journal of Automated Reasoning, 2017, 58(4): 1–69.
|
| [2] |
Birnbaum E, Lozinskii E L.
The good old Davis-Putnam procedure helps counting models[J]. Journal of Artificial Intelligence Research, 1999, 10(1): 457–477.
|
| [3] |
Sang T, Beame P, Kautz H.Heuristics for fast exact model counting[C]//International Conference on Theory and Applications of Satisfiability Testing.Berlin: Springer, 2005: 226-240.
|
| [4] |
Sang T, Bacchus F, Beame P, et al.Combining component caching and clause learning for effective model counting[C]//International Conference on Theory and Applications of Satisfiability Testing.Berlin: Springer, 2004: 20-28.
|
| [5] |
Thurley M.sharpSAT: counting models with advanced component caching and implicit BCP[C]//International Conference on Theory and Applications of Satisfiability Testing.Berlin: Springer, 2006: 424-429.
|
| [6] |
Lin H, Sun J G, Zhang Y M.
Theorem proving based on extension rule[J]. Journal of Automated Reasoning, 2003, 31(1): 11–21.
|
| [7] |
殷明浩, 林海, 孙吉贵.
一种基于扩展规则的#SAT求解系统[J]. 软件学报, 2009, 20(7): 1714–1725.
( Yin Ming-hao, Lin Hai, Sun Ji-gui. Solving #SAT using extension rules[J]. Journal of Software, 2009, 20(7): 1714–1725. ) |
| [8] |
赖永, 欧阳丹彤, 蔡敦波, 等.
基于扩展规则的模型计数与智能规划方法[J]. 计算机研究与发展, 2009, 46(3): 459–469.
( Lai Yong, Ouyang Dan-tong, Cai Dun-bo, et al. Model counting and planning using extension rule[J]. Journal of Computer Research and Development, 2009, 46(3): 459–469. ) |
| [9] |
贾凤雨, 欧阳丹彤, 张立明, 等.
结合扩展规则重构的#SAT问题增量求解方法[J]. 软件学报, 2015, 26(12): 3117–3129.
( Jia Feng-yu, Ouyang Dan-tong, Zhang Li-ming, et al. Reconstructive algorithm based on extension rule for solving #SAT incrementally[J]. Journal of Software, 2015, 26(12): 3117–3129. ) |
| [10] |
欧阳丹彤, 贾凤雨, 刘思光, 等.
结合互补度的基于扩展规则#SAT问题求解方法[J]. 计算机研究与发展, 2016, 53(7): 1596–1600.
( Ouyang Dan-tong, Jia Feng-yu, Liu Si-guang, et al. An algorithm based on extension rule for solving #SAT using complementary degree[J]. Journal of Computer Research and Development, 2016, 53(7): 1596–1600. ) |
| [11] |
Wang J, Yin M, Wu J.
Two approximate algorithms for model counting[J]. Theoretical Computer Science, 2017, 657: 28–37.
DOI:10.1016/j.tcs.2016.04.047 |
| [12] |
Lin H, Sun J G.
Knowledge compilation using extension rule[J]. Journal of Automated Reasoning, 2004, 32(2): 93–102.
DOI:10.1023/B:JARS.0000029959.45572.44 |
| [13] |
Yin L, He F, Hung W N N, et al.
Maxterm covering for satisfiability[J]. IEEE Transactions on Computers, 2012, 61(3): 420–426.
DOI:10.1109/TC.2010.270 |