无限制命题公式转CNF、3-SAT的实例实现及SMT-LIB2输出咨询

用到的合取范式重写规则 #

• 双条件消去：α ↔ β 等价于 (¬α ∨ β) ∧ (¬β ∨ α)
• 蕴含消去：α → β 等价于 ¬α ∨ β
• 德摩根律1：¬(α ∨ β) 等价于 ¬α ∧ ¬β
• 德摩根律2：¬(α ∧ β) 等价于 ¬α ∨ ¬β
• 双重否定消去：¬¬α 等价于 α
• 分配律1：α ∨ (β ∧ γ) 等价于 (α ∨ β) ∧ (α ∨ γ)
• 分配律2：(α ∧ β) ∨ γ 等价于 (α ∨ γ) ∧ (β ∨ γ)

1. 原始无限制命题公式（USAT-org） #

本次演示使用包含多类运算符的典型公式：(a ↔ b) → ¬(c ∨ d)
该公式包含双条件、蕴含、嵌套否定、析取多种结构，可覆盖大多数转换规则的应用场景。 #

2. 转换为CNF的分步过程 #

1. 消去蕴含：代入蕴含消去规则，原公式变为 ¬(a ↔ b) ∨ ¬(c ∨ d)
2. 消去双条件：代入双条件消去规则，得到 ¬[(¬a ∨ b) ∧ (¬b ∨ a)] ∨ ¬(c ∨ d)
3. 向内推进否定：
   • 对双条件外层的否定应用德摩根律2，得到 [¬(¬a ∨ b) ∨ ¬(¬b ∨ a)] ∨ ¬(c ∨ d)
   • 对三处析取结构的否定分别应用德摩根律1：
     • ¬(¬a ∨ b) = a ∧ ¬b
     • ¬(¬b ∨ a) = b ∧ ¬a
     • ¬(c ∨ d) = ¬c ∧ ¬d
   • 代入后公式简化为 [(a ∧ ¬b) ∨ (b ∧ ¬a)] ∨ (¬c ∧ ¬d)
4. 应用分配律转CNF：
   • 先展开前半部分(a ∧ ¬b) ∨ (b ∧ ¬a)，消去重言式a∨¬a和b∨¬b后得到 (a ∨ b) ∧ (¬a ∨ ¬b)
   • 再将后半部分(¬c ∧ ¬d)与前半部分做两次分配律运算，最终得到CNF：
     (a ∨ b ∨ ¬c) ∧ (a ∨ b ∨ ¬d) ∧ (¬a ∨ ¬b ∨ ¬c) ∧ (¬a ∨ ¬b ∨ ¬d)

3. 3-SAT转换说明 #

本次演示得到的CNF所有子句长度均为3，已经符合3-CNF要求。如果转换得到的子句长度大于3，可通过新增辅助变量的方式转换：
对于长度为n（n>3）的子句(l1 ∨ l2 ∨ l3 ∨ ... ∨ ln)，新增n-3个辅助变量z1,z2...z(n-3)，转换为如下等价可满足的3-CNF子句组：
(l1∨l2∨z1) ∧ (¬z1∨l3∨z2) ∧ ... ∧ (¬z(n-3)∨l(n-1)∨ln) #

4. 转换后的3-CNF格式SMT-LIB2文件（USAT-converted） #

(set-logic QF_BOOL)
; 声明原始命题变量
(declare-const a Bool)
(declare-const b Bool)
(declare-const c Bool)
(declare-const d Bool)
; 断言转换后的3-CNF公式
(assert (and
  (or a b (not c))
  (or a b (not d))
  (or (not a) (not b) (not c))
  (or (not a) (not b) (not d))
))
; 求解并输出模型
(check-sat)
(get-model)

5. 等价性验证方法 #

将原始无限制公式也写成SMT-LIB2格式提交给SAT求解器，对比二者的求解结果：转换后的3-CNF公式与原始公式可满足性完全一致，原始公式的所有可满足赋值都对应转换后公式的可满足赋值，反之亦然。

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