Как объявить ограничения с переменной как индекс массива в Z3Py?

Question

Пусть х, у, г являются INT переменных и А представляет собой матрицу, я хочу выразить ограничение как:

z == A[x][y] 

Однако это приводит к ошибке: Ошибка типа: объект не может быть истолковано как индекс

Что было бы правильным способом сделать это?

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

Конкретный пример:

Я хочу, чтобы выбрать 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: объект не может быть истолкован как индекс я знаю другой способ заключается в использовании вложенного для создания экземпляра первого выбора, затем представляет 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

Оказывается, лучший способ справиться с этой проблемой, является на самом деле не использовать массивы на всех, а просто создавать целые переменные. С помощью этого метода, проблема 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 для этой проблемы. Конечно, если вы хотите максимизировать несколько показателей, то вы, вероятно, можете структурировать код, чтобы вы могли использовать большое количество ограничений, таким образом, амортизируя затраты на построение модели только один раз и постепенно оптимизируя их для оптимальной производительности.