时间戳

首页 > 解决方案 > z3 Optimize 不会在 Solver 产生结果的情况下产生结果

z3 - z3 Optimize 不会在 Solver 产生结果的情况下产生结果

问题描述

我正在编写一个函数来识别掉落的物体何时会撞到地面。它从y某个初始速度的某个高值开始y0。它考虑了重力加速度 (9.81m/s) 并试图确定dt在哪个y == 0。

代码（如下）可以很好地确定质量将在什么点撞击地面。但是，我必须找出我必须使用Solver而不是Optimize. （结果：）unknown。有人可以解释这个原因吗？不应该优化也能找到解决方案吗？（显然在这种情况下只有一个）

这是我的代码：

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

标签： z3z3py

解决方案

Z3 的优化器仅适用于线性约束。您有一个非线性项（由于涉及vy和的乘法dt），因此优化求解器放弃了Unknown。

然而，可满足性求解器可以处理非线性实际约束；因此给你一个模型没有问题。

有关 Z3 中非线性优化的更多信息，只需搜索该术语。你会看到很多人问类似的问题！这是一个例子：z3Opt 使用 qfnra-nlsat 优化非线性函数

（请注意，与纯可满足性相比，非线性优化对于实数来说是一个非常困难的问题。因此，这不仅仅是“尚未实现它”的问题。）

推荐阅读