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

SAT 问题的子句消去法及数学原理 姜咏江 对外经济贸易大学 （UIBE） k+1 摘要 本文我们介绍如何利用限位数理论，通过子句消去法算法 （CEASP），在O(n )多项式 算法时间复杂度来求解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 问题是给出一个逻辑公式 （合取范式） 来确定其是否可满足的问题。这个判定问题在不同的计算机科学领域都非常重要，其中包括 计算机科学理论、计算复杂度理论、算法、密码学和人工智能等方面。 2. SAT 问题的定义 对于布尔看满足性问题给出严格的数学定义。 定义1. 将逻辑变量x 的非，用 x 表示，集合A ｛x ,x ,...,x ｝,A’ ｛x ’,x ’,...,x ’｝, 合 1 2 n 1 2 n m vi vi vi ∧(∨x )  (∨x ) (∨x ) 取范式SAT-CNF , 文字 x ∈A∪A’ 和 x x ’ ， 是子句,v ij ij  ij i ij ij ij i 1 j 1 j 1 j 1 是 i 号子句的文字数, 变量个数用表示n，n 是最少的变量个数，k 是子句中文字最多的个 0 数，满足v k n ,m 是合取范式子句的数量。如果有一个 n 元二进制向量为这些逻辑变 i ≤ 0 量的值，能够使得 SAT-CNF 1, 那么这个二进制向量就叫SAT 的满足解。 本文中 i 1,2,3,...,k. 定义 2. 在 合取范