Есть ли способ манипулировать верхними границами в z3? - PullRequest
Новая
       9

Есть ли способ манипулировать верхними границами в z3?

0 голосов
/ 06 февраля 2019

Я пытаюсь минимизировать значения, используя Z3.Я установил verbose в 0 и заметил, что Z3 находит верхнюю границу и начинает работать оттуда, чтобы минимизировать значение.Пример: 

(optimize:check-sat)
(optimize:sat)
(optsmt upper bound: 3460)
(optsmt upper bound: 3455)
(optsmt upper bound: 3445)
(optsmt upper bound: 2430)
(optsmt upper bound: 2425)
(optsmt upper bound: 2325)
(optsmt upper bound: 2155)
(optsmt upper bound: 2150)
(optsmt upper bound: 2145)
(optsmt upper bound: 2135)
(optsmt upper bound: 2125)
(optsmt upper bound: 2055)
(optsmt upper bound: 2045)
(optsmt upper bound: 155)
(optsmt upper bound: 135)
(optsmt upper bound: 115)
(optsmt upper bound: 15)
(optsmt upper bound: 10)

Я хочу знать, есть ли способ установить верхнюю границу на гораздо более низкий уровень, чтобы получить более быстрый вывод.

1 Ответ

0 голосов
/ 06 февраля 2019

Если вы знаете, что есть ограничение, почему бы просто не указать это как дополнительное утверждение:

(assert (< goal 200))

Конечно, это не гарантирует ускорения;и вообще может пропустить оптимальную точку, если вы ошиблись.Но попробовать это просто.

В общем, чем больше информации вы предоставляете решателю, тем больше шансов, что он быстрее сходится.

Обратите внимание, что z3 недействительно «искать» во время оптимизации. Вместо этого он алгоритмически определяет и ограничивает границы. Так что на самом деле нет «начального» значения. Дополнительные ссылки о том, как оптимизация работает в z3, смотрите в этом превосходном недавнем ответе Патрика: Чтотеория Z3 оптимизирует максимальную и минимальную функциональность?

...