Encoding returns “unknown”

Question

For this example: http://pastebin.com/QyebfD1p z3 and cvc4 return "unknown" as result of check-sat. Both are not very verbose about the cause, is there a way to make z3 more verbose about its execution ?

Answer 1

Your script uses the tactic

s = Then('simplify','smt').solver()

This tactic applies the Z3 simplifier, and then executes a "general purpose" SMT solver available in Z3. This solver is not complete for nonlinear arithmetic. It is based on a combination of: Simplex, Interval Arithmetic and Grobner Basis. One of the big limitations of this module is that it can't find models/solutions containing irrational numbers. In the future, we will replace this module with new nonlinear solvers available in Z3.

For nonlinear arithmetic, we usually suggest the nlsat solver available in Z3. This is a complete procedure and is usually very effective for unsatisfiable and satisfiable instances. You can find more about nlsat in this article. To use nlsat, we have to use

s = Tactic('qfnra-nlsat').solver()

Unfortunately, nlsat will get stuck in your example. It will get stuck computing Subresultants of very big polynomials produced during solving..

Z3 has yet another engine for handling nonlinear arithmetic. This engine reduces the problem to SAT. It is only effective on satisfiable problems that have solutions of the form a + b sqrt(2) where a and b are rational numbers. Using this engine, we can solve your problem in a very short amount of time. I attached the result in the end of the post. To use this engine, we have to use

s = Then('simplify', 'nla2bv', 'smt').solver()

EDIT Moreover, the tactic nla2bv encodes the rational numbers a and b as a pair of bit-vectors. By default, it uses bit-vectors of size 4. However, this value can be specified using the option nlsat_bv_size. This is not a global option, but an option provided to the tactic nla2bv. Thus, nla2bv can only find solutions of the form a + b sqrt(2) where a and b can be encoded using a small number of bits. If a satisfiable problem does not have a solution of this form, this tactic will fail and return unknown. END EDIT

Your example also suggests that we have to improve nlsat, and make it more effective as a model/solution finding procedure. The current version gets stuck when trying to show that the problem has no solution. We are aware of these limitations and are working on new procedures to workaround them.

BTW, in the Python front-end, Z3 displays the models/solutions in decimal notation. However, everything is computed precisely. To get the precise representation of the solution. We can use the method sexpr(). For example, I changed your loop to

for d in m.decls():
    print "%s = %s = %s" % (d.name(), m[d], m[d].sexpr())

In the new loop, I'm displaying the result in decimal notation and the internal precise one. The meaning of (root-obj (+ (* 2 (^ x 2)) (* 12 x) (- 7)) 2) is the 2nd root of the polynomial 2*x^2 + 12x - 7.

EDIT Z3 provides combinators for creating non-trivial solvers. In the examples above, we used Then to perform the sequential composition of different tactics. We may also use OrElse to try different tactics. and TryFor(t, ms) that tries tactic t for ms milliseconds, and fails if the problem can't be solved in the given time. These combinators can be used to create tactics that use different strategies for solving a problem. END EDIT

sat
Presenting results
traversing model...
s_2_p_p = 0.5355339059? = (root-obj (+ (* 2 (^ x 2)) (* 12 x) (- 7)) 2)
s_1_p_p = 0 = 0.0
s_init_p_p = 0.2928932188? = (root-obj (+ (* 2 (^ x 2)) (* (- 4) x) 1) 1)
s_2_p = 0.7071067811? = (root-obj (+ (* 2 (^ x 2)) (- 1)) 2)
s_1_p = 0 = 0.0
s_init_p = 0.2928932188? = (root-obj (+ (* 2 (^ x 2)) (* (- 4) x) 1) 1)
epsilon = 0 = 0.0
p_b2_s2_s_sink = 0.9142135623? = (root-obj (+ (* 4 (^ x 2)) (* 4 x) (- 7)) 2)
p_b2_s2_s_target = 0.0857864376? = (root-obj (+ (* 4 (^ x 2)) (* (- 12) x) 1) 1)
p_b2_s2_s_2 = 0 = 0.0
p_b2_s2_s_1 = 0 = 0.0
p_a2_s2_s_sink = 0 = 0.0
p_a2_s2_s_target = 0.8284271247? = (root-obj (+ (^ x 2) (* 4 x) (- 4)) 2)
p_a2_s2_s_2 = 0.1715728752? = (root-obj (+ (^ x 2) (* (- 6) x) 1) 1)
p_a2_s2_s_1 = 0 = 0.0
sigma_s2_b2 = 1 = 1.0
sigma_s2_a2 = 0 = 0.0
p_b1_s1_s_sink = 1 = 1.0
p_b1_s1_s_target = 0 = 0.0
p_b1_s1_s_2 = 0 = 0.0
p_b1_s1_s_1 = 0 = 0.0
p_a1_s1_s_sink = 1 = 1.0
p_a1_s1_s_target = 0 = 0.0
p_a1_s1_s_2 = 0 = 0.0
p_a1_s1_s_1 = 0 = 0.0
sigma_s1_b1 = 0 = 0.0
sigma_s1_a1 = 1 = 1.0
p_sinit_sink = 0.7071067811? = (root-obj (+ (* 2 (^ x 2)) (- 1)) 2)
p_sinit_target = 0.2928932188? = (root-obj (+ (* 2 (^ x 2)) (* (- 4) x) 1) 1)
p_sinit_2 = 0 = 0.0
p_sinit_1 = 0 = 0.0
s_sink = 0 = 0.0
s_target = 1 = 1.0
s_2 = 0.0857864376? = (root-obj (+ (* 4 (^ x 2)) (* (- 12) x) 1) 1)
s_1 = 0 = 0.0
s_init = 0.2928932188? = (root-obj (+ (* 2 (^ x 2)) (* (- 4) x) 1) 1)

EDIT You can solve the problem in your comment by using the tactic

s = Then('simplify', 'nlsat').solver()

This tactic will solve the problem in a couple of seconds, and produce the solution in the end of the post. As I said above, nlsat is complete, but it may take very long time. Your problem is on the fringe of what the current version of Z3 can decide/solve automatically. We can combine different tactics with OrElse and TryFor to make it more stable. Example:

s = OrElse(TryFor(Then('simplify', 'nla2bv', 'smt', 'fail-if-undecided'), 1000),
           TryFor(Then('simplify', 'nlsat'), 1000),
           TryFor(Then('simplify', 'nla2bv', 'smt', 'fail-if-undecided'), 10000),
           Then('simplify', 'nlsat')).solver()

The tactic above tries the nla2bv approach for 1 sec, then nlsat for 1 sec, then nla2bv for 10 secs, and finally nlsat without a timeout.

I know this is not an ideal solution, but variations like that may be useful workarounds until the next solver for nonlinear arithmetic is ready. Moreover, Z3 has many other tactics that may be used to simplify/preprocess the problem before we invoke nlsat. END EDIT

s_init = 15/32
s_1 = 7/16
s_2 = 1/2
s_target = 1
s_sink = 0
p_sinit_1 = 1/2
p_sinit_2 = 1/4
p_sinit_target = 1/8
p_sinit_sink = 1/8
sigma_s1_a1 = 1/2
sigma_s1_b1 = 1/2
p_a1_s1_s_1 = 1/2
p_a1_s1_s_2 = 1/4
p_a1_s1_s_target = 1/8
p_a1_s1_s_sink = 1/8
p_b1_s1_s_1 = 1/2
p_b1_s1_s_2 = 1/4
p_b1_s1_s_target = 1/16
p_b1_s1_s_sink = 3/16
sigma_s2_a2 = 1/2
sigma_s2_b2 = 1/2
p_a2_s2_s_1 = 1/2
p_a2_s2_s_2 = 1/4
p_a2_s2_s_target = 11/64
p_a2_s2_s_sink = 5/64
p_b2_s2_s_1 = 3/4
p_b2_s2_s_2 = 1/32
p_b2_s2_s_target = 9/64
p_b2_s2_s_sink = 5/64
epsilon = 1/4
s_init_p = 1649/3520
s_1_p = 797/1760
s_2_p = 103/220
s_init_p_p = 1809/3904
s_1_p_p = 813/1952
s_2_p_p = 127/244

EDIT 2 Your problems are on the fringe of what Z3 can do in a reasonable amount of time. Nonlinear real arithmetic is decidable, but is very expensive. Regarding debugging/tracing what is going on in Z3. Here are some possibilities:

• We can enable verbose messages using the command: set_option("verbose", 10). The number is the verbosity level: 0 == "no message", and higher numbers == "more messages".

• Compile Z3 with support for tracing. See this post for more information.

• Create a log of the Z3 APIs invoked by the Python program using the command open_log("z3.log"). This command should be invoked before any other Z3 API call. Then execute the log using the z3 executable inside of gdb. So, you will be able to stop the execution and find where Z3 is stuck. The nlsat solver usually gets stuck in two different places:

  1. Computing subresultants (the procedure psc_chain will be on the stack), and

  2. isolating the roots of polynomials with algebraic coefficients (the procedure isolate_roots will be on the stack).

Problem 2 will be soon fixed, after we replace the old algebraic number package with the new one that is much more efficient. Unfortunately, it seems your problems get stuck in the subresultant step.

Another remarks: although nla2bv was effective for your original benchmark, it is unlikely your new benchmarks will have a solution of the form a + b sqrt(2) where a and b are rational numbers. So, using nla2bv is just overhead. The tactic nlsat assumes the problem to be in CNF. So, for pastebin.com/QRCUQE10, we have to invoke tseitin-cnf before invoking nlsat. Another option is to use "big" tactic qfnra-nlsat. It invokes many pre-processing steps before invoking nlsat. However, some of these steps may make some problems harder to solve.

END EDIT 2