z3 Оптимизация не дает результата, когда Солвер выдает результат - PullRequest
Новая
       6

z3 Оптимизация не дает результата, когда Солвер выдает результат

0 голосов
/ 13 мая 2018

Я пишу функцию, которая будет определять, когда упавший объект упадет на землю.Он начинается с некоторого значения высоты y с некоторой начальной скоростью y0.Он учитывает ускорение силы тяжести (9,81 м / с) и пытается определить 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())

1 Ответ

0 голосов
/ 13 мая 2018

Оптимизатор Z3 работает только с линейными ограничениями. У вас есть нелинейный член (из-за умножения, включающего vy и dt), и, следовательно, оптимизатор решает с Unknown.

Однако решатель выполнимости может иметь дело с нелинейными вещественными ограничениями; и, следовательно, без проблем дает вам модель.

Чтобы узнать больше о нелинейной оптимизации в Z3, просто найдите этот термин. Вы увидите много людей, задающих подобные вопросы! Вот один пример: z3Opt оптимизирует нелинейную функцию, используя qfnra-nlsat

(Обратите внимание, что нелинейная оптимизация представляет собой значительно более сложную проблему для реальных, а не просто удовлетворяемости. Таким образом, это не просто вопрос "не реализовал ее пока".)

...