两种新的基于扩展规则#SAT问题求解算法

doi:10.12068/j.issn.1005-3026.2019.05.005

东北大学学报:自然科学版 ›› 2019, Vol. 40 ›› Issue (5): 630-635.DOI: 10.12068/j.issn.1005-3026.2019.05.005

两种新的基于扩展规则#SAT问题求解算法

吕帅，张桐搏，王强，刘磊

(吉林大学计算机科学与技术学院，吉林长春130012)

收稿日期:2018-03-26 修回日期:2018-03-26 出版日期:2019-05-15 发布日期:2019-05-17
通讯作者: 吕帅
作者简介:吕帅(1981-)，男，吉林公主岭人，吉林大学副教授；刘磊(1960-)，男，吉林长春人，吉林大学教授，博士生导师.
基金资助:
国家重点研究发展计划项目(2017YFB1003103); 国家自然科学基金资助项目(61502197，61503044，61763003); 吉林省科技发展计划项目(20180101053JC).

Two Novel Algorithms Based on Extension Rule for Solving #SAT Problem

LYU Shuai， ZHANG Tong-bo， WANG Qiang， LIU Lei

College of Computer Science and Technology， Jilin University， Changchun 130012， China.

Received:2018-03-26 Revised:2018-03-26 Online:2019-05-15 Published:2019-05-17
Contact: LIU Lei
About author:-
Supported by:
-

摘要/Abstract

摘要： 提出一种新的基于扩展规则的#SAT求解算法NCER，该算法在#ER的基础上加入启发式策略.该策略每次选择当前子句集的最长子句来减小极大项空间，使得递归调用的次数减少，从而加快求解效率.为解决基于扩展规则的#SAT求解器在互补因子较小的样例上的不良表现，结合NCER和CDP的优点提出混合#SAT求解算法NCDPER.实验结果表明:NCER较先前的#ER在所有85个随机SAT测试用例上有了显著的提高.通过与目前最好的基于扩展规则的#SAT求解器的比较，该求解器具有更好的性能.

关键词: 自动推理, 扩展规则, 模型计数, 极大项空间, 启发式策略

Abstract: A novel #SAT solver NCER based on extension rule is proposed， which adds heuristic strategy on #ER algorithm. The heuristic strategy chooses the longest clause in current set of clauses every calling procedure to reduce the maxterm space， and it helps decrease the frequency of recursive invocation to enhance the efficiency of solving. Besides， a mixed model counting algorithm called NCDPER is proposed by combining NCER algorithm and CDP algorithm， to overcome the poor performance on instances where complementary factor of the #SAT solvers is small using the extension rule. NCDPER integrates advantages of NCER algorithm and CDP algorithm. According to the experimental results， NCER has a significant improvement over previous #SAT solvers on all 85 random SAT instances. The #SAT solvers proposed are compared with state-of-the-art #SAT solvers using extension rule， and the results show that the proposed #SAT solvers have better performances.

Key words: automated reasoning, extension rule, model counting, maxterm space, heuristic strategy

中图分类号:

TP181

吕帅，张桐搏，王强，刘磊. 两种新的基于扩展规则#SAT问题求解算法[J]. 东北大学学报:自然科学版, 2019, 40(5): 630-635.

LYU Shuai， ZHANG Tong-bo， WANG Qiang， LIU Lei. Two Novel Algorithms Based on Extension Rule for Solving #SAT Problem[J]. Journal of Northeastern University Natural Science, 2019, 40(5): 630-635.

参考文献

[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.
[12]Lin H，Sun J G.Knowledge compilation using extension rule［J］.Journal of Automated Reasoning，2004，32(2):93-102.
[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.

两种新的基于扩展规则#SAT问题求解算法

Two Novel Algorithms Based on Extension Rule for Solving #SAT Problem

RichHTML

PDF (PC)

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 3

编辑推荐

Metrics

本文评价

[1]	韩淑婷，赖永，刘杰. 混合exactly-one约束的模型计数研究[J]. 东北大学学报（自然科学版）, 2022, 43(4): 463-469.
[2]	李占山，刘兆赓，俞寅，鄢文浩. 量子化信息素蚁群优化特征选择算法[J]. 东北大学学报:自然科学版, 2020, 41(1): 17-22.
[3]	郭莹，张长胜，张斌. 一种求解SAT问题的人工蜂群算法[J]. 东北大学学报:自然科学版, 2014, 35(1): 29-32.