Optimize () в z3py не находит оптимальных решений - PullRequest
Новая
       29

Optimize () в z3py не находит оптимальных решений

2 голосов
/ 27 июня 2019

Я пытаюсь использовать z3py в качестве решателя оптимизации, чтобы максимизировать объем кубоида, вырезанного из листа бумаги.Python API предоставляет объект Optimize (), но его использование кажется ненадежным, давая мне решения, которые явно неточны.

Я пытался использовать h = opt.maximise с последующим opt.upper(h), а также просто проверять модель, а также определять объем кубоида перед добавлением его в модель v = w*b*l и после, а такжекак установка цели как w*b*l вместо v.Никто из них не дал мне ничего похожего на хорошее решение. 

from z3 import *
l = Real("l")
w = Real("w")
b = Real("b")
v = Real("v")
opt = Optimize()
width = 63.6
height = 51

opt.add(b+l <= width)
opt.add(w+b+w+l+w <= height)
opt.add(w > 0)
opt.add(b > 0)
opt.add(l > 0)
opt.add(v == w*b*l)
opt.maximize(w * b * l)
# h = opt.maximize(v)


print(opt.check())
# print(opt.upper(h))
print(opt.model())

Выходы: 

unknown
[w = 1, b = 1, l = 47, v = 47]

Это определенно не максимум.Установка всех значений на 10 дает большее решение, которое удовлетворяет ограничениям.

1 Ответ

3 голосов
/ 27 июня 2019

Оптимизатор Z3 не обрабатывает нелинейные задачи. И действительно, именно поэтому он печатает unknown. Когда вы видите, что check возвращает unknown, это точно означает, что: Z3 не знает, является ли проблема выполнимой или нет, не говоря уже о том, нашел ли она оптимальное решение.

Если вы добавите: 

print(opt.reason_unknown())

после звонка на check вы увидите: 

(incomplete (theory arithmetic))

В этих случаях вызов model вернет некоторый промежуточный результат z3, полученный при работе над проблемой, но ни в коем случае он не будет гарантированно оптимальным.

Ваша проблема нелинейная, потому что вы умножаете переменные. (w, b и l.) Z3 может решать нелинейные задачи выполнимости по реалам, но не задач оптимизации. См., Например, здесь: z3Opt оптимизирует нелинейную функцию, используя qfnra-nlsat

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

...