如何在Z3Py中將變量聲明爲數組索引？

假定x，y，z是INT變量，A是一個矩陣，我想表達類似的約束：如何在Z3Py中將變量聲明爲數組索引？

z == A[x][y]

然而，這會導致錯誤：類型錯誤：對象不能被解釋爲索引

這樣做的正確方法是什麼？

=======================

一個具體的例子：

我要選擇2項與最佳組合得分，其中分數由每個項目的值和選擇對上的獎金給出。例如，有3項：a，b，c與相關值[1,2,1] ）= 3，最好的選擇是（a，c），因爲它得分最高：1 + 1 + 5 = 7.

我的問題是如何表示選擇獎金的約束。假設CHOICE [0]和CHOICE [1]是選擇變量，B是獎金變量。理想約束應該是：

B = bonus[CHOICE[0]][CHOICE[1]]

但它導致類型錯誤：對象不能被解釋爲索引我知道另一種方式是使用一個嵌套的for實例第一選擇，然後代表B，但是這對於大量數據來說真的是效率低下。請問任何專家建議我一個更好的解決方案嗎？

如果有人願意玩玩具的例子，下面的代碼：

from z3 import * 

items = [0,1,2] 
value = [1,2,1] 
bonus = [[1,2,5], 
     [2,1,3], 
     [5,3,1]] 
choices = [0,1] 
# selection score 
SCORE = [ Int('SCORE_%s' % i) for i in choices ] 

# bonus 
B = Int('B') 

# final score 
metric = Int('metric') 

# selection variable 
CHOICE = [ Int('CHOICE_%s' % i) for i in choices ] 

# variable domain 
domain_choice = [ And(0 <= CHOICE[i], CHOICE[i] < len(items)) for i in choices ] 

# selection implication 
constraint_sel = [] 
for c in choices: 
    for i in items: 
     constraint_sel += [Implies(CHOICE[c] == i, SCORE[c] == value[i])] 

# choice not the same 
constraint_neq = [CHOICE[0] != CHOICE[1]] 

# bonus constraint. uncomment it to see the issue 
# constraint_b = [B == bonus[val(CHOICE[0])][val(CHOICE[1])]] 

# metric definition 
constraint_sumscore = [metric == sum([SCORE[i] for i in choices ]) + B] 

constraints = constraint_sumscore + constraint_sel + domain_choice + constraint_neq + constraint_b 

opt = Optimize() 
opt.add(constraints) 
opt.maximize(metric) 

s = [] 
if opt.check() == sat: 
    m = opt.model() 
    print [ m.evaluate(CHOICE[i]) for i in choices ] 
    print m.evaluate(metric) 
else: 
    print "failed to solve"

來源

2017-01-17 tong

原來對付這個問題的最好方法是實際不是在所有使用數組，而只是創建整型變量。使用這種方法，原本居然貼317x317項問題得到解決了約40秒我比較老的計算機上：

[ 0.01s] Data loaded 
[ 2.06s] Variables defined 
[37.90s] Constraints added 
[38.95s] Solved: 
c0  = 19 
c1  = 99 
maxVal = 27

注意實際的「解決方案」中關於第二個被發現！但是添加所有必需的約束需要花費40秒的大部分時間。這裏的編碼：

from z3 import * 
import sys 
import json 
import sys 
import time 

start = time.time() 

def tprint(s): 
    global start 
    now = time.time() 
    etime = now - start 
    print "[%ss] %s" % ('{0:5.2f}'.format(etime), s) 

# load data 
with open('data.json') as data_file: 
    dic = json.load(data_file) 
tprint("Data loaded") 

items  = dic['items'] 
valueVals = dic['value'] 
bonusVals = dic['bonusVals'] 

vals = [[Int("val_%d_%d" % (i, j)) for j in items if j > i] for i in items] 
tprint("Variables defined") 

opt = Optimize() 
for i in items: 
    for j in items: 
     if j > i: 
     opt.add(vals[i][j-i-1] == valueVals[i] + valueVals[j] + bonusVals[i][j]) 

c0, c1 = Ints('c0 c1') 
maxVal = Int('maxVal') 

opt.add(Or([Or([And(c0 == i, c1 == j, maxVal == vals[i][j-i-1]) for j in items if j > i]) for i in items])) 
tprint("Constraints added") 

opt.maximize(maxVal) 

r = opt.check() 
if r == unsat or r == unknown: 
    raise Z3Exception("Failed") 
tprint("Solved:") 
m = opt.model() 
print " c0  = %s" % m[c0] 
print " c1  = %s" % m[c1] 
print " maxVal = %s" % m[maxVal]

我認爲這是一樣快，它會得到與Z3這個問題。當然，如果您想要最大化多個指標，那麼您可以構建代碼，以便您可以重用大部分約束，從而將構建模型的成本分攤一次，然後逐步優化，以獲得最佳性能。

來源

2017-01-25 05:20:07

如何在Z3Py中將變量聲明爲數組索引？

回答

相關問題