合取範式的可滿足性判定算法和謂詞邏輯不可判定性

作爲本系列的最後一篇文章，我們來看被廣爲研究的SAT問題。 SAT問題是第一個被證明爲NP問題的判定問題。更多信息可以去百度或者維基一下。   前面我們看到了Horn公式可滿足性的判定算法，現在把它推廣到任意公式Φ。首先將公式變換成具有下面語法的等值公式：φ ::= p | (¬φ) | (φ ∧ φ)。變換方法如下（已被證明變換後是等價的）：  在結果T(φ)的語法樹中要公共子公式共享，這樣將語

>>阅读原文<<