公式等式(Smt)

Question

我的公式是：(a和b和c)意味着( c )当且仅当(a和b)转化为CNF：(a或b或C)或(a或b或c)和(b或a)和(c或a)

这个公式是相等的，我从真值表中检查过，如您所见：

​

​

因此，我编写了下面的代码，以便显示格式是相等的，但它会给出错误。关于密码的事请帮忙。

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