论文部分内容阅读
命题公式的满足性问题(简称SAT问题)是指布尔表达式的可满足性问题.它是理论计算机科学中的一个重要问题.在数理逻辑、人工智能、约束满足问题、VLSI集成电路设计与检测以及计算机科学理论等领域具有广阔的应用背景。SAT问题是第一个NP-完全问题，并且是一大类NP-完全问题的核心。
一个CNF公式(conjunctivenormalform)是有限个子句的合取，(r.s)-CNF公式是指每个子句恰恰含有r个不同的文字，且每个变量出现的次数最多出现s次的CNF公式类，(r.s)-SAT是限定在(r.s)-CNF上的命题满足性实例。一个SAT算法能在有限时间内判定任意给定的CNF公式是否可满足，DPLL算法和消解反驳法是判定SAT问题的两个重要方法。OlgaTveretina和HansZantema已经详细分析了DPLL算法到消解的转换，并证明了，如果有一个长度为s的DPLL反驳，结点数为r，且每个结点标记的单位消解序列是完备的，则存在一个长度为s-r的消解反驳，显然这个长度已经优于s。我们已经知道，对于任意一个MU(1)公式对应一个(1，1)-消解。极小不可满足公式的研究是近年来兴起的问题的一个热点方向。德国学者H.KleineBüning，O.kullmann等人在这方面做了许多重要的工作。极小不可满足公式的一些结构和性质将有助于判定SAT算法的研究。
本文通过研究极小不可满足公式的树消解证明及极小不可满足公式的分裂，构建了(r，s)-SAT中的一些极小不可满足实例。并在此基础上，表示了(r，s)-SAT中的一些NP-完全实例。
进一步，在极小不可满足公式的构建方法及分裂定理的基础上，将消解转换到了(1，1)-消解，由此，得到了DPLL到(1，1)-消解的转换，从而建立了一套完备的消解证明系统。