计算机科学 ›› 2021, Vol. 48 ›› Issue (11): 294-299.doi: 10.11896/jsjkx.201000142
王钇杰, 徐扬, 吴贯锋
WANG Yi-jie, XU Yang, WU Guan-feng
摘要: 对于SAT求解器,目前流行的分支变量决策策略大多是基于冲突的变量活跃度评估算法,选择具有最大活性的未赋值变量作为决策变量,优先解决最近的冲突。但是,它们都忽略了包含决策变量的子句数目对布尔约束传播(BCP)的影响。针对此问题,提出了一种基于学习子句删除策略的分支变量决策策略(VDALCD),在删除学习子句的同时减小被删除子句中变量的活跃度。基于VDALCD策略分别对Glucose4.1,MapleLCMDistChronoBT-DL-v2.1进行改进,形成了求解器Glucose4.1_VDALCD和Maple-DL_VDALCD。以2018年、2019年SAT国际竞赛题为基准测试例,将改进版本与原版本求解器进行比较。实验结果表明,在2018年的例子测试中,Gluose4.1_VDALCD比Gluose4.1多求出26个例子,增加了15.5%。在2019年的例子测试中,Maple-DL_VDALCD比MapleLCMDistChronoBT-DL-v2.1多求出17个例子,增加了7.6%。
中图分类号:
[1]COOK S A.The complexity of Theorem-Proving Procedures[C]//Proceedings of the 3rd Annual ACM Symposium on Theo-ry of Computing.New York:ACM,1971:151-158. [2]KARP R M.Reducibility Among Combinatorial Problems[M]//Complexity of Computer Conputation.Berlin:Spring US,1972:85-103. [3]HOOS H H,STYUTZLE T.Stochastic Local Search:Foundations & Applications [M]//Access Online Via Elsecier.2004. [4]ROBINSON J A.A Machine-Oriented Logic Based on the Resolution Principle[J].Journal of the ACM (JACM),1965,12(1):23-41. [5]DAVIS M,PUTNAM H.A Computing Procedure for Quantification Theory[J].Journal of the ACM(JACM),1960,7(3):201-215. [6]DAVIS M,LOGEMANN G,LOVELAND D.A machine Pro-gram for Theorem Proving[J].Communication of the ACM,1962,5(7):394-397. [7]MARQUES-SILVA J,LYNCE I,MALIK S.Conflict-DrivenClause Learning SAT Solves [M].Amsterdam:IOS Press,2009:127-149. [8]MARQUES-SILVA J,SAKALLAH K.GRASP:A New Search Algorithm for Satisfiability [M]//The Best of ICCAD.New York:Springer,2003:73-89. [9]LUO M,LI C M,XIAO F,et al.An Effective Learnt Clause Mi-nimization Approach for CDCL SAT Solvers[C]//Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence.2017:703-711. [10]SIMON L,AUDEMARD G.Predicting Learnt Clauses in Mo-dern SAT Solver[C]//Proceedings of the Twenty-First International Joint Conference on Artificial Intelligence (IJCAI'09).Menlo Park:AAAI Press,2009:399-404. [11]BIEKE A.Lingeling and Friends Entering the SAT Challenge 2012[C]//Proceedings of SAT Challenge.2012:33-34. [12]GLOUER F,KELLY J P,LAGUNA M.Genetic Algorithmsand Tabu Search:Hybrids for Optimization[J].Computer & Operations Research,1995,22(1):111-134. [13]BURO M,BÜNING H K.Report on a SAT Competition [M]//Fachbereich Math-Informatik.Univ.Gesamthochschule.West Germany,1992. [14]FREEMAN J W.Improvements to Propositional SatisfiabilitySearch Algorithms [D].Philadelphia:University of Pennsylvania,1995. [15]WEIDENBACH C,DIMOVA D,FIETZKE A,et al.SPASSVersion 3.5[C]//CADE.2009:140-145. [16]BIERE A,FROHLICH A.Evaluating CDCL Variable Scoring Schemes[C]//Theory and Applications of Satisfiability Testing-SAT 2015.Switzerland:Springer USA,2015:405-422. [17]RVAN L.Efficient Algorithms for Clause-Learning SAT Sol-vers [D].Vancouver:Simon Fraser University,2004. [18]CHANG W J.Study of Satisfiability Solving Systems and Application Based on Contradiction Separation Based Multiple Dynamic Automated Deduction[D].Chengdu:Southwest Jiaotong University,2019. [19]WANG G J.Introduction to Mathematical Logic and Resolution Principle[M].Beijing:Science Press,2003. [20]CHEN Q S,XU Y,HE X X.Heuristic Complete Algorithm for SAT Problem by Using Logical Deduction[J].Journal of Southwest Jiaotong University,2017,52(6):1224-1232. [21]AUDEMAND G,SIMON L.Predicting Learnt Clauses Quality in Modern SAT Solvers[C]//Proceeding of the 21st International Joint Conference on Artificial.Intelligence.San Francisco,CA:Margan Kaufmann,2009:399-404. |
[1] | 沈雪, 陈树伟, 艾森阳. 基于奖励机制的SAT求解器分支策略 Reward Mechanism Based Branching Strategy for SAT Solver 计算机科学, 2020, 47(7): 42-46. https://doi.org/10.11896/jsjkx.190700191 |
[2] | 刘江, 周鸿昊. 一种布尔公式的代数逻辑约化新方法 New Algebraic Logic Reduction Method for Boolean Formula 计算机科学, 2020, 47(5): 32-37. https://doi.org/10.11896/jsjkx.190400018 |
[3] | 毛义坪, 余磊, 官泽瑾. 基于分数阶微分的多聚焦图像融合 Multi-focus Image Fusion Based on Fractional Differential 计算机科学, 2019, 46(11A): 315-319. |
[4] | 陈青山, 徐扬, 吴贯锋. 基于趋势强度的SAT问题学习子句评估算法 Learnt Clause Evaluation Algorithm of SAT Problem Based on Trend Strength 计算机科学, 2018, 45(12): 137-141. https://doi.org/10.11896/j.issn.1002-137X.2018.12.021 |
[5] | 郭莹,张长胜,张斌. 求解SAT问题的算法的研究进展 Research Advance of SAT Solving Algorithm 计算机科学, 2016, 43(3): 8-17. https://doi.org/10.11896/j.issn.1002-137X.2016.03.002 |
[6] | 王锦坤,姜元春,孙见山,孙春华. 考虑用户活跃度和项目流行度的基于项目最近邻的协同过滤算法 Item-based Collaborative Filtering Algorithm Integrating User Activity and Item Popularity 计算机科学, 2016, 43(12): 158-162. https://doi.org/10.11896/j.issn.1002-137X.2016.12.028 |
[7] | 田铭,邬江兴,兰巨龙. 信息中心网络中基于局部内容活跃度的自适应缓存算法 Adaptive Cache Algorithm Based on Local Content Activity in Information-centric Networks 计算机科学, 2016, 43(11): 164-171. https://doi.org/10.11896/j.issn.1002-137X.2016.11.032 |
[8] | 何旵阳,孙鲁敬,杨家海. 基于Feeds的社交网络活跃度分析 OSN Activities Analysis Based on User Feeds 计算机科学, 2015, 42(11): 149-153. https://doi.org/10.11896/j.issn.1002-137X.2015.11.031 |
[9] | 王晓峰,李强,丁红胜. 规则实例集上警示传播算法的收敛性 Convergence of Warning Propagation Algorithm for Regular Structure Instances 计算机科学, 2015, 42(1): 279-284. https://doi.org/10.11896/j.issn.1002-137X.2015.01.062 |
[10] | 何琨,姚鹏程,李立文. 求解二维矩形Packing问题的完备算法 Complete Algorithm for 2D Rectangular Packing Problem 计算机科学, 2014, 41(8): 55-59. https://doi.org/10.11896/j.issn.1002-137X.2014.08.011 |
[11] | 李屾,常亮,孟瑜,李凤英. 分支时态描述逻辑ALC-CTL及其可满足性判定 Branching Temporal Description Logic ALC-CTL and its Satisfiability Decision 计算机科学, 2014, 41(3): 205-211. |
[12] | 周军海,林亚平,周四望. 一种低功耗的社区机会网络消息路由算法 Power-efficient Message Routing Algorithm for Community-based Opportunistic Network 计算机科学, 2014, 41(1): 178-182. |
[13] | 李金屏,黄艺美. 基于相似关系的社会集合论 Social Set Theory Based on Similarity Relations 计算机科学, 2013, 40(5): 54-57. |
[14] | 常亮,王娟,古天龙,董荣胜. 时态描述逻辑ALC-LTL的Tableau判定算法 Tableau Decision Algorithm for the Temporal Description Logic ALC-LTL 计算机科学, 2011, 38(8): 150-154. |
[15] | 张晓星,刘冀伟,胡广大,崔朝辉. 分布式视频编码中的边信息改进算法 Improved Side Information Generation Algorithm in Distributed Video Coding 计算机科学, 2011, 38(11): 275-277. |
|