arrays - Z3求解器中的二维数组

Question

我想使用 C API 使用 z3 求解器定义一个二维数组，如下所示

a[3][3] = { {0,0,0},{0,0,0},{0,0,0}}

如何使用 Z3 求解器 C API 定义它，其中我需要添加约束，例如每行的总和等于 1，并且每个列的总和应该 <= 100。

Answer 1

Z3 支持数组理论，但通常用于编码无界数组或非常大的数组。此问题已在其他帖子中讨论过（请参阅：创建具有固定大小的数组并对其进行初始化）。如果我们搜索[z3] array，我们会发现许多其他帖子。对于预定义大小的数组，创建“Z3 表达式数组”更容易（也更有效）。Z3 教程中的数独示例展示了如何做到这一点。这是您帖子中描述的问题的 Python 代码（也可在此处在线获得）。

# 3x3 matrix of integer variables
A = [ [ Int("a_%s_%s" % (i+1, j+1)) for j in range(3) ] 
      for i in range(3) ]
print A

# Rows constraints
rows_c = [ Sum(r) == 1 for r in A ]
print rows_c

# Columns constraints
A_transpose = [ [ A[i][j] for i in range(3) ] for j in range(3) ]
cols_c = [ Sum(c) <= 10 for c in A_transpose ]
print cols_c

s = Solver()
s.add(rows_c)
s.add(cols_c)
# solve constraints
print s.check()
# print solution
m = s.model()
print m
# printing the solution in a nicer way
r = [ [ m.evaluate(A[i][j]) for j in range(3) ] for i in range(3) ]
print_matrix(r)