Displaying a goal as DIMACS does not effectively require calling the tseitin-cnf tactic, although it should

[ekuiter]

Hi,
thanks for creating such a high-quality SMT solver! However, I believe I found a bug related to CNF representations (I reproduced it in z3 4.11.2 and 4.12.1).

I am using Z3 to transform Boolean formulas into CNF using its tseitin-cnf tactic. The simplest Python code I found to do that is this:

from z3 import *
goal = Goal()
with open(sys.argv[1], 'rb') as file:
  goal.add(parse_smt2_string(file.read()))
goal = Tactic("tseitin-cnf")(goal)[0] # this line calls the Tseitin tactic
print(goal.dimacs())

This works reliably.

However, when the second-to-last line is omitted (e.g., forgotten), things get weird.
This sample input:

(declare-fun X () Bool)
(assert (and
     (or (not X))
     (or (and X (not X)))
))

is (correctly) transformed into the following when the Tseitin tactic is applied:

p cnf 1 1
1 0
c 1 false

(that is, the formula is an obvious contradiction), but it is (wrongly) transformed into the following when the Tseitin tactic is not applied:

p cnf 2 2
-1 0
2 0
c 1 X
c 2 and

which is satisfiable, although it should not be (the inner and expression that violates CNF is not represented correctly).

For larger formulas (e.g., the feature dependencies in the Linux kernel 2.6.12), this creates the impression that Z3 creates a correct CNF, although it doesn't (satisfiability is not generally preserved, as shown above).

It can be argued that this is simply the wrong way to call the Z3 library. However, the fact that the user has to apply the Tseitin tactic explicitly is not very well-documented, and one would expect a helpful error message instead of returning an incorrect DIMACS file.

In fact, it seems that raising an error is also the intended behavior, as there is a check for CNF before printing a goal as DIMACS: https://github.com/Z3Prover/z3/blob/master/src/api/api_goal.cpp#L200
So, my guess is that goal::is_cnf contains a bug, which only detects a violation of CNF in some, but not all cases (e.g., it does not detect that (assert (and (or (not X)) (or (and X (not X))) is not in CNF, but it does for (assert (and (or (and X (not X)))).

As a casual user of the library, it is easy to mistake the c 2 and variable above for a proper Tseitin skolem variable (k!0 in Z3) and believe that the CNF tactic was applied correctly. (Case in point is kmax, which does not apply the CNF tactic at all and therefore runs into this exact problem.)

Maybe this can be improved so future users don't stumble like I did. Thanks!

[NikolajBjorner]

so far a couple of bugs fixes based on your post.

Regarding general behavior: it is allowed to create CNF of non-propositional formulas. To make this work I append a comment section with definitions. The definitions are for diagnostic purposes: they list the function symbol and nothing more.
The expectation is that CNF then encodes a propositional abstraction of the original formula.

[ekuiter]

thanks for the quick fix!

[ekuiter]

I have another question (or maybe bug): In the latest version 4.12.1, calling Tactic("tseitin-cnf") does not always work. For some inputs, I get the error message operator not supported, apply simplifier before invoking this strategy.
Example input:

(declare-fun CONFIG_MTD_DOC2001 () Bool)
(declare-fun CONFIG_MTD_DOC2000 () Bool)
(declare-fun CONFIG_MTD_DOC2001PLUS () Bool)
(declare-fun CONFIG_MTD () Bool)
(assert (let (
      (a!202 (and (not CONFIG_MTD_DOC2001)
                  (not CONFIG_MTD_DOC2000)
                  (not CONFIG_MTD_DOC2001PLUS)
                  (or CONFIG_MTD_DOC2001 CONFIG_MTD_DOC2000))))
  (and (or a!202
                 (and (or CONFIG_MTD_DOC2001
                          CONFIG_MTD_DOC2000
                          CONFIG_MTD_DOC2001PLUS)
                      (not (and CONFIG_MTD a!202)))))))

In version 4.11.2, this worked fine. Is this intended?

I am now using Then("simplify", "elim-and", "tseitin-cnf"), which works, but I am not sure whether both simplify and elim-and are necessary. Looking at https://github.com/Z3Prover/z3/blob/master/src/tactic/core/tseitin_cnf_tactic.cpp#L903, I see that elim-and should be called by tseitin-cnf automatically, so why do I need to call it explicitly? I thought that's the difference between tseitin-cnf and tseitin-cnf-core, so to my mind calling tseitin-cnf without simplify and elim-and should work, too.

[NikolajBjorner]

You should use

(apply (then (with simplify :elim_and true) tseitin-cnf))

This produces better CNF than default.

I fixed some of the fragility issues so you don't have to use simplification.

[ekuiter]

Hi, please consider the following SMTlib file:
min-bool.smt.txt
In Z3 4.12.1, the following:

import z3

goal = z3.Goal()
with open('min-bool.smt', 'rb') as file:
  goal.add(z3.parse_smt2_string(file.read()))

goal_1 = z3.Tactic("tseitin-cnf")(goal)[0]
goal_2 = z3.Then("simplify", "elim-and", "tseitin-cnf")(goal)[0]

throws for both goal_1 and goal_2:

Traceback (most recent call last):
  File "/home/x/smt2dimacs.py", line 8, in <module>
    goal_1 = z3.Tactic("tseitin-cnf")(goal)[0]
  File "/usr/local/lib/python3.10/dist-packages/z3_solver-4.12.1.0-py3.10-linux-x86_64.egg/z3/z3.py", line 8254, in __call__
    return self.apply(goal, *arguments, **keywords)
  File "/usr/local/lib/python3.10/dist-packages/z3_solver-4.12.1.0-py3.10-linux-x86_64.egg/z3/z3.py", line 8244, in apply
    return ApplyResult(Z3_tactic_apply(self.ctx.ref(), self.tactic, goal.goal), self.ctx)
  File "/usr/local/lib/python3.10/dist-packages/z3_solver-4.12.1.0-py3.10-linux-x86_64.egg/z3/z3core.py", line 3849, in Z3_tactic_apply
    _elems.Check(a0)
  File "/usr/local/lib/python3.10/dist-packages/z3_solver-4.12.1.0-py3.10-linux-x86_64.egg/z3/z3core.py", line 1482, in Check
    raise self.Exception(self.get_error_message(ctx, err))
z3.z3types.Z3Exception: b'operator not supported, apply simplifier before invoking this strategy'

Can you tell me what I am doing wrong? The file only uses and, or, and not. We are out of ideas over at paulgazz/kmax/issues/226.