Тайм-аут для Z3 Optimize

Question

Тайм-аут для Z3 Optimize

Как установить тайм-аут для оптимизатора z3, чтобы он давал вам наиболее известное решение, когда время истекает?

from z3 import *
s = Optimize()
# Hard Problem
print(s.check())
print(s.model())

Последующий вопрос: можете ли вы настроить z3 на случайное восхождение на холм или он всегда выполняет полный поиск?

5

optimization timeout z3 z3py optimathsat

Источник

user6844327 25 мар '20 в 03:59

2 ответа

Решение

В общем, Levent Erkok прав, когда заявляет, что решатель OMT не дает никаких гарантий того, что решение будет доступно в конце поиска оптимизации, когда он прерываетсяtimeout сигнал.

Решатель OMT может искать оптимальное решение одним из двух способов:

начиная с исходной модели формулы и пытаясь улучшить значение целевой функции; Это случай стандартного подхода OMT, который перечисляет ряд частично оптимизированных решений, пока не будет найдено оптимальное.
начиная с более чем оптимального, неудовлетворительного назначения и постепенно ослабляя такое назначение, пока оно не приведет к оптимальному решению; AFAIK, это только случай механизма максимального разрешения для решения проблем MaxSMT.

Когда решающая программа OMT использует технику оптимизации, которая попадает в первую категорию, тогда возможно получить наиболее известное решение, когда для него не хватит времени, при условии, что решающая программа OMT сохранит его в безопасном месте во время поиска оптимизации. Это не относится ко второму механизму MaxRes (см. Этот вопрос / ответ).

Возможный обходной путь. (CAVEAT: я не тестировал это) z3 отслеживает lower а также upperграница целевой функции по поиску оптимизации. При сворачиванииupperграница соответствует значению целевой функции в последнем частичном решении, найденном решателем OMT (двойное для максимизации). После появления сигнала тайм-аута при минимизации (или максимизации)obj экземпляр получен из minimize() (соотв. maximize()), должно быть возможно получить последнее приближение v оптимального значения obj позвонив obj.upper() (соотв. obj.lower()). Предполагая, что такое значениеv отличается от +oo (соотв. -oo), можно постепенно изучать ограничение вида cost = v и выполнить инкрементную SMT-проверку выполнимости, чтобы восстановить модель, соответствующую субоптимальному решению, для которого z3.

OptiMathSAT- это одна из решателей OMT, которая хранит в надежном месте последнее решение, с которым сталкивается во время поиска по оптимизации. Это позволяет легко достичь того, что вы хотите делать.

Есть два типа timeout сигналы в OptiMathSAT:

жесткий тайм-аут: как толькоtimeoutсрабатывает, поиск оптимизации немедленно останавливается; если решатель OMT нашел какое-либо решение, результат поиска оптимизации (доступен черезmsat_objective_result(env, obj)) является MSAT_OPT_SAT_PARTIALи модель, соответствующая последнему субоптимальному решению, может быть извлечена и распечатана; если вместо этого решающая программа OMT не нашла никакого решения, результатом поиска оптимизации будетMSAT_UNKNOWN и модель недоступна.
мягкий тайм-аут: еслиtimeoutсрабатывает после того, как решатель OMT нашел какое-либо решение, затем поиск немедленно останавливается, как в случае жесткого тайм-аута. В противном случаеtimeoutне игнорируется, пока ОМТ решатель находит одно решение.

Тип timeout сигнал можно установить с помощью опции opt.soft_timeout=[true|false].

Пример: Следующий пример - это модульный тест timeout.py, содержащийся в моем репозитории github omt_python_examples, который содержит ряд примеров использования интерфейса API Python дляOptiMathSAT.

"""
timeout unit-test.
"""

###
### SETUP PATHS
###

import os
import sys

BASE_DIR = os.path.dirname(os.path.abspath(__file__))
INCLUDE_DIR = os.path.join(BASE_DIR, '..', 'include')
LIB_DIR = os.path.join(BASE_DIR, '..', 'lib')
sys.path.append(INCLUDE_DIR)
sys.path.append(LIB_DIR)

from wrapper import * # pylint: disable=unused-wildcard-import,wildcard-import

###
### DATA
###

OPTIONS = {
    "model_generation" : "true",      # !IMPORTANT!
    "opt.soft_timeout" : "false",
    "opt.verbose"      : "true",
}

###
### TIMEOUT UNIT-TEST
###

with create_config(OPTIONS) as cfg:
    with create_env(cfg) as env:

        # Load Hard Problem from file
        with open(os.path.join(BASE_DIR, 'smt2', 'bacp-19.smt2'), 'r') as f:
            TERM = msat_from_smtlib2(env, f.read())
            assert not MSAT_ERROR_TERM(TERM)
            msat_assert_formula(env, TERM)

        # Impose a timeout of 3.0 seconds
        CALLBACK = Timer(3.0)
        msat_set_termination_test(env, CALLBACK)

        with create_minimize(env, "objective", lower="23", upper="100") as obj:
            assert_objective(env, obj)

            solve(env)                    # optimization search until timeout
            get_objectives_pretty(env)    # print latest range of optimization search

            load_model(env, obj)          # retrieve sub-optimal model
            dump_model(env)               # print sub-optimal model

Это подробный результат поиска по оптимизации:

# obj(.cost_0) := objective
# obj(.cost_0) - search start: [ 23, 100 ]
# obj(.cost_0) - linear step: 1
# obj(.cost_0) -  new: 46
# obj(.cost_0) -  update upper: [ 23, 46 ]
# obj(.cost_0) - linear step: 2
# obj(.cost_0) -  new: 130/3
# obj(.cost_0) -  update upper: [ 23, 130/3 ]
# obj(.cost_0) - linear step: 3
# obj(.cost_0) -  new: 40
# obj(.cost_0) -  update upper: [ 23, 40 ]
# obj(.cost_0) - linear step: 4
# obj(.cost_0) -  new: 119/3
# obj(.cost_0) -  update upper: [ 23, 119/3 ]
# obj(.cost_0) - linear step: 5
# obj(.cost_0) -  new: 112/3
# obj(.cost_0) -  update upper: [ 23, 112/3 ]
# obj(.cost_0) - linear step: 6
# obj(.cost_0) -  new: 104/3
# obj(.cost_0) -  update upper: [ 23, 104/3 ]
# obj(.cost_0) - linear step: 7
# obj(.cost_0) -  new: 34
# obj(.cost_0) -  update upper: [ 23, 34 ]
# obj(.cost_0) - linear step: 8
# obj(.cost_0) -  new: 133/4
# obj(.cost_0) -  update upper: [ 23, 133/4 ]
# obj(.cost_0) - linear step: 9
# obj(.cost_0) -  new: 161/5
# obj(.cost_0) -  update upper: [ 23, 161/5 ]
# obj(.cost_0) - linear step: 10
# obj(.cost_0) -  new: 32
# obj(.cost_0) -  update upper: [ 23, 32 ]
# obj(.cost_0) - linear step: 11
# obj(.cost_0) -  new: 158/5
# obj(.cost_0) -  update upper: [ 23, 158/5 ]
# obj(.cost_0) - linear step: 12
# obj(.cost_0) -  new: 247/8
# obj(.cost_0) -  update upper: [ 23, 247/8 ]
# obj(.cost_0) - linear step: 13
# obj(.cost_0) -  new: 123/4
# obj(.cost_0) -  update upper: [ 23, 123/4 ]
# obj(.cost_0) - linear step: 14
# obj(.cost_0) -  new: 61/2
# obj(.cost_0) -  update upper: [ 23, 61/2 ]
# obj(.cost_0) - linear step: 15
unknown                                       ;; <== Timeout!
(objectives
  (objective 61/2), partial search, range: [ 23, 61/2 ]
)                                             ;; sub-optimal value, latest search interval

  course_load__ARRAY__1 : 9                   ;; and the corresponding sub-optimal model
  course_load__ARRAY__2 : 1
  course_load__ARRAY__3 : 2
  course_load__ARRAY__4 : 10
  course_load__ARRAY__5 : 3
  course_load__ARRAY__6 : 4
  course_load__ARRAY__7 : 1
  course_load__ARRAY__8 : 10
  course_load__ARRAY__9 : 4
  course_load__ARRAY__10 : 1
  course_load__ARRAY__11 : 1
  course_load__ARRAY__12 : 5
  course_load__ARRAY__13 : 10
  course_load__ARRAY__14 : 9
  course_load__ARRAY__15 : 1
  ...
  ;; the sub-optimal model is pretty long, it has been cut to fit this answer!
  ...

4

Источник

user6024122 25 мар '20 в 14:20

Другие вопросы по тегам optimization timeout z3 z3py optimathsat

user936310 25 мар '20 в 04:48 2020-03-25 04:48 · Accepted Answer · 2020-03-25 04:48

Длинный ответ, короткий, нельзя. Оптимизатор работает не так. То есть он не находит решения, а затем пытается его улучшить. Если вы прервете его или установите тайм-аут, когда таймер истечет, у него может даже не быть удовлетворительного решения, не говоря уже об "улучшенном" каким-либо образом. Подробности см. В документе по оптимизации: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-nuz.pdf

Однако верно, что z3 действительно отслеживает границы переменных для числовых величин. Возможно, вам удастся извлечь их, хотя в целом у вас не будет возможности узнать, какие значения из этих интервалов вам нужно выбрать, чтобы получить удовлетворительное решение для общей проблемы. См. Этот ответ для обсуждения: возможно ли получить достоверную информацию о диапазоне при использовании ограничения SMT с Z3

На этом форуме часто возникают такие "восхождения в гору". Ответ прост: оптимизатор z3 работает не так. Некоторые предыдущие вопросы таким образом:

Есть несколько других вопросов по этим строкам в stack-overflow. Ищите "оптимизировать" и "тайм-аут".

Ваш лучший выбор

Это теоретическая сторона дела. На практике я считаю, что лучший подход к решению проблемы такого рода - вообще не использовать оптимизатор. Вместо этого сделайте следующее:

Укажите свою проблему
Спросите модель. Если модели нет, ответьтеunsat. Уволиться.
Сохраняйте текущую модель как "лучшую на данный момент"
Вне времени? Верните имеющуюся у вас модель как "лучшую на данный момент". Вы сделали.
Еще есть время?
5а. Вычислите "стоимость" этой модели. т. е. показатель, который вы пытаетесь минимизировать или максимизировать. Если вы храните стоимость в качестве переменной в своей модели, вы можете просто запросить ее значение из модели.
5б. Утвердите новое ограничение, согласно которому стоимость должна быть ниже, чем стоимость текущей модели. (Или выше, если вы максимизируете.) В зависимости от того, насколько хорошо вы хотите получить, вы можете захотеть "удвоить" функцию стоимости или реализовать какой-то бинарный поиск, чтобы быстрее найти значение. Но все это действительно зависит от точных деталей проблемы.
5c. Спросите новую модель. Еслиunsat, верните последнюю полученную модель как "оптимальную". В противном случае повторите с шага 3.

Я считаю, что это наиболее практичный подход для оптимизации временных ограничений в z3. Это дает вам полный контроль над тем, сколько раз выполнять итерацию, и направлять поиск любым удобным для вас способом. (Например, вы можете запросить различные переменные для каждой модели и направить поиск, сказав "найди мне более крупнуюx, или меньший yи т. д., вместо того, чтобы смотреть только на одну метрику.) Надеюсь, что это имеет смысл.

Резюме

Обратите внимание, что решающая программа SMT может работать так, как вы описываете, т. Е. Давать вам оптимальное на данный момент решение, когда истекает время ожидания. Просто оптимизатор z3 так не работает. Для z3 я обнаружил, что итерационный цикл, описанный выше, является наиболее практичным решением такого рода оптимизации на основе тайм-аута.

Вы также можете посмотреть OptiMathSAT ( http://optimathsat.disi.unitn.it/), который может предложить лучшие возможности в этом отношении. @ Патрик Трентен, который часто читает этот форум, является экспертом в этом вопросе и может высказать отдельное мнение относительно его использования.