作为本系列的最后一篇文章，我们来看被广为研究的SAT问题。
SAT问题是第一个被证明为NP问题的判定问题。更多信息可以去百度或者维基一下。
前面我们看到了Horn公式可满足性的判定算法，现在把它推广到任意公式Φ。首先将公式变换成具有下面语法的等值公式：φ ::= p | (¬φ) | (φ ∧ φ)。变换方法如下（已被证明变换后是等价的）：
在结果T(φ)的语法树中要公共子公式共享，这样将语法树变成一个有向无回路(环)图(DAG)。
例如，φ = p∧ ¬(q ∨¬p)，变换后T(φ)=p ∧¬¬(¬q ∧¬¬p)。它们语法树分别是：
看明白怎么就是“分享子公式”了吧。
对于变换后的语法树进行从上到下的标记，根部标记T，如果没有冲突标记的结果就是一次合格的赋值。标记中需要用到的逼迫规则有下：
那么这个算法能判断所有的公式吗？答案是否定的！对于形如¬(φ1 ∧ φ2)这样的公式无法判断（自己试一下）。
上述算法是一个线性时间算法。我们还有一个三次多项式时间算法。算法的主要思想:
1.任选一个未标记结点试探标记T,运行线性时间求解算法.若报告可满足,则输出可满足指派并停机;若算法报告失败或报告不可满足(矛盾),而不再有待试探的结点,算法报告”标记失败”并停机;否则转2.
2.对该结点标记F,运行线性时间求解算法.若报告可满足,则输出可满足指派并停机;若算法报告不可满足且在前面标记该结点时也报告不可满足,则报告不可满足并停机;否则将两次试探标记都相同的结点标记作为永久标记.转1.
这个算法也不是万能的，比如它对于下图语法树对应的CNF不能判定：
SAT问题目前依然是逻辑界和计算理论界的研究热点。有兴趣的可以关注一下。
命题逻辑公式是否定理最起码可以通过真值表查看是否可满足，那么对于谓词逻辑公式呢？我们是不是有其他什么方法可以判断谓词逻辑公司是否有效呢？
答案是否定的：给定一个谓词逻辑公式φ，|=φ是否有效是不可判定的。这有点震惊了，到底是啥意思呢？
我们采用问题归约技术：将一个已知不可判定问题归约到所考虑的判定问题，使得要考虑的判定问题可判定必导致已知的不可判定问题成为可判定问题，这就导致了矛盾。这证明我们要考虑的判定问题是不可判定的。（如果没有学过算法的，可以先花点时间了解下什么是规约）
那么哪个判定问题是不可判定问题呢？我们选择著名的波斯特对应问题（Post Correspondence Problem， PCP，你可以先百度一下）：PCP的一个问题实例由某个字母表Σ上串的两个表组成，这两个表的长度相等，一般称为A表和B表。对于某个正整数k，A=（s1,s2,...,sk），B=（t1,t2,...,tk）。（si, ti）表示一个对应对。如果存在整数序列i1,i2,...,in，当把这个序列解释成A表和B表中串的下标时，能够产生相同的串，则说这个PCP问题实例有解。i1,i2,...,in称为这个问题的一个解。PCP问题就是对于一个PCP实例，它是否有解。
波斯特对应问题是不可判定的。可以参考《自动机理论、语言和计算导论》John E. Hopcroft Rejeev Motwani Jeffrey D.Ullman著， 刘田、姜晖、王捍贫译，机械工业出版社，2004年6月第1版。
看一个波斯特对应问题实例：字母表Σ=｛0，1｝。
例1. A={1,10,011}, B={101,00,11}，其解为：（1，3，2，3），串是1011 10 011。
例2. A=｛1，10111，10｝，B=｛111，10，0｝，其解为(2,1,1,3)或(2,1,1,3,2,1,1,3)
例3. A={10,011,101},B={101,11,011} 这个PCP问题实例无解。
（你说什么？你感觉这个问题很简单，能够设计出算法？那你可以试试。）
定理 谓词逻辑公式的有效性判定问题是不可判定的：不存在判定算法，使得对于任给谓词逻辑公式Ф，判定是否|=Ф是有效的。
证明： 采用归约技术。对于给定的波斯特对应问题实例C，构造一个谓词逻辑公式Ф，且构造在有限的空间和时间内完成，使得｜=Ф有效当且仅当波斯特对应问题实例C有解。
设波斯特对应问题实例C：
构造公式Ф：函数符号F=｛e,f0 ,f1｝,e是常量，e,f0 ,f1是一元函数。谓词符号P。
