线性公式可满足性判定问题的复杂性

摘要

可满足性问题(SAT)是计算机科学的中心问题之一，也是第一个被证明的NP-完全问题，并且是一大类NP-完全问题的核心。SAT问题是指可满足布尔表达式的集合，它在数理逻辑、人工智能、约束可满足性问题、VLSI集成电路设计与检测、计算机科学理论、计算机视觉、机器定理证明、机器人规划、机器学习等领域具有广阔的应用背景。一个CNF公式F称为线性的，如果F中任意两个不同的子句中至多包含一个相同的变元。一个CNF公式F称为严格线性的，如果F中任两个不同的子句恰好包含一个相同的变元。所有严格线性公式是可满足的([33]S.Porschenetc.,2006)。对于线性公式类LCNF，判定问题LSAT是NP-完全的。对于LCNF的子类LCNF≥k(其公式中每个子句的长度至少为k)，如果在LCNF≥k公式中存在一个不可满足公式，则判定问题LSAT≥k是NP-完全的([31，32]S.Porschen，E.Speckenmeyer,2006)。因此，对于LCNF≥k(k≥3)公式，判定问题LSAT≥k的NP-完全性取决于在LCNF≥k公式中是否存在不可满足公式。在([31，32]S.Porschen.E.Speckenmeyer,2006)中，通过构造超图和拉丁方阵，已经证明了LCNF≥3和LCNF≥4都包含不可满足公式，并提出了一个公开问题：当k≥5时，在LCNF≥k公式中是否存在不可满足公式。 本文基于线性公式的结构与特点，提出了线性化算法，使用该算法可以在|F|多项式时间内把任一公式F转化为线性公式Flin，且两者有相同的可满足性。另外，本文通过研究极小不可满足公式在公式归约中的应用，给出了在k-LCNF(其公式中每个子句的长度都为k，k≥3)公式中构造不可满足公式的一般方法。证明了：对每个k≥3，k-LCNF公式中存在极小不可满足公式，并且证明了下面更强的结果：对每个k≥3，k-LSAT是NP-完全的。

目录

文摘

英文文摘

声明

第一章前言

1.1研究背景

1.2研究意义

1.3研究的主要内容

1.4本文的结构安排

第二章预备知识

2.1命题逻辑公式

2.2 DPLL算法

2.3消解

2.4 MU公式

第三章线性公式

3.1基本概念

3.2线性化算法

3.3线性公式的判定复杂性

第四章线性公式可满足性问题的判定

4.1基本概念

4.2MU公式的应用

4.2.1基本应用

4.2.2三种类型的MU公式

4.3不可满足公式的存在性

4.4线性公式可满足性问题的判定复杂性

4.5结论

致谢

主要参考文献

附录