と仮定X、Y、Zは整数変数であり、Aは行列であり、Iは次のように制約を表現したい:Z3Pyで変数を配列のインデックスとして宣言するにはどうすればいいですか?
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"