4

I'm new to Z3 and I'm trying to understand how it works, and what it can and cannot do. I know that Z3 has at least some support for exponentials through the power (^) operator (see Z3py returns unknown for equation using pow() function, How to represent logarithmic formula in z3py, and Use Z3 and SMT-LIB to define sqrt function with a real number). What I'm unclear on is how extensive this support is, and what kind of inferences z3 can make about exponentials.

Here's a simple example involving exponentials which z3 can analyze. We define an exponential function, and then ask it to verify that exp(0) == 1:

(define-fun exp ((x Real)) Real
  (^ 2.718281828459045 x))
(declare-fun x1 () Real)
(declare-fun y1 () Real)
(assert (= y1 (exp x1)))
(assert (not (=> (= x1 0.0) (= y1 1.0))))
(check-sat)
(exit)

Z3 returns unsat, as expected. On the other hand, here's a simple example which Z3 can't analyze:

(define-fun exp ((x Real)) Real
  (^ 2.718281828459045 x))
(declare-fun x1 () Real)
(declare-fun y1 () Real)
(assert (= y1 (exp x1)))
(assert (not (< y1 0.0)))
(check-sat)
(exit)

This should be satisfiable, since literally any value for x1 would give y1 > 0. However, Z3 returns unknown. Naively I might have expected that Z3 would be able to analyze this, given that it could analyze the first example.

I realize this question is a bit broad, but: can anyone give me any insight into how Z3 handles exponentials, and (more specifically) why it can solve the first example I gave but not the second?

Stephen Foster
  • 43
  • 3
  • 1
    Sometimes `(check-sat-using (or-else default qfnra-nlsat))` gives better results, using the non-linear sat engine. (Though it doesn't work for your second example.) In my experience, it's really hard to say when something works and when it doesn't once you have non-linear terms. – alias Mar 22 '18 at 16:46

1 Answers1

1

It is hard to say in general, since non-linear solving is challenging, but the case you presented is actually not so mysterious. You wrote:

(assert (= y (exp x)))
(assert (not (=> (= x 0) (= y 1))))

Z3 is going to simplify the second assertion, yielding:

(assert (= y (exp x)))
(assert (= x 0))
(assert (not (= y 1)))

Then it will propagate the first equality, yielding:

(assert (= y (exp 0)))
(assert (not (= y 1)))

Now when exp is expanded, you have a case of constant^constant, which Z3 can handle (for integer exponents, etc).

For the second case, you are asking it a very very basic question about variable exponents, and Z3 immediately barfs. That's not too odd, since so many questions about variable exponents are either known uncomputable or unknown but hard.

pavpanchekha
  • 2,073
  • 1
  • 17
  • 23
  • Thanks! This was very helpful (obvious in retrospect, really). Just to add to it for future reference: I've since been dealing with exponentials in Z3 a fair amount, and I've found that it can sometimes, but not always, propagate equalities in this manner and determine that it's evaluating constant^constant. For more complicated expressions, I've found it to be fairly sensitive to the exact formulation of the assertions you give it. One formulation will immediately return unknown, and another slightly different (but logically equivalent) formulation will immediately return unsat. – Stephen Foster Jun 01 '18 at 13:17
  • Yes, it'll be quite sensitive, because you're relying on the simplifier to massage the equation into a form that is decidable. Simplifying it manually is often going to be necessary, because the simplifier is not very smart. Generally, you will get "unknown" very fast since it is often a syntactic check. That you get "unsat" quickly I think is just a fact about the assertions you send. By the way, if my answer was correct I'd appreciate you "accepting" it. – pavpanchekha Jun 02 '18 at 18:03