Могу ли я получить решение с использованием «тайм-аута» при использовании Optimize.minimize ()? - PullRequest
Новая
       16

Могу ли я получить решение с использованием «тайм-аута» при использовании Optimize.minimize ()?

1 голос
/ 26 марта 2019

Я пытаюсь минимизировать переменную, но z3 занимает много времени, чтобы дать мне решение.

И я хотел бы знать, возможно ли найти решение при срабатывании тайм-аута.

Если да, как я могу это сделать?

Спасибо заранее!

1 Ответ

2 голосов
/ 27 марта 2019

Если под «решением» вы подразумеваете последнее приближение оптимального значения, то вы можете иметь возможность его получить, при условии, что используемый алгоритм оптимизации находит какое-либо промежуточное решениепо пути. (Некоторые алгоритмы оптимизации - например, maxres - не находят промежуточного решения).

Пример: 

import z3

o = z3.Optimize()
o.add(...very hard problem...)
cf = z3.Int('cf')
o.add(cf = ...)
obj = o.minimize(cf)
o.set(timeout=...)
res = o.check()
print(res)
print(obj.upper())

Даже когда res = unknown из-за тайм-аута, экземпляр objective содержит самое последнее приближение оптимального значения, найденного z3 до тайм-аута.

К сожалению, я не уверен, является ли онТакже возможно получить соответствующую субоптимальную модель с помощью o.model() (или любым другим способом).

Для OptiMathSAT я покажу, как получить последнее приближение оптимального значения и соответствующей модели в модульном тесте timeout.py.

...