Question

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

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

Дополнительный вопрос, можете ли вы установить для z3 случайное значение? восхождение на гору или он всегда выполняет полный поиск?

Patrick Trentin · Answer 1 · 25 марта 2020

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

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

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

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

Возможный обходной путь. (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:

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

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

Пример: Следующий пример - timeout.py unit-test, содержащийся в моем omt_python_examples github-репозитории, в котором есть несколько примеров использования Python API-интерфейса 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!
  ...

alias · Answer 2 · 25 марта 2020

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

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

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

Есть несколько других вопросов, связанных с переполнением стека. Ищите «optimize» и «timeout».

Ваша лучшая ставка

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

Укажите свою проблему
Попросите модель. Если модели нет, ответьте unsat. Выйти.
Сохранить текущую модель как "лучшую на данный момент"
Вне времени? Верните модель, которая у вас есть, как "лучшую на данный момент". Вы закончили.
Еще есть время?

5a. Рассчитайте «стоимость» этой модели. т. е. метри c, которую вы пытаетесь минимизировать или максимизировать. Если вы храните стоимость как переменную в вашей модели, вы можете просто запросить ее значение из модели.

5b. Утвердите новое ограничение, сказав, что стоимость должна быть ниже, чем стоимость текущей модели. (Или выше, если вы максимизируете.) В зависимости от того, насколько вы хотите получить, вы можете захотеть «удвоить» функцию стоимости или внедрить некоторый вид бинарного поиска, чтобы быстрее сходиться по значению. Но все это действительно зависит от точных деталей проблемы.

5 c. Спросите новую модель. Если unsat, верните последнюю полученную модель как «оптимальную». В противном случае повторите с шага 3.

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

Резюме

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

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

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

Пожалуйста, войдите или зарегистрируйтесь чтобы ответить на этот вопрос.

Ответы [ 2 ]

Пожалуйста, войдите или зарегистрируйтесь что бы добавить комментарий.

Ваша лучшая ставка

Резюме

Пожалуйста, войдите или зарегистрируйтесь что бы добавить комментарий.

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

Пожалуйста, войдите или зарегистрируйтесь чтобы ответить на этот вопрос.

Ответы [ 2 ]

Пожалуйста, войдите или зарегистрируйтесь что бы добавить комментарий.

Ваша лучшая ставка

Резюме

Пожалуйста, войдите или зарегистрируйтесь что бы добавить комментарий.

Похожие темы