CODEWITHSUNDEEP
z3z3py
stklik
stklik

Reputation: 844

z3 Optimize does not produce result where Solver produces one

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())

Upvotes: 2

Views: 1176

Answers (1)

alias
alias

Reputation: 30428

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.")

Upvotes: 3

Related Questions