Geek Answers Handbook

Satisfactory Models Under Zeitin Coding

I am using the following code snippet 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 of lines here ; ; ------ snap ------- :precision precise :depth 2) )

I assumed that each of the expressions following goal is one of the CNF points, i.e. all of these expressions must be combined to get the actual formula. I will refer to this connection as a “coded” formula.

Obviously, the original formula and the encoded formula are not equivalent, since the encoded formula contains the new variables k!0, k!1, ... that encode Zeitin. However, I expected that they would be satisfactory or actually be satisfied with the same models (if you do not take into account the variables k!i ).

Ie, I expected (encoded formula) AND (NOT original formula) be unsatisfactory. Unfortunately, this does not seem to be the case; I have a counterexample where this check really returns sat .

Is this a bug in z3, am I using it incorrectly or are any of my assumptions invalid?

+4
source share
1 answer

This is a mistake in the new tseitin-cnf . I fixed the error and the correction will be available in the next version (Z3 4.1). In the meantime, you can get around the error using rounds of simplification. That is, use

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

instead

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

More articles:


All Articles