基于CDCL求解器的分支策略和删除策略的研究

发布时间：2022-02-09 11:31

　　SAT问题是计算机科学理论和人工智能中的著名问题。NP完全问题（NP-complete,NPC）排在千禧年七大难数学问题之首,许多NP完全问题都可以在多项式时间内转换为SAT问题进行求解。SAT问题广泛应用于数学定理证明、计算机软件与理论、工程技术、软件验证以及逻辑电路等价性验证等多个领域。因而SAT问题一直是国内外学者关注的热点问题,设计并实现求解SAT问题的高效算法具有重要的钻研意义和应用远景。DPLL求解器开创了求解SAT问题的先河,但其算法自身的回溯机制对大规模问题的求解有一定程度的制约性。为了提升DPLL算法的求解效率,国内外学者们进行了大量的研究,添加了一些关键技术。例如启发式分支策略、基于冲突分析和子句学习、非时序回溯、学习子句的删除和周期性重启等,形成了当前最流行的CDCL（Conflict-Driven-Clause-Learning,CDCL）求解器。基于CDCL算法结构,本文做了以下研究工作:一、借鉴VSIDS策略及其延伸策略的思想,研究变量的决策层和变量参与冲突的冲突次数对分支决策阶段的影响,在此基础上提出一种改进的启发式分支策略——基于变量决策层的启发式变量选... 

【文章来源】：西南交通大学四川省211工程院校教育部直属院校

【文章页数】：59 页

【学位级别】：硕士

【部分图文】：

不同删除比例的求解性能对比

图 5-1 不同求解器对 2017 年测试例的求解性能对比.2.2 2018 年 SAT 竞赛结果表 5-3 列出了四个求解器对 2018 年 SAT 国际竞赛问题中 Main Track 组中 400 个

不同求解器对2018年测试例的求解性能对比

【参考文献】：
期刊论文
[1]基于演绎长度的学习子句删除策略[J]. 常文静,徐扬,吴贯锋.  计算机工程与应用. 2018(16)
[2]一种求解SAT问题的人工蜂群算法[J]. 郭莹,张长胜,张斌.  东北大学学报(自然科学版). 2014(01)
[3]着色归结、PI着色碰撞及其完备性[J]. 陆汝占,林凯,孙永强.  计算机学报. 1987(12)

博士论文
[1]基于矛盾体分离的命题逻辑动态自动演绎推理求解系统研究[D]. 陈青山.西南交通大学 2018

硕士论文
[1]基于CDCL结构的SAT问题优化策略的研究[D]. 杜忠和.西南交通大学 2018
[2]布尔可满足关键问题研究[D]. 王艺源.吉林大学 2014
[3]基于DPLL的SAT算法的研究及应用[D]. 陈稳.电子科技大学 2011



本文编号：3616929