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

#z3 #z3py #optimathsat

Вопрос:

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

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

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

Заранее спасибо!

Ответ №1:

Если под «решением» вы подразумеваете последнее приближение оптимального значения, то вы можете получить его при условии, что используемый алгоритм оптимизации найдет какое-либо промежуточное решение по пути. (Некоторые алгоритмы оптимизации — например, 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 .

1. Спасибо за помощь! Но я получаю минус бесконечный (-1 * oo) Вы знаете, почему?

2. Я пытаюсь минимизировать

3. Другой вопрос: могу ли я вместо использования тайм-аута для выхода использовать условие if? Если да, то как я могу это сделать?

4. Я предполагаю, что это нижняя граница — Если minimeze становится ниже определенного предела, выходите из решателя

5. @AndreOliveira При минимизации lower обновляется при неудовлетворительных шагах двоичного поиска и upper обновляется при удовлетворительных шагах линейного / двоичного поиска , поэтому вам следует проверить значение obj.upper() . Я ничего не нашел в z3 API для выполнения другой вещи, о которой вы спрашивали. Было бы довольно тривиально сделать это с помощью OptiMathSAT , используя либо параметр opt.abort_interval , либо опцию opt.abort_tolerance , либо написав пользовательскую msat_termination_test функцию обратного вызова.