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.