基于子句权重求解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 未来工作展望
• 参考文献
• 致谢