Разные времена выполнения для одного и того же ограничения, установленного с помощью Z3Py - PullRequest
Новая
       9

Разные времена выполнения для одного и того же ограничения, установленного с помощью Z3Py

0 голосов
/ 05 сентября 2018

Я кодирую проблему планирования с помощью решателя Z3 с помощью API z3py. Он работает довольно хорошо, за исключением того факта, что время выполнения решателя отличается во времени (иногда в 10/100 раз) при каждом запуске. Что я часто делаю, если решатель занимает слишком много времени, я просто убиваю запрос и перезапускаю его.

Мне кажется, что решатель (для каждого прогона) выбирает какой-то другой путь для поиска решения, что приводит к разным временам прогона.

Таким образом, мой вопрос заключается в том, могу ли я заставить решатель выбирать один и тот же (похожий) путь каждый раз для одного и того же набора ограничений (задачи)?

После некоторых исследований я наткнулся на концепцию установки случайного семени вручную. Это поможет мне? Есть ли еще информация, как это сделать с помощью Python API?

лучший

Jenny

1 Ответ

0 голосов
/ 05 сентября 2018

Нет, если вы заранее не знаете, какое случайное семя работает лучше всего. Однако вы действительно можете установить начальное число в сценариях регрессии, чтобы получить повторяемое поведение.

Проверяя вывод z3 -p, я вижу много возможностей: 

fixedpoint.spacer.random_seed (unsigned int) (default: 0)
sat.random_seed (unsigned int) (default: 0)
nlsat.seed (unsigned int) (default: 0)
fp.spacer.random_seed (unsigned int) (default: 0)
smt.random_seed (unsigned int) (default: 0)
sls.random_seed (unsigned int) (default: 0)

(NB. 0 ​​говорит «забрать» его самостоятельно для решателя.) Наиболее вероятный вариант - smt. или sat. one; возможно оба.

Вы можете установить эту опцию из Python API, используя функцию set_param, см .: https://z3prover.github.io/api/html/namespacez3py.html#a54767807c828563030b9400332f81d48

...