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.