即命题逻辑的可满足性问题，可判定，也是第一个被证明为 NP 完全的问题。An extension of SAT is SMT 如果公式被限定为 Horn Clause 的形式，则问题变为 HORNSAT，为 P-complete，在线性时间可解。