Satisfying Models under Tseitin Encoding

z3

Solution

This is a bug in the new `tseitin-cnf` tactic. I fixed the bug, and the fix will be available in the next release (Z3 4.1). In the meantime, you can workaround the bug by using the rounds of simplification. That is, use

 (apply 
    (then (! simplify :elim-and true)
          (! simplify :elim-and true)
          tseitin-cnf))

instead of

 (apply 
    (then (! simplify :elim-and true)
          tseitin-cnf))

Problem

I am using the following code fragment in z3 4.0 to convert a formula to CNF. ``` (set-logic QF_UF) ( set-option :produce-models true ) ; ------ snip ------- ; ; declarations, ; and assert statement ; of "original" formula ; here. ; ; ------ snap ------- ( apply ( then ( ! simplify :elim-and true ) tseitin-cnf ) ) ``` I get something like the following: ``` (goals (goal ; ------ snip ------- ; ; Lot's of lines here ; ; ------ snap ------- :precision precise :depth 2) ) ``` I was assuming that each of the expressions that follows `goal` is one clause of the CNF, i.e., all those expressions should be conjuncted to yield the actual formula. I will refer to this conjunction as the "encoded" formula. Obviously, the original formula and the encoded formula are not equivalent, as the encoded formula contains new variables `k!0, k!1, ...` which do the Tseitin encoding. However, I was expecting that they are equisatisfiable, or actually that they are satisfied by the same models (when disregarding the `k!i` variables). I.e., I was expecting that `(encoded formula) AND (NOT original formula)` is unsatisfiable. Unfortunately, this does not seem to be the case; I have a counterexample where this check actually returns `sat`. Is this a bug in z3, am I using it wrong, or are any of my assumptions not valid?

Original source