可满足性问题的相关问题研究

发布时间：2024-06-03 04:33

　　布尔可满足性问题是第一个NP完全问题,是计算机科学领域的重要核心之一,并且广泛应用于多个领域,例如电子设计自动化、模型检测、软件验证、集成电路验证、组合优化以及计算生物学等。本文将侧重研究布尔可满足性问题中的经典问题及其相关的扩展问题,包括经典SAT推理方法的形式化描述;子句学习算法所涉及的相关问题研究;归结方法的逆运算——扩展规则方法的相关问题研究以及推理问题的扩展形式——#SAT相关方面的研究。本文的主要研究贡献总结如下:(1)为了达到利用细胞膜演算形式化描述带子句学习的DPLL算法的整个推理过程的目的,采用细胞膜演算的形式化方法描述带子句学习的DPLL算法。分别定义了部分赋值、变量反转、回溯、回跳最大层、细胞膜溶解等反应规则,给出了DPLL的一般过程和冲突分析过程的描述。最后通过规模大小不同的两个测试用例的求解过程验证了该形式化描述方法的可行性。依赖细胞膜演算可以更直观、简洁地展现推理算法的推理过程,同时展示了膜演算的描述能力和处理能力。(2)子句学习技术在可满足性问题中已得到了广泛的应用。在本文中,我们以优化学习子句数据库为目的,在原MiniSAT求解器的基础上,提出了一种新的...

【文章页数】：111 页

【学位级别】：博士

【文章目录】：
摘要
abstract
第1章 绪论
    1.1 研究背景与意义
    1.2 命题逻辑推理方法的研究现状
        1.2.1 推理方法的研究进展
        1.2.2 推理问题的扩展
        1.2.3 研究趋势和问题分析
        1.2.4 SAT求解器
    1.3 本文主要工作
    1.4 本文结构安排
第2章 基础知识
    2.1 可满足性问题的定义和表示
    2.2 可满足性问题的求解方法
        2.2.1 DPLL与子句学习
        2.2.2 局部搜索
        2.2.3 扩展规则
第3章 利用细胞膜演算描述带子句学习的DPLL算法
    3.1 引言
    3.2 细胞膜演算
        3.2.1 基本概念
        3.2.2 语法
        3.2.3 反应规则
    3.3 描述DPLL的一般过程
        3.3.1 细胞膜演算规则
        3.3.2 细胞膜演算描述DPLL
    3.4 冲突分析
    3.5 实例验证
    3.6 本章小结
第4章 基于重启策略的学习子句优化方法
    4.1 引言
    4.2 学习子句数据库的化简
    4.3 博弈论简介
        4.3.1 博弈模型的引入
        4.3.2 博弈模型
    4.4 SAT方法与博弈论的对应
        4.4.1 博弈模型的分析
        4.4.2 基于博弈论的学习子句优化算法
    4.5 实验结果
    4.6 本章小结
第5章 基于局部搜索的并行扩展推理方法
    5.1 引言
    5.2 ERACC算法
    5.3 并行扩展规则推理方法
        5.3.1 CPVI算法
        5.3.2 PERRM算法
        5.3.3 SIMT算法
    5.4 实验结果与分析
        5.4.1 实验环境与测试用例
        5.4.2 UNIFORM RANDOM-3-SAT问题测试用例实验结果
        5.4.3 图着色问题测试用例实验结果
        5.4.4 AIM类问题测试用例实验结果
    5.5 本章小结
第6章 基于格局检测的并行模型计数方法
    6.1 引言
    6.2 基于格局检测的模型计数方法
        6.2.1 SWCC迭代法
        6.2.2 SWCC优化增量法
    6.3 并行模型计数算法
        6.3.1 SVHD算法
        6.3.2 基于格局检测的并行模型计数算法
    6.4 实验结果与分析
        6.4.1 实验环境与测试用例
        6.4.2 UNIFORM RANDOM-3-SAT问题测试用例实验结果
        6.4.3 CBS类问题测试用例实验结果
        6.4.4 PARITY类问题测试用例实验结果
    6.5 本章小结
第7章 总结与展望
    7.1 总结
    7.2 展望
参考文献
作者简介及在学期间科研成果
致谢



本文编号：3988185