对可满足性(SAT)问题求全解的算法研究及实现

摘要

可满足性问题（satisfiability problem，简称SAT问题）作为第一个被证明的NP完全问题，有着重要的理论及应用意义。它是计算机理论与应用的核心问题，在计算机科学、人工智能等学科中有重要的理论及应用价值。而对可满足性问题求全解，在电子设计自动化（Electronic Design Automation，简称EDA）领域有着重要的应用价值。 本文介绍了对可满足性问题求全解的理论及实践意义。对可满足性求解器算法进行比较，从中选择了效率较高且适用于全解求解器的算法。分别从增量式和隔离子句的角度，提出了两点适用于全解求解器的新算法： （1）从增量式角度对文字权值进行调整，并提出对隔离子句的冲突分析及回溯处理。本算法结合了布尔可满足性程序中的变量状态独立衰减总和的启发式决策算法，对于全解求解器运行过程中加入的隔离子句所涉及的文字权值进行调整，从而提高全解求解效率。对隔离子句造成的冲突提出专门的冲突分析及回溯处理机制，使每次添加一个隔离子句后，程序可以迅速进入下一次求解过程。 （2）从隔离子句的角度对全解求解器进行改进。提出了基于CNF的类Don‘t cares算法。这一算法借鉴了基于混合表示法（hybrid representations，即将电路特征和合取范式相结合）的Don't cares算法，提出了单纯基于合取范式输入法的类Don，t cares算法。使基于CNF输入的全解求解器效率得到了一定程度的提高。提出对隔离子句的归并处理策略。能够对当前得到的隔离子句进行一定程度的归并处理，又不需要消耗太多的运行时间和系统空间资源。 从实验结果可以看出以上两种算法对全解求解器效率的提高。

目录

文摘

英文文摘

声明

致谢

1 综述

1.1 课题研究意义

1.1.1 理论意义

1.1.2 应用意义

1.2 对可满足性问题求全解

1.3 国内外研究现状

1.4 论文主要工作及内容安排

1.4.1 主要工作

1.4.2 内容安排

2可满足性求解器的实现

2.1 DPLL算法框架

2.1.1 原始DPLL算法

2.1.2 改进的DPLL算法

2.2 启发式算法

2.2.1 传统启发式算法

2.2.2 变量状态独立衰减总和的启发式决策算法

2.3 布尔约束传播算法

2.3.1 一些布尔约束传播算法

2.3.2 文字监视算法

2.4 冲突学习算法

2.4.1 蕴含关系图

2.4.2 冲突分析和学习机制

2.4.3 各种分割学习算法及其比较

2.5 实验结果

3 从增量式角度提高全解求解效率

3.1 对可满足性求解器的算法改变

3.1.1 隔离子句

3.1.2 内存问题

3.2 全解求解器的基本算法实现

3.2.1 可满足性求解器算法

3.2.2 全解求解器的基本算法

3.3 增量式求解

3.3.1 基本概念

3.3.2 文字权值调整

3.3.3 冲突分析及回溯处理

3.4 实验结果及分析

4 对隔离子句的算法改进

4.1 类Don't cares算法

4.1.1 Don't cares算法思想

4.1.2 基于CNF的类Don't cares算法

4.2 对隔离子句的归并

4.3 低内存条件下的算法

4.4 实验结果及分析

5 总结与展望

5.1 全文工作总结

5.2 研究展望

参考文献

作者简历