Найти максимальное значение переменной с учетом ограничений в z3py - PullRequest
Новая
       34

Найти максимальное значение переменной с учетом ограничений в z3py

1 голос
/ 12 апреля 2020

Например, учитывая следующие 4 ограничения, a и x равны ints, b равны array, карты int - int: 

a >= 0
b[0] == 10
x == 0
b[x] >= a

find_max(a) => 10
find_min(a) => 0

Может ли z3py сделать что-то подобное?

1 Ответ

2 голосов
/ 12 апреля 2020

Да, конечно.

Вы можете сделать это постепенно, с помощью нескольких поисков оптимизации с одной целью, или использовать более эффективный в штучной упаковке ( aka Multi-Independent ) комбинация, предложенная z3 для работы с многоцелевой оптимизацией.

Определение 4.6.3. (Множественно независимый OMT [LAK + 14, BP14, BPF15, ST15b, ST15c]). Пусть <φ,O> - многоцелевая проблема OMT, где φ - это основная формула SMT, а O = {obj_1 , ..., obj_N} - это отсортированный список N целевых функций. Мы называем множественную независимую задачу ОМТ , , то есть, проблему OMT в штучной упаковке [BP14, BPF15] , проблему поиска за один раз набора моделей {M_1, ...,M_N}, таких что каждая M_i делает obj_i минимум по общей формуле φ.

Замечание 4.6.3. Решение множественной независимой задачи ОМТ <φ, {obj_1, ..., obj_N }> похоже на самостоятельное решение N одноцелевые задачи ОМТ <φ, obj_1>, ..., <φ, obj_N>. Тем не менее, первый позволяет факторизовать поиск и, таким образом, получить значительное повышение производительности по сравнению с последним подходом [LAK + 14, BP14, ST15c].

[ source, pag. 104 ]

Пример: 

from z3 import *

a = Int('a')
x = Int('x')
b = Array('I', IntSort(), IntSort())

opt = Optimize()

opt.add(a >= 0)
opt.add(x == 0)
opt.add(Select(b, 0) == 10)
opt.add(Select(b, x) >= a)

obj1 = opt.maximize(a)
obj2 = opt.minimize(a)

opt.set('priority', 'box')   # Setting Boxed Multi-Objective Optimization

is_sat = opt.check()
assert is_sat

print("Max(a): " + str(obj1.value()))
print("Min(a): " + str(obj2.value()))

Вывод: 

~$ python test.py 
Max(a): 10
Min(a): 0

См. Публикации в топи c как, например,

1. Николай Бьорнер и Ан-Дунг Фан. νZ - максимальное удовлетворение Z3. в Pro c Международный симпозиум по Symboli c Вычисления в Software Science, Gammart, Тунис, декабрь 2014 г. Материалы EasyChair по вычислительной технике (EPi C). [PDF]

2. Николай Бьорнер, Ан-Дунг Фан и Ларс Флекенштейн. Z3 - Оптимизирующий SMT Solver . В Pro c. ТАКАС, объем 9035 LNCS. Springer, 2015. [Springer] [[PDF]

...