公式等效为SMT文件

Question

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

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

​

​

我想展示这两个公式给出的结果与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)

Answer 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和fml2确实是等价的。)