Z3Pyで変数を配列のインデックスとして宣言するにはどうすればいいですか？

Question

と仮定X、Y、Zは整数変数であり、Aは行列であり、Iは次のように制約を表現したい：

z == A[x][y] 

しかし、これはエラーにつながる： 例外TypeError：オブジェクトインデックス

として解釈することはできません

これを行う正しい方法は何でしょうか？

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

具体的な例：私は最高の組み合わせスコアを持つ2つの項目を選択したい

、 ここでスコアは各項目の値と選択ペアのボーナスによって与えられます。 例：3つのアイテム：a、b、c、関連値[1,2,1]、ペア（a、b）= 2、（a、c）= 5、（b、c）のボーナス）= 3、最高の選択肢は（a、c）です。これは1 + 1 + 5 = 7のスコアが最も高いためです。

私の質問は選択ボーナスの制約をどのように表現するかです。 CHOICE [0]とCHOICE [1]が選択変数であり、Bがボーナス変数であるとします。

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

それはTypeError例外を生じる： 理想的制約がなければならないオブジェクトを指標として解釈することができない Iは、別の方法は、その後、最初の選択肢をインスタンス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" 

Answer 1

は、この問題に対処するための最良の方法は、実際にすべての配列を使用しないで、単に整数の変数を作成することですが判明。実際の「ソリューション」は1秒程度で発見されていること

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

注：この方法では、もともと掲示317x317項目の問題は、実際に私の比較的古いコンピュータ上で約40秒で解決します！しかし、すべての必要な制約を加えることは、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でこの問題を解決するのと同じくらい速いと思います。もちろん、複数のメトリックを最大化したい場合は、のほとんどの制約を再利用できるようにコードを構造化して、モデルを1回構築するコストを償却し、後で最適なパフォーマンスを得るために徐々に最適化します。