无限制表格至限制表格(CNF)
无限制表格至限制表格(CNF)
提问于 2021-12-05 12:50:07
我需要把不受限制的命题公式转换成CNF，然后转换成3-SAT。我知道把公式转换成连接范式的重写规则。
α ↔ β (¬α ∨ β) ∧ (¬β ∨ α)
α → β ¬α ∨ β (4.2)
¬(α ∨ β) ¬α ∧ ¬β (4.3)
¬(α ∧ β) ¬α ∨ ¬β (4.4)
¬¬α α (4.5)
α ∨ (β ∧ γ) (α ∨ β) ∧ (α ∨ γ) (4.6)
(α ∧ β) ∨ γ (α ∨ γ) ∧ (β ∨ γ 但我不明白我是怎么找到现实生活中关于概念的例子的。你能帮上忙吗。我找不到现实生活的例子。谢谢。
实际上，我试图证明，不受限制的公式可以转换为受限形式，两者的解决方案是相同的。因此，我写任何不受限制的命题公式，把它转换成CNF，然后再转换成3-SAT(手工)，这样我就可以显示类似的结果。因此，我需要USAT-org和USAT-转换，其中org是不受限制的公式，在3-CNF中转换为SMT语法(SMT-LIB2 2文件)。
回答 1
Stack Overflow用户
发布于 2021-12-06 19:00:05
你可以一次一个地去做。让我们以第二个例子为例：
α → β变成：
¬α ∨ β在SMTLib中，您可以通过断言它们的等价性并检查它们的unsat来证明它们的等价性。其思想是，如果否定是不可满足的，那么所有的价值都必须是等价的。
(set-option :produce-models true)
(set-logic QF_BV)
(declare-fun alpha () Bool)
(declare-fun beta () Bool)
(define-fun lhs () Bool (=> alpha beta))
(define-fun rhs () Bool (or (not alpha) beta))
(assert (not (= lhs rhs)))
(check-sat)这些指纹：
unsat因此，上述转换对于alpha和beta的任意值都是正确的。
使用同样的技巧，您应该证明您的每个转换。然后是一些元推理(或者您可以自己手工归纳)来说明，如果您将这些转换应用于所有子公式，直到它们都被写入，您就可以将任意公式转换成这种形式。注意，这最后一步不能直接用SMT求解器完成，因为它需要归纳法；但是您可以手动证明使用适当的定理证明程序，如Isabelle/ACL2 2/Hol/Lean等等。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/70234457
复制相关文章
相似问题
腾讯云开发者
