公式等效为 SMT 文件答案

【问题标题】：Formula equivalence as SMT file公式等效为 SMT 文件
【发布时间】：2022-01-25 15:01:44
【问题描述】：

从真值表可以看出，我有 SMT 公式：

为了定义 3-sat 问题，我添加了两个新变量 d 和 e。无论 d 和 e 的值如何，真值表对于相同的 a b c 给出相同的结果。

我想展示这两个公式给出的结果与 SMT 相同。所以我在下面写代码。我有两个问题我的代码有什么问题，我想这是真的，但它给出了错误。第二个问题，即使有两个新变量，我能否证明这种平衡。谢谢。

(declare-fun a () Bool)
(declare-fun b () Bool)
(declare-fun c () Bool)
(declare-fun d () Bool)
(declare-fun e () Bool)

(define-fun fml1 () Bool
    (or (or a (or b (not c)))
    (and (or b (or c (not a)))
         (and (or d (or a (not b)))
            (and (or a (or (not b) (not d)))
                (and (or e (or a (not c)))
                    (and (or a (or (not e) (not c)))
)

(define-fun fml2 () Bool
    (implies (and (not a) (and (not b) c))
             (= a (or b c)))
)

(assert (distinct fml1 fml2))
(check-sat)

【问题讨论】：

标签： z3 smt

【解决方案1】：

您没有正确关闭第一个公式中的所有括号，即当您定义 fml1 时。它应该是这样的：

(define-fun fml1 () Bool
    (or (or a (or b (not c)))
    (and (or b (or c (not a)))
         (and (or d (or a (not b)))
            (and (or a (or (not b) (not d)))
                (and (or e (or a (not c)))
                    (and (or a (or (not e) (not c)))))))))
)

注意额外的括号以关闭公式，以平衡括号。您应该使用可以匹配括号的编辑器来提醒您此类问题。

（请注意，我实际上并没有检查您是否正确编写了公式。只是括号匹配以关闭您开始的所有公式。如前所述，z3 在此生成unsat，建议fml1 和@987654325 @ 确实是等价的。）

【讨论】：