公式相等（smt）

Question

我有以下公式： (!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)

这个公式彼此相等我从事实中检查table 如你所见：

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

(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)

Answer 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是等价的。

公式相等（smt）

Equility of formulas(smt)

z3

sat