如何在Z3Py中声明变量作为数组索引的约束？ [英] How to declare constraints with variable as array index in Z3Py?

问题描述

假设x，y，z是int变量，A是一个矩阵，我想表达一个约束，例如：

Suppose x,y,z are int variables and A is a matrix, I want to express a constraint like:

z == A[x][y]

但是这会导致错误：
TypeError：对象不能解释为索引

However this leads to an error: TypeError: object cannot be interpreted as an index

执行此操作的正确方法是什么？

What would be the correct way to do this?

=

一个具体示例：

我想选择2个组合得分最高的项目，
，其中得分由每个项目的值和选择对上的奖励给出。
例如，
对应3个项目：a，b，c，其相关值为[1,2,1]，并且对（a，b）= 2时的奖励为（a，c）= 5，（b，c）= 3，最好的选择是（a，c），因为它的得分最高：1 +1 + 5 = 7。

I want to select 2 items with the best combination score, where the score is given by the value of each item and a bonus on the selection pair. For example, for 3 items: a, b, c with related value [1,2,1], and the bonus on pairs (a,b) = 2, (a,c)=5, (b,c) = 3, the best selection is (a,c), because it has the highest score: 1 + 1 + 5 = 7.

我的问题是如何代表选拔奖金的约束。
假设CHOICE [0]和CHOICE [1]是选择变量，B是奖励变量。
理想约束应为：

My question is how to represent the constraint of selection bonus. Suppose CHOICE[0] and CHOICE[1] are the selection variables and B is the bonus variable. The ideal constraint should be:

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

但这会导致TypeError：无法将对象解释为索引
我知道另一种方法是首先使用嵌套实例化CHOICE，然后表示B，但这对于大量数据实在是无效的。
任何专家都可以建议我一个更好的解决方案吗？

but it results in TypeError: object cannot be interpreted as an index I know another way is to use a nested for to instantiate first the CHOICE, then represent B, but this is really inefficient for large quantity of data. Could any expert suggest me a better solution please?

如果有人想玩玩具示例，则代码如下：

If someone wants to play a toy example, here's the code:

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"

推荐答案

解决此问题的最佳方法是实际上根本不使用数组，而只是创建整数变量。使用这种方法，最初发布的317x317项目问题实际上在我相对较旧的计算机上得到了大约40秒的解决：

Turns out the best way to deal with this problem is to actually not use arrays at all, but simply create integer variables. With this method, the 317x317 item problem originally posted actually gets solved in about 40 seconds on my relatively old computer:

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

请注意，实际的解决方案大约在一秒钟内即可找到！但是添加所有必需的约束将花费40秒的大部分时间。编码如下：

Note that the actual "solution" is found in about a second! But adding all the required constraints takes the bulk of the 40 seconds spent. Here's the encoding:

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可以解决此问题。当然，如果要最大化多个指标，则可以构造代码，以便重用大多数约束，从而分摊一次构建模型的成本，然后逐步进行优化以获得最佳性能。

I think this is as fast as it'll get with Z3 for this problem. Of course, if you want to maximize multiple metrics, then you can probably structure the code so that you can reuse most of the constraints, thus amortizing the cost of constructing the model just once, and incrementally optimizing afterwards for optimal performance.

这篇关于如何在Z3Py中声明变量作为数组索引的约束？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！