SAT问题 | gxblog

前言

所有的问题都可以被转化为数学问题模型，SAT问题就是其中的一个模型

SAT的问题被证明是NP-Hard的问题，目前解决该问题的方法主要有完备的方法和不完备的方法两大类

完备的方法优点是保证能正确地判断SAT问题的可满足性，但其计算效率很低，平均的计算时间为多项式阶，最差的情况计算时间为指数阶，不适用于求解大规模的SAT问题

不完备的方法的优点是求解的时间比完备的方法快得多，但在很少数的情况下不能正确地判断SAT问题的可满足性

传统的方法有：枚举法、局部搜索法和贪婪算法等，但由于搜索空间大，问题一般难以求解

对于像SAT一类的NP-Hard问题，采用一些现代启发式方法如演化算法往往较为有效

SAT(satisfiability)问题是：

在计算机科学的许多领域都重要：

SAT问题被称为命题可满足性问题，因为它的

是命题逻辑公式(formula)：(p1∨﹁p2)∧(﹁p1∨﹁p2∨p3)∧(﹁p3)

(p1∨﹁p2)∧(﹁p1∨﹁p2∨p3)∧(﹁p3)
变量：p1,p2,… → 文字(literal)

(p1∨﹁p2)∧(﹁p1∨﹁p2∨p3)∧(﹁p3)
运算符：﹁

(p1∨﹁p2)∧(﹁p1∨﹁p2∨p3)∧(﹁p3)
运算符：∨：or → 作用于变量之间 → (﹁p1∨﹁p2∨p3) → 子句(clause)

(p1∨﹁p2)∧(﹁p1∨﹁p2∨p3)∧(﹁p3)
运算符：∧：and → 作用于子句之间 → 子句∧子句 → 公式(formula)

空公式：空集对应的公式
C：the resolvent(预解式) of C1 and C2：C = ( C1 - { p } ) U ( C2 - { pc } )

若存在 p 属于 C1 , p 逆属于 C2 ,则存在子句 C 为子句 C1 与 C2 的 resolvent。C1、C2 称为 C 的 parent clauses

总结：literal → clause → formula. 可以写成两种形式：

若为命题逻辑公式中的每个变量赋一个逻辑值（真/假），
逻辑值也会相应地扩展到子句，
并继续扩展到命题逻辑公式。
以上给变量赋值的过程称为 Interpretation
An interpretation is a function

函数 ⨚：
- literal：⨚ ( p ) = T，⨚ ( p ) = F
- clause：
  - ⨚ ( C ) = T：at least one p ∈ C，⨚ ( p ) = T
  - ⨚ ( C ) = F：for all p ∈ C，⨚ ( p ) = F
- formula：
  - ⨚ ( A ) = T：for all C ∈ A，⨚ ( C ) = T
  - ⨚ ( A ) = F：at least one C ∈ A，⨚ ( C ) = T
如果存在一个 interpretation 使命题逻辑公式为真（ ⨚ ( A ) = T ），那么公式 A 是可满足的；反之是不可满足的。
如果一个 interpretation 只需给公式中的部分变量赋逻辑值，就可以得出公式的逻辑值，则这个 interpretation 称为 partial interpretation
单位子句定则：
- 单位子句 C = { p } 属于公式 A；存在 partial interpretation ⨚ 没有对文字 p 赋值，可以通过在 ⨚ 中添加 p 赋值构建一个 interpretation ⨚'，⨚’ ( p ) = T。
- 通过将 A 中的单位子句删除，并将剩余子句中的 p 逆删除构建公式 A'
- 定理： 由单位子句定则得到的 A'，如果 A' 是可满足的，那么 A 就是可满足的
分解 ( Resolution ) 定则：

C1、C2 是两个子句，且有 p ∈ C1，p 逆 ∈ C2，C1、C2的 resolvent 是子句 C = ( C1 - { p } ) U ( C2 - { p 逆 } )。C1、C2 是 C 的 parent clauses.
定理：只有 C 的 parent clauses C1、C2 都可满足时，C 才可满足
定理：空子句是不可满足的
定理：空公式是可满足的