12SAT问题 121SAT问题及其串行算法 1SAT问题描述 所谓可满足性问题( Satisfiability Problem)即SAT问题,其定义为:对于一个命题逻 辑公式,是否存在对其变元的一个真值赋值公式使之成立。这个问题在许多领域都有着非常 重要的意义,而且对其快速求解算法的研究成为计算机科学的核心课题之一。例如在机器定 理证明领域,某命题是否是一个相容的公理集合的推论,这个问题归结为该命题的反命题与 该公理集合一起是否是不可满足的。特别是1971年Cook首次证明了SAT是NP完全的, 从而大量的计算问题都可以归结到SAT。正是由于SAT重要的理论和应用地位,众多学者 对它进行了广泛而深入的研究 由命题逻辑知识可以知道,任何命题逻辑公式都逻辑等价与一个合取范式 Conjunctive Normal form,简写为CNF,因此本文只讨论CNF的SAT求解问题 下面给出几种常见的SAT问题化简策略,以下均假定F是CNF范式:①单元子句规则: 若C=L}是F的子句,则F变为F'=FF1]:②纯文字规则:若文字L出现在F中,而一L 不出现F中,则L称为F的纯文字。F变为F=FF]:③重音子句规则:若C∈F且C是 重言子句,则从F中删去C得F'=FC:④两次出现规则:若L∈C1,=L∈C2,且L和L 都不在其它子句中出现,则将C1,C2合并为C'=(C1-{L})U(C2{L}),F变为F=F- C1,C2}UC}:⑤包含规则:若C1,C2是F的子句,且C1∈C2,则F中删去C2,得 F'=F{C2}。 2SAT问题串行算法 SAT问题的DP算法是由 M. Davis和 H. Putnam于1960年首次提出,现在已经成为最 著名的SAT算法,其描述如下: 算法16.3SAT问题的DP算法 输入:合取范式F 输出:F是否可满足 (1)iF为空公式then return Yes if (2)ifF包含一个空子句then return No end if (3)iF包含一个子句{l}then /*单元子句规则* return DP(F[/ID) end if (4)iF包含一个文字l,但不包含 I then/*纯文字规则 return DP(FIND)3 1.2 SAT 问题 1.2.1 SAT 问题及其串行算法 1.SAT 问题描述 所谓可满足性问题（Satisfiability Problem）即 SAT 问题，其定义为：对于一个命题逻 辑公式，是否存在对其变元的一个真值赋值公式使之成立。这个问题在许多领域都有着非常 重要的意义，而且对其快速求解算法的研究成为计算机科学的核心课题之一。例如在机器定 理证明领域，某命题是否是一个相容的公理集合的推论，这个问题归结为该命题的反命题与 该公理集合一起是否是不可满足的。特别是 1971 年 Cook 首次证明了 SAT 是 NP-完全的， 从而大量的计算问题都可以归结到 SAT。正是由于 SAT 重要的理论和应用地位，众多学者 对它进行了广泛而深入的研究。 由命题逻辑知识可以知道，任何命题逻辑公式都逻辑等价与一个合取范式(Conjunctive Normal Form，简写为 CNF),因此本文只讨论 CNF 的 SAT 求解问题。 下面给出几种常见的 SAT 问题化简策略，以下均假定 F 是 CNF 范式：①单元子句规则： 若 C=｛L｝是 F 的子句，则 F 变为 F’=F[F/1]；②纯文字规则：若文字 L 出现在 F 中，而  L 不出现 F 中，则 L 称为 F 的纯文字。F 变为 F’=F[F/1]；③重言子句规则：若 C∈F 且 C 是 重言子句，则从 F 中删去 C 得 F’=F-C；④两次出现规则：若 L∈C1， L∈C2，且 L 和  L 都不在其它子句中出现，则将 C1 ，C2 合并为 C’=( C1-｛L｝)∪( C2-｛  L｝)，F 变为 F’=F- ｛C1, C2｝∪｛C’｝；⑤包含规则：若 C1 ，C2是 F 的子句，且 C1∈C2，则 F 中删去 C2，得 F’=F-｛C2｝。 2.SAT 问题串行算法 SAT 问题的 DP 算法是由 M.Davis 和 H.Putnam 于 1960 年首次提出[2]，现在已经成为最 著名的 SAT 算法，其描述如下： 算法 16.3 SAT 问题的 DP 算法 输入：合取范式 F。 输出：F 是否可满足。 procedure DP(F) Begin (1) if F 为空公式 then return Yes end if (2) if F 包含一个空子句 then return No end if (3) if F 包含一个子句{l} then /* 单元子句规则 */ return DP(F[l/1]) end if (4) if F 包含一个文字 l，但不包含  l then /* 纯文字规则 */ return DP(F[l/1])