基于CDCL的SAT问题的分支启发式策略研究

发布时间：2023-08-15 19:41

　　命题逻辑公式的可满足性问题(SAT问题)是指给出一个合取范式,判断是否存在一组赋值使得这个合取范式可满足。SAT问题是计算机科学与工程、人工智能、计算机视觉和计算机辅助设计等领域的一个核心问题,它也是第一个被证明的NP完全(Non-Deterministic Polynomial-Complete,NPC)问题。正因为如此,研究SAT问题并提高求解器的效率是很有价值的。求解SAT问题的算法分为完备算法和不完备算法。完备算法的特点是在问题可满足时,给出一个模型;不可满足时,给出证明。基于完备算法的优点,本文以CDCL(Conflict Driven Clause Learning,CDCL)算法为框架,研究CDCL算法的以下主要流程:决策、冲突分析、学习子句和回溯之间的关系。SAT求解器的成功绝大多数归因于从错误赋值中学习的能力、快速地删除搜索空间以及首先集中在那些“重要”变量中^[1]。故本文集中在CDCL算法中的决策和冲突分析上,取得的主要研究结果如下:1.当一个命题逻辑中的逻辑公式以CNF的形式输入到数据库时,从中选择“重要”变量的依据是变量出现的次数和包含该变...

【文章页数】：55 页

【学位级别】：硕士

【文章目录】：
摘要
Abstract
第1章 绪论
    1.1 研究背景和意义
    1.2 SAT问题国内外研究现状
    1.3 本文研究的内容和结构安排
第2章 SAT问题基本理论
    2.1 算法复杂度
    2.2 P问题、NP问题和NPC问题
    2.3 SAT问题基本定义
    2.4 本章小结
第3章 CDCL算法研究进展
    3.1 DPLL算法
    3.2 CDCL算法
        3.2.1 CDCL算法伪代码
        3.2.2 analyze-conflict()和Backtrack()
    3.3 决策启发式策略
    3.4 本章小结
第4章 基于VSIDS改进的分支启发式策略
    4.1 CLVDL分支启发式策略
        4.1.1 变量初始记分
        4.1.2 变量“碰撞”记分
    4.2 CLVDL算法步骤
    4.3 本章小结
第5章 算法分析及实验结果
    5.1 算法分析
    5.2 测试相关说明
    5.3 测试结果比较
        5.3.1 SAT竞赛结果比较
        5.3.2 SATLIB测试结果比较
    5.4 本章小结
第6章 总结与展望
    6.1 总结
    6.2 展望
致谢
参考文献
攻读硕士学位期间发表的论文及参与的科研工作
    1.硕士期间发表的论文
    2.硕士期间参与的科研项目



本文编号：3842149