以字符个数为参数的可满足性问题算法研究

摘要

在可计算性理论和复杂性理论中，可满足性问题是一个重要的NP-完全问题。可满足性问题已经广泛地应用于自动推演，计算机辅助设计，计算机辅助操作，机器视觉，数据库等等。通常来说，可满足性问题是指离散的有约束的一类判定性问题，其形式化定义为:给定一个布尔合取范式F，是否存在一个F的赋值，使得F为真。可满足性问题算法的时间复杂度计算过程主要涉及3类参数:范式中变量的个数n，范式中子句的个数m，范式中字符的个数L。
　　本文从字符个数L的角度，研究了一般性可满足性问题的精确算法。在以同样参数来解决该问题的精确算法中，目前最好的算法时间复杂度为O*(1.0652L)，其中L是范式中字符的个数。本文首先研究了可满足性问题的预处理过程。根据消除(resolution)原理和引入的度量——范式F中所有变量的频率权值之和，本文给出了12条化简规则的预处理过程及其证明。对于化简后的范式，所有子句都包含至少两个字符，同时明确了包含两个字符的子句和其他类型子句的关系，并且任意两个不同的字符都不可能同时包含在两个子句中。
　　本文采用分支搜索技术对可满足性问题进行求解。算法在每次分支之前，对范式进行预处理。当预处理后的范式中含有特定的3种子句结构之一时，算法针对这种子句结构进行特殊分支。否则，算法将选出范式中频率最大的变量进行分支。本文的主要贡献除了改进可满足性问题算法时间复杂度外，还引入了一种全新的分析方法，即加权分治(Measure and Conquer)。该方法给范式中每个变量赋予一个权值，该权值在分支过程中会产生额外的减少量，从而使得最终的时间复杂度更紧。通过改进分支算法并在分析中引入加权分治分析技术，本文算法的时间复杂度为O*(1.0651L)。

目录

声明

摘要

1 绪论

1．1 研究背景

1．2 研究内容

1．3 研究意义

1．4 论文组织

2 SAT问题相关概念和技术

2．1 相关概念及术语

2．2 分支搜索技术

2．3 加权分治分析技术

2．4 本章小结

3 基于字符个数SAT问题的预处理过程

3．1 化简规则

3．2 不可化简范式的性质

3．3 本章小结

4 基于字符个数SAT问题的算法及分析

4．1 主算法

4．2 相关定理

4．3 3类特殊分支上基于加权分治的分析

4．4 其他分支上基于加权分治的分析

4．5 本章小结

5 结束语

5．1 研究工作总结

5．2 研究展望

参考文献

攻读硕士学位期间研究成果

致谢