z3 timeout on nonlinear constraints

Question

I have a timeout problem when using z3 for nonlinear real arithmetics. The following code is to check if the 4-dimensional hyper-rectangle has a volume greater than 50000 and also satisfies some constraints. But the z3 cannot give an answer within 1 minute. How to make it faster?

a0min = Real('a0min')
a0max = Real('a0max')
a1min = Real('a1min')
a1max = Real('a1max')
a2min = Real('a2min')
a2max = Real('a2max')
a3min = Real('a3min')
a3max = Real('a3max')
volume = Real('volume')

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

s.add(-a0min * (1.0 - a1max) + a2max * a3max <= -95000.0,
a0min >  0.0,
a0min < a0max,
a0max < 1000000.0,
a1min > 0.0,
a1min < a1max,
a1max < 1.0,
a2min > 1.0,
a2min < a2max,
a2max < 1000.0,
a3min > 1.0,
a3min < a3max,
a3max < 50.0,
(a0max - a0min) * (a1max -  a1min) * (a2max -  a2min) * (a3max - a3min) > 50000.0,
volume == (a0max - a0min) * (a1max -  a1min) * (a2max -  a2min) * (a3max - a3min))
print s.check()

And there is an interesting thing: if replacing some of the ">" and "<" with "<=" and ">=", the z3 solver can return the answer in two seconds. The corresponding code is as follows. Anyone knows why this happens?

a0min = Real('a0min')
a0max = Real('a0max')
a1min = Real('a1min')
a1max = Real('a1max')
a2min = Real('a2min')
a2max = Real('a2max')
a3min = Real('a3min')
a3max = Real('a3max')
volume = Real('volume')

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

s.add(-a0min * (1.0 - a1max) + a2max * a3max <= -95000.0,
a0min >=  0.0,
a0min <= a0max,
a0max <= 1000000.0,
a1min >= 0.0,
a1min <= a1max,
a1max <= 1.0,
a2min >= 1.0,
a2min <= a2max,
a2max <= 1000.0,
a3min >= 1.0,
a3min <= a3max,
a3max <= 50.0,

(a0max - a0min) * (a1max -  a1min) * (a2max -  a2min) * (a3max - a3min) > 50000.0,
volume == (a0max - a0min) * (a1max -  a1min) * (a2max -  a2min) * (a3max - a3min))
print s.check()

Answer 1

In the first case, Z3 got "stuck" computing with real algebraic numbers. If we execute your script with

 valgrind --tool=callgrind python nl.py

Interrupt after several minutes, and run

 kcachegrind 

We will see that Z3 is stuck inside algebraic_numbers::isolate_roots. The current real algebraic number package used by the nlsat solver is very inefficient. We have a new package for computing with algebraic numbers, but it is not integrated with nlsat yet.

One trick to avoid algebraic number computations is to use only strict inequalities. The equality volume == ... is harmless since it is eliminated during pre-processing time. If we replace the first constraint with -a0min * (1.0 - a1max) + a2max * a3max < -95000.0, then Z3 also terminates quickly (also available online here).

a0min = Real('a0min')
a0max = Real('a0max')
a1min = Real('a1min')
a1max = Real('a1max')
a2min = Real('a2min')
a2max = Real('a2max')
a3min = Real('a3min')
a3max = Real('a3max')
volume = Real('volume')

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

s.add(-a0min * (1.0 - a1max) + a2max * a3max < -95000.0,
a0min >  0.0,
a0min < a0max,
a0max < 1000000.0,
a1min > 0.0,
a1min < a1max,
a1max < 1.0,
a2min > 1.0,
a2min < a2max,
a2max < 1000.0,
a3min > 1.0,
a3min < a3max,
a3max < 50.0,
(a0max - a0min) * (a1max -  a1min) * (a2max -  a2min) * (a3max - a3min) > 50000.0,
volume == (a0max - a0min) * (a1max -  a1min) * (a2max -  a2min) * (a3max - a3min))
print s.check()
print s.model()

BTW, when you replace everything with <=, nlsat still has to use real algebraic computations, but the change influences the nlsat search-tree, and it manages to find the solution before it gets stuck in a real algebraic number computation.

Here are the three places where nlsat gets "stuck" in the examples we tried/examined

• Real algebraic number computations (like your example). This will be fixed when we replace the current package with the new one.

• Polynomial factorization. The current algorithm implemented in Z3 is very inefficient. This can also be fixed.

• Subresultant computations. This one is tricky since as far as I know Z3 uses a very efficient implementation. The performance is similar to the implementation in state-of-the-art systems like Mathematica. This operation is used when Z3 is backtracking the search. The nice property is that we can prove that Z3 will always terminate using this approach. One alternative is to consider approximate methods that do not guarantee termination but are cheaper. Unfortunately, this is not a minor change like the previous two.