z3py：符号表达式不能转换为具体的布尔值

Question

我在用 z3py 定义 SMT 问题中的 objective 函数时遇到问题。

长话短说，我必须优化宽度固定但高度可变的板内较小块的放置。

我有一个坐标数组（由一个长度为 2 的整数数组表示）和一个整数列表（表示要放置的块的高度）。

    # [x,y] list of integer variables
    P = [[Int("x_%s" % (i + 1)), Int("y_%s" % (i + 1))]
         for i in range(blocks)]
    
    y = [int(b) for a, b in data[2:]]

我这样定义 objective 函数：

    obj= Int(max([P[i][1] + y[i] for i in range(blocks)]))

它根据块的起始坐标及其高度计算板的最大高度。我知道它可能会更好，但我认为即使定义不同，问题也会相同。

无论如何，如果我运行我的代码，objective 函数行会出现以下错误：

" raise Z3Exception("符号表达式不能转换为具体的布尔值。") "

在调试时我看到 P[i][1] 给出了一个错误，我认为这是因为程序读取“y_i + 3”（例如）并且他们不能相加。

要点是：很明显objective函数依赖于问题的变量，那么我怎样才能摆脱这个错误呢？是否还有另一个地方我应该定义 objective 函数，以便它在执行任何操作之前等待实例化 P 数组？

完整代码：

    from z3 import *
    from math import ceil
    
    
    width = 8
    blocks = 4
    x = [3,3,5,5]
    y = [3,5,3,5]
    
    height = ceil(sum([x[i] * y[i] for i in range(blocks)]) / width) + 1
    
    # [blocks x 2] list of integer variables
    P = [[Int("x_%s" % (i + 1)), Int("y_%s" % (i + 1))]
         for i in range(blocks)]
    
    # value/ domain constraint
    values = [And(0 <= P[i][0], P[i][0] <= width - 1, 0 <= P[i][1], P[i][1] <= height - 1)
              for i in range(blocks)]
    
    
    obj = Int(max([P[i][1] + y[i] for i in range(blocks)]))
    
    board_problem = values # other constraints I've not included for brevity
    
    o = Optimize()
    o.add(board_problem)
    o.minimize(obj)
    
    if (o.check == 'unsat'):
        print("The problem is unsatisfiable")
    else:
        print("Solved")

Answer 1

这里的问题是您在符号值上调用 Python 的 max，这不适用于符号表达式。相反，定义 max 的符号版本并使用它：

# Return maximum of a vector; error if empty
def symMax(vs):
  m = vs[0]
  for v in vs[1:]:
    m = If(v > m, v, m)
  return m

obj = symMax([P[i][1] + y[i] for i in range(blocks)])

通过此更改，您的程序将在运行时执行并打印 Solved。

z3py：符号表达式不能转换为具体的布尔值

z3py: Symbolic expressions cannot be cast to concrete Boolean values

optimization

smt

z3py