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

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

我在使用 z3py 定义 SMT 问题中的目标函数时遇到了麻烦。

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

我有一个坐标数组（由长度为 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:]]

我这样定义目标函数：

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

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

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

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

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

>

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

完整代码：

    from z3 import *
    from math import ceil
    
    
    width = 8
    blocks = 4
    x = [3,3,5,5]
    y = [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")

解决方法

这里的问题是你在符号值上调用 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。