Solvability of nonlinear real arithmetic with premises

Question

A small example indicates that the nonlinear real arithmetic (NRA) solvers are hindered when NRA assertions are labeled by premises pi in connection with (sat p1 ... pn) checks.

The following SMT2 example returns SAT with the correct model:

(declare-const p1 Bool)
(declare-const p2 Bool)
(declare-const p3 Bool)
(declare-const p4 Bool)

(declare-const x1 Real)
(declare-const x2 Real)
(declare-const x3 Real)

(assert (=> p1 (= x1 (/ 1.0 (* x2 x2)))))
(assert (=> p2 (not (= x2 0.0))))
(assert (=> p3 (= x3 (* 2.0 x1))))
(assert (=> p4 (= x3 5.0)))

(assert (and p1 p2 p3 p4))
(check-sat)
(get-model)

The following semantically equivalent example returns unknown:

(declare-const p1 Bool)
(declare-const p2 Bool)
(declare-const p3 Bool)
(declare-const p4 Bool)

(declare-const x1 Real)
(declare-const x2 Real)
(declare-const x3 Real)

(assert (=> p1 (= x1 (/ 1.0 (* x2 x2)))))
(assert (=> p2 (not (= x2 0.0))))
(assert (=> p3 (= x3 (* 2.0 x1))))
(assert (=> p4 (= x3 5.0)))

(check-sat p1 p2 p3 p4)
(get-model)

Moreover, the model query returns a model, which is incorrect!

Working with the first style is not an option for me since I am particularly interested in getting unsat-cores from UNSAT problem instances, and I wish to dynamically combine "active" premises. However, by connecting the premise with "and", unsat core production is prevented.

It looks like the first example with (assert (and p1 p2 p3 p4)) is somehow simplified in a preprocessing step, so that the NRA solver looks at all four constraints together and is able to solve them. This seems not to be the case using the second example with (check-sat p1 p2 p3 p4).

Am I missing something? Thank you!

PS: I'm working with Z3 version 4.4.0 from the unstable branch (loaded 2015-03-26).

Christoph Wintersteiger Christoph Wintersteiger · Accepted Answer · 2015-03-26T13:54:53

This difference in behavior is explained by the fact that Z3 runs a different solver when assumptions are used. If no assumptions, incremental features, proofs or theory combination are required, it will run a new solver (NLSAT), while when at least one of those features are required, it falls back to an older, much weaker solver which gives up quickly and returns unknown. You can run Z3 with -v:100 and it will report

(combined-solver "using solver 1")
...
(nlsat :num-exprs ...)

The invalid model however is indeed something that shouldn't be output by default.

Solvability of nonlinear real arithmetic with premises

1 Answers