基于矛盾体分离的命题逻辑动态自动演绎推理求解系统研究

发布时间：2021-09-04 04:18

　　SAT问题是一类特殊的约束满足问题（CSP）,也是信息科学领域一个著名的决策问题。在理论应用领域,许多经典的可计算问题,诸如覆盖问题、打包问题、路由选择问题、排序问题等都可以转换为SAT问题求解;在实际应用领域,诸如模型检验、软件形式化验证、硬件形式化验证、智能规划、知识编译以及其他组合优化领域的问题也可以转换为SAT问题求解。因此,研究高效的SAT求解算法有着重要的理论价值和应用价值。由于SAT问题是NP完全的,迄今为止没有发现哪一个SAT求解器长期处于领先地位。针对主流的CDCL SAT求解算法的不足,本文基于徐扬教授提出的基于矛盾体分离的演绎自动推理理论,在构建动态、多元的矛盾体分离的演绎算法核心方面进行了深入的研究,并开发了独立的基于矛盾体分离的命题逻辑动态自动演绎推理求解器和基于矛盾体分离的命题逻辑动态自动演绎推理核心与CDCL融合的求解器。实现了基于矛盾体分离的命题逻辑动态自动演绎推理求解基础算法,并针对CDCL求解算法规避潜在搜索冲突的机制进行了研究,提出了基于矛盾体重构的子句学习算法。利用CDCL求解器冲突分析给出的回溯层与当前冲突层之间的决策信息,在子句集中选择合适子... 

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

【文章页数】：139 页

【学位级别】：博士

【部分图文】：

8bits_10.dimacs运行中决策层及冲突次数变化情况

【参考文献】：
期刊论文
[1]求解SAT问题的量子免疫克隆算法[J]. 李阳阳,焦李成.  计算机学报. 2007(02)



本文编号：3382544