公式相等(smt)答案

【问题标题】：Equility of formulas(smt)公式相等(smt)
【发布时间】：2022-01-25 12:50:19
【问题描述】：

我有以下公式： (!a and !b and c) 暗示 (c iff (a and b) 转换为 CNF 公式： (a or b or !c) or (!a or b or c) and (!b or a) and (!c or a)

如你所见，我从真值表中检查了这个公式彼此相等：

所以我编写了如下代码，以显示公式是 equisatisfable 但它给出了错误。请帮助有关代码。

(set-logic QF_LIA)
(declare-fun a () Bool)
(declare-fun b () Bool)
(declare-fun c () Bool)

(assert (distinct (and((or(or a b (not c)(or ((not a) b c)) (or (not b) a)(or not c a) 
(and(or (not a) (not b) c) (iff a(or b c))
(check-sat)
; unsat
(exit)

【问题讨论】：

标签： z3 sat

【解决方案1】：

您在编写公式时有几个语法错误。另请注意，您不应该真正将逻辑设置为QF_LIA，因为这里不涉及算术。（QF_LIA 表示无量词线性整数运算。）不要设置它。另一个注意事项：虽然 z3 接受 iff 作为函数，但据我所知，它不是标准的一部分；所以最好改用=，这对布尔值意味着同样的事情。为公式的不同部分命名以保持可读性也是一个好主意。

在此基础上，您可以通过以下方式编写等效检查：

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

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

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

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

打印出来：

unsat

表示fml1 和fml2 是等价的。

【讨论】：

谢谢，我还有一个问题，与此问题类似，但更深入。