Z3：执行矩阵运算

Question

我的情况

我正在处理一个需要：

• 证明涉及矩阵操作的3D矩阵变换公式的正确性
• 找到具有未知矩阵条目值的模型。

我的问题

• 如何使用矩阵操作表达公式，以便它们可以通过 z3 求解？（在 Z3Py数独示例中使用的方法不太优雅，似乎不适用于更复杂的矩阵操作。）

谢谢。 - 如果有任何不清楚的地方，请留下问题评论。

- fdj815

Answer 1

Z3不支持这种矩阵，因此最好的方法是对其表示的公式进行编码。这与数独示例编码方式大致相同。以下是一个简单的示例，例如，使用2x2实矩阵（Z3py链接：http://rise4fun.com/Z3Py/MYnB）。

# nonlinear version, constants a_ij, b_i are variables
# x_1, x_2, a_11, a_12, a_21, a_22, b_1, b_2 = Reals('x_1 x_2 a_11 a_12 a_21 a_22 b_1 b_2')

# linear version (all numbers are defined values)
x_1, x_2 = Reals('x_1 x_2')

# A matrix
a_11 = 1
a_12 = 2
a_21 = 3
a_22 = 5

# b-vector
b_1 = 7
b_2 = 11

newx_1 = a_11 * x_1 + a_12 * x_2 + b_1
newx_2 = a_21 * x_1 + a_22 * x_2 + b_2

print newx_1
print newx_2

# solve using model generation
s = Solver()
s.add(newx_1 == 0) # pointers to equations
s.add(newx_2 == 5)
print s.check()
print s.model()

# solve using "solve"
solve(And(newx_1 == 0, newx_2 == 5))

为了让Z3求解未知矩阵实体，请取消第二行的注释（具有a_11、a_12等符号名称），在第五行注释x_1、x_2的其他符号定义，并注释掉对a_11 = 1等的特定赋值。然后，通过找到这些变量的满足分配来使Z3解决任何未知数，但请注意，您可能需要启用模型完成以满足您的需求（例如，如果您需要所有未知矩阵参数或x_i变量的分配，请参见，例如：Z3 4.0：获取完整模型）。

然而，根据您分享的链接，您想使用正弦函数（旋转）执行操作，这些函数通常是超越的，而此时Z3不支持超越（一般指数等）。这将是您的挑战部分，例如，证明旋转的任何角度选择都可以运作，甚至只是编码旋转。缩放和平移应该不太难编码。

此外，查看以下回答以了解如何编码线性微分方程，这些方程的形式为 x' = Ax，其中 A 是一个 n * n 矩阵，x 是一个 n 维向量：将一阶微分方程编码为一阶公式。

- Taylor T. Johnson