Print

基于子句权重求解SAT问题

论文摘要

可满足性(SAT)问题一直是电子设计自动化和人工智能领域的一个热点研究问题,因为它在这些领域有着非常广泛的应用。长期以来,人们对此进行了深入地研究,提出了很多解决可满足性问题的算法,其中最为流行的要数DPLL算法。基于DPLL算法,有很多的解决器被开发出来,ZCHAFF就是其中最著名的解决器之一。在这篇文章中,我们介绍了可满足性问题的应用及其经典算法,并着重研究了DPLL算法的决策过程。本文在决策过程中考虑了给定的CNF描述中子句长短不同的问题,采用子句加权改善决策策略。实验表明,对于那些CNF子句长短不一的SAT问题,子句加权后的决策策略能有效提高解决器的性能。在一些例子上,采用子句加权后的解决器,运行时间比ZCHAFF要快几十到几百倍,甚至能解决一些ZCHAFF当前无法解决的问题。

论文目录

  • 摘要
  • Abstract
  • 引言
  • 第一章 可满足性问题基础知识
  • 1.1 合取范式（CNF）和析取范式（DNF）
  • 1.2 什么是可满足性问题（SAT）
  • 1.3 小结
  • 第二章 可满足性问题的应用
  • 2.1 SAT问题的广泛应用
  • 2.2 SAT问题在形式验证领域的应用
  • 2.3 逻辑电路转化为CNF
  • 2.4 小结
  • 第三章 可满足问题的算法及其解决器
  • 3.1 SAT问题的定义
  • 3.2 SAT问题算法概述
  • 3.3 BDD算法
  • 3.4 DPLL算法
  • 3.5 ZCHAFF解决器
  • 3.6 小结
  • 第四章 基于子句权重求解可满足性问题
  • 4.1 传统决策方法介绍
  • 4.2 基于子句权重的决策策略
  • 4.3 基于子句权重求解SAT问题
  • 4.3.1 算法流图
  • 4.3.2 基本数据结构
  • 4.3.3 算法小结
  • 4.4 实验结果
  • 4.4.1 实验数据
  • 4.4.2 实验结果小结
  • 4.5 小结
  • 第五章 总结与展望
  • 5.1 工作总结
  • 5.2 未来工作展望
  • 参考文献
  • 致谢

    • 相关论文文献

    本文来源: https://www.lw50.cn/article/28f5d90876469a3615e29921.html