SAT问题的子句消去法及数学原理

姜咏江

对外经济贸易大学（UIBE）

摘要  本文我们介绍如何利用限位数理论，通过子句消去法算法（CEASP），在O(n^k+1)多项式算法时间复杂度来求解SAT问题满足解。SAT问题可以用二进制数码以表的形式表达出来。我们借助于限位数理论文中定义变量唯一解和它的可选解概念，基于它们我们可以求出SAT问题的满足解。本文提出了一些新的概念，给出了一些重要的定理并给出了证明。CEASP是求解SAT问题完备性算法。我已经设计了3-SAT计算机程序（CEASP）而且经过测试没有错误。

关键词  CEASP 限位数 i-子句块 变量可选解 算法时间复杂度 多项式

CCS Concepts: • Theory of computation → Computational complexity and cryptography; Circuit complexity; Prove complexity

1. 背景

P与NP问题是计算机科学中尚未解决的巨大问题。攻破P=NP问题，NP完全问题的概念十分重要。NP完全问题是一个问题的集合，它们之间可以在多项式时间相互归约。任何一个NP问题都可以转成NP完全问题，形式上，NP完全问题是一个NP问题，它至少象其它NP问题一样具有代表性。依据库克.史提芬定理，任何一个NP问题都可以在多项式时间内，机械地转化成布尔可满足性问题（SAT）。布尔可满足性问题是一个NP完全问题。如果布尔可满足性问题有多项式时间算法，则它是P问题，必然导致有P=NP的结论。

命题逻辑公式又叫布尔逻辑表达式，它由逻辑变量、与运算符（/）、或运算符（/）、非运算符（'）和括号组成。如果能够找到一组变量值（真或假），使得一个逻辑公式的运算结果为“真”，那么称这个逻辑公式为可满足的。SAT问题是给出一个逻辑公式（合取范式）来确定其是否可满足的问题。这个判定问题在不同的计算机科学领域都非常重要，其中包括计算机科学理论、计算复杂度理论、算法、密码学和人工智能等方面。

(由于版面显示的原因，余下部分阅读请下载附件。英文稿请阅读 http://blog.sciencenet.cn/blog-340399-1070668.html  ）

SAT问题的子句消去法及数学原理.pdf

Mathematical Theory of Clause Elimination Algorithm for SAT_acm00.pdf