I'm writing a function that will identify when a dropped object will hit the ground. It starts at some highness-value y with some initial velocity y0. It takes gravity acceleration (9.81m/s) into account and tries to determine a dt at which y == 0.
The code (below) works fine to determine at what point the mass will hit the ground. However, I had to find out the hard way that I have to use Solver and not Optimize. (result: unknown). Can somebody explain the reason for this?
Shouldn't optimize also be able to find a solution? (obviously there is only one in this scenario)
Here's my code:
from z3 import *
vy0, y0 = Reals("vy0 y0") # initial velocity, initial position
dt, vy, y = Reals("dt vy y") # time(s), acceleration, velocity, position
solver = Solver() # Optmize doesn't work, but why?
solver.add(vy0 == 0)
solver.add(y0 == 3)
solver.add(dt >= 0) # time needs to be positive
solver.add(vy == vy0 - 9.81 * dt) # the velocity is initial - acceleration * time
solver.add(y == y0 + vy/2 * dt) # the position changes with the velocity (s = v/2 * t)
solver.add(y == 0)
# solver.minimize(dt) # Optmize doesn't work, but why?
print(solver.check())
print(solver.model())
Z3's optimizer only works with linear constraints. You have a non-linear term (due to the multiplication involving vy and dt), and thus the optimizing solver gives up with Unknown.
The satisfiability solver, however, can deal with non-linear real constraints; and hence has no problem giving you a model.
For more on non-linear optimization in Z3, simply search for that term. You'll see many folks asking similar questions! Here's one example: z3Opt optimize non-linear function using qfnra-nlsat
(Note that nonlinear optimization is a significantly harder problem for reals as opposed to pure satisfiability. So, it's not just a matter of "not having implemented it yet.")