计算机科学 ›› 2021, Vol. 48 ›› Issue (11): 294-299.doi: 10.11896/jsjkx.201000142

• 人工智能 • 上一篇    下一篇

基于学习子句删除策略的SAT求解器分支策略

王钇杰, 徐扬, 吴贯锋   

  1. 西南交通大学数学学院 成都610031
    系统可信性自动验证国家地方联合工程实验室 成都610031
  • 收稿日期:2020-10-26 修回日期:2021-01-23 出版日期:2021-11-15 发布日期:2021-11-10
  • 通讯作者: 吴贯锋(wgf1024@swjtu.edu.cn)
  • 作者简介:806657831@qq.com
  • 基金资助:
    国家自然科学基金(61673320);中央高校基本科研业务费专项资金(2682020CX59)

Branching Heuristic Strategy Based on Learnt Clauses Deletion Strategy for SAT Solver

WANG Yi-jie, XU Yang, WU Guan-feng   

  1. School of Mathematics,Southwest Jiaotong University,Chengdu 610031,China
    National-Local Joint Engineering Laboratory of System Credibility Automatic Verification,Chengdu 610031,China
  • Received:2020-10-26 Revised:2021-01-23 Online:2021-11-15 Published:2021-11-10
  • About author:WANG Yi-jie,born in 1997,postgra-duate.His main research interests include processing and automated reaso-ning.
    WU Guan-feng,born in 1986,Ph.D,is a member of China Computer Federation.His main research interests include intelligent information processing and parallel computing.
  • Supported by:
    National Natural Science Foundation of China(61673320) and Fundamental Research Funds for the Central Universities(2682020CX59).

摘要: 对于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%。

关键词: 活跃度, 可满足性问题, 完备算法, 学习子句, 学习子句删除策略

Abstract: For the SAT solver,most popular branch variable decision-making strategies are based on the variable activity evaluation of conflict.The unassigned variable with the maximum activity is selected as the decision variable,and the most recent conflict is solved first.However,they all ignore the impact of the number of clauses containing decision variables on the Boolean constraint propagation (BCP).To solve this problem,this paper proposes a branch variable decision strategy (VDALCD) based on the learning clause deletion strategy,which reduces the activity of variables in the deleted clause when the clause is deleting.Based on the VDALCD strategy,Glucose4.1 and MapleLCMDistChronoBT-DL-v2.1 are improved to solvers Glucose4.1_VDALCD and Maple-DL_VDALCD.This paper uses 2018 and 2019 SAT international competition questions as benchmark test cases to compare the improved version with the original version of the solver.The experimental results show that Gluose4.1_VDALCD finds out 26 more examples than Gluose4.1,an increase of 15.5% in the 2018 example test.In the 2019 example test,Maple-DL_VDALCD finds out 17 more examples than MapleLCMDistChronoBT-DL-v2.1,an increase of 7.6%.

Key words: Activity, Complete algorithms, Learnt clause, Learnt clause deletion strategy, Satisfiability problem

中图分类号: 

  • TP181
[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.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!