Search code examples
z3sat

Equility of formulas(smt)

I have formulas which is: (!a and !b and c) implies (c iff (a and b) Transformed to formula as a CNF : (a or b or !c) or (!a or b or c) and (!b or a) and (!c or a)

This formulas equal to each other I checked from truth table as you can see:

enter image description here

So I write code as below in order show the formuas are equisatisfable but it gives error. Please help about codes.

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

  • You've a couple of syntax-errors in how you wrote the formula. Also note that you shouldn't really set the logic to QF_LIA since there's no arithmetic involved here. (QF_LIA means quantifier-free linear integer arithmetic.) Just leave it unset. Another note: while z3 accepts iff as a function, it's not part of the standard so far as I know; so best to use = instead, which means the same thing over booleans. It's also a good idea to give names to different parts of the formula to keep it readable.

    Based on this, here's how you can write your equivalence check:

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

    This prints:

    unsat

    meaning that fml1 and fml2 are equivalent.