Is that normal that Z3 solver cannot solve 2^x=4?

Question

I have tried to solve 2^x=4 with Z3, by putting the following on the Z3 website: https://rise4fun.com/z3/tutorial.

(declare-const x Real) 
(declare-const y Real) 
(declare-const z Real) 
(assert (=(^ 2 x) 4)) 
(check-sat) 
(get-model)

Z3 produced

unknown
(model 
)

Am I misusing Z3?

Answer 1

Problems involving exponentials are typically beyond the reach of z3, or general-purpose SMT solvers. This doesn't mean that they cannot solve them: Theory of reals is decidable. But they may not have the right "heuristics" to kick in to answer every query involving exponentials as sat/unsat. You can search stack-overflow for keywords like nnf, non-linear, etc., to see a plethora of questions regarding queries that involve such difficult terms.

Having said that, there's a separate line of research called delta-satisfiability that can help with these sorts of problems to a great extent. Note that delta-satisfiability is different than regular satisfiability. It means either the formula is satisfiable, or a delta-perturbation of it is. The most prominent such solver is dReal, and you can read all about it here: http://dreal.github.io/

For your query, dReal says:

[urfa]~/qq>dreal a.smt2
delta-sat with delta = 0.001
(model
  (define-fun x () Real [2, 2])
  (define-fun y () Real [-0.0005, 0.0005])
  (define-fun z () Real [-0.0005, 0.0005])
)

(You didn't actually use y and z in your query, so you can ignore those outputs.)

As you can see dReal determines x must be in the range [2, 2], i.e., it must be 2. But it also says delta-sat with delta = 0.001: This means it has ensured the correctness within that factor. (You can tweak the factor yourself, making it arbitrarily small, but not zero.) When you have problems that arise from physical systems, delta-sat is the right choice in modeling them in the SMT-world.