Ускорение оптимизатора z3 - PullRequest
1 голос
/ 09 апреля 2020

У меня есть набор линейных ограничений, определенных для набора реальных параметров. Цель состоит в том, чтобы найти решение параметров, которое удовлетворяет максимальному числу этих ограничений. Я использую оптимизатор в z3, но он очень медленный. Количество ограничений равно 100, а количество параметров равно 9, что не является большим числом. Я использую следующий код:

from z3 import *
s = Optimize()
W = RealVector('w', 9)
s.add(And([And(w >= -100, w <= 100) for w in W]))

**Add soft constraints from a text file

out = s.check()

Ниже приведен пример мягких ограничений, каждый с весом 1, которые добавляются к проблеме:

w__0 + 7*w__1 + 181*w__2 + 84*w__3 + 21*w__4 + 192*w__5 + 36*w__6 + 59*w__7 + 51*w__8 > 0

w__0 + 2*w__1 + 127*w__2 + 58*w__3 + 24*w__4 + 275*w__5 + 28*w__6 + 160*w__7 + 25*w__8 < 0

w__0 + 11*w__1 + 138*w__2 + 76*w__3 + 0*w__4 + 0*w__5 + 33*w__6 + 42*w__7 + 35*w__8 < 0

w__0 + 2*w__1 + 81*w__2 + 60*w__3 + 22*w__4 + 0*w__5 + 28*w__6 + 29*w__7 + 25*w__8 < 0

w__0 + 0*w__1 + 84*w__2 + 82*w__3 + 31*w__4 + 125*w__5 + 38*w__6 + 23*w__7 + 23*w__8 < 0

w__0 + 9*w__1 + 140*w__2 + 94*w__3 + 0*w__4 + 0*w__5 + 33*w__6 + 73*w__7 + 45*w__8 > 0

w__0 + 8*w__1 + 197*w__2 + 74*w__3 + 0*w__4 + 0*w__5 + 26*w__6 + 119*w__7 + 39*w__8 > 0

w__0 + 8*w__1 + 120*w__2 + 0*w__3 + 0*w__4 + 0*w__5 + 30*w__6 + 18*w__7 + 38*w__8 > 0

w__0 + 7*w__1 + 161*w__2 + 86*w__3 + 0*w__4 + 0*w__5 + 30*w__6 + 17*w__7 + 47*w__8 > 0

w__0 + 4*w__1 + 120*w__2 + 68*w__3 + 0*w__4 + 0*w__5 + 30*w__6 + 71*w__7 + 34*w__8 < 0

w__0 + 7*w__1 + 187*w__2 + 50*w__3 + 33*w__4 + 392*w__5 + 34*w__6 + 83*w__7 + 34*w__8 > 0

w__0 + 2*w__1 + 87*w__2 + 0*w__3 + 23*w__4 + 0*w__5 + 29*w__6 + 77*w__7 + 25*w__8 < 0

w__0 + 1*w__1 + 97*w__2 + 68*w__3 + 21*w__4 + 0*w__5 + 27*w__6 + 110*w__7 + 22*w__8 < 0

w__0 + 4*w__1 + 123*w__2 + 80*w__3 + 15*w__4 + 176*w__5 + 32*w__6 + 44*w__7 + 34*w__8 < 0

w__0 + 6*w__1 + 195*w__2 + 70*w__3 + 0*w__4 + 0*w__5 + 31*w__6 + 33*w__7 + 31*w__8 > 0

w__0 + 0*w__1 + 101*w__2 + 64*w__3 + 17*w__4 + 0*w__5 + 21*w__6 + 25*w__7 + 21*w__8 < 0

w__0 + 12*w__1 + 92*w__2 + 62*w__3 + 7*w__4 + 258*w__5 + 28*w__6 + 93*w__7 + 44*w__8 > 0

w__0 + 1*w__1 + 88*w__2 + 62*w__3 + 24*w__4 + 44*w__5 + 30*w__6 + 42*w__7 + 23*w__8 < 0

Я знаю, что производительность решения будет зависеть от характера проблемы, но при 100 таких ограничениях вычисления go навсегда. Есть ли дополнительная опция, которую я могу использовать, чтобы сделать это быстрее?

Я также сам реализовал алгоритм fu-malik, извлекая ядро, даже при том, что оно действительно медленное.

...