3-SAT与CNF的区别及Z3求解3-SAT的SMT-LIB示例咨询

我们以下面这个3-SAT问题为例进行演示：
待求解的CNF公式包含3个布尔变量p、q、r，共4个子句，具体形式为：

(p ∨ ¬q ∨ r) ∧ (¬p ∨ q ∨ ¬r) ∧ (p ∨ q ∨ r) ∧ (¬p ∨ ¬q ∨ ¬r)

完整SMT-LIB代码 #

(set-logic QF_BOOL)
; 声明三个布尔变量
(declare-fun p () Bool)
(declare-fun q () Bool)
(declare-fun r () Bool)
; 断言所有子句成立
(assert (or p (not q) r))
(assert (or (not p) q (not r)))
(assert (or p q r))
(assert (or (not p) (not q) (not r)))
; 求解可满足性
(check-sat)
; 输出可满足赋值
(get-model)

运行结果说明 #

将上述代码输入Z3求解器执行，会首先返回sat表示该公式可满足，随后输出对应的赋值模型，示例输出如下：

sat
(
  (define-fun r () Bool
    false)
  (define-fun q () Bool
    false)
  (define-fun p () Bool
    true)
)

该结果表示p=true、q=false、r=false是一组有效解，代入原公式验证可知所有子句均成立。
如果输入的3-SAT公式本身不可满足，求解器会直接返回unsat，表示不存在能满足所有子句的赋值。

内容的提问来源于stack exchange，提问作者Promise89