5

我的情况

我正在做一个需要：

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

我的问题

  • 使用矩阵运算来表达公式以便它们可以解决的最佳方法是z3什么？（Z3Py 的 Sudoku 示例中使用的方式不是很优雅，似乎不适合更复杂的矩阵运算。）

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

4

1 回答 1

3

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 维向量：一阶微分方程的编码为 First排序公式

于 2013-03-24T14:18:45.157 回答