matrix - Z3:执行矩阵运算

Question

我的情况

我正在开展一个项目，需要:

• 证明 3D matrix transformation 的正确性涉及矩阵运算的公式
• 查找包含未知矩阵条目值的模型。

我的问题

• 使用矩阵运算表达公式的最佳方式是什么？它们可以通过 z3 解决吗？ (Z3Py's SudokuExample中使用的方式不是非常优雅，似乎不适合更复杂的矩阵操作。)

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

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: get complete model )。

但是，根据您共享的链接，您有兴趣使用正弦曲线(旋转)执行操作，这些操作通常是超越的，而 Z3 目前不支持超越(一般指数等)。这对您来说将是具有挑战性的部分，例如，证明操作有效的任何旋转角度选择，甚至只是对旋转进行编码。缩放和平移不应该太难编码。

此外，请参阅以下答案，了解如何对线性微分方程进行编码，线性微分方程是 x' = Ax 形式的方程，其中 A 是 n * n 矩阵，x 是 n 维向量:Encoding of first order differential equation as First order formula