Z3:执行矩阵运算 [英] Z3: Performing Matrix Operations
问题描述
我正在做一个项目，需要:
I'm working on a project which needs to:
- 证明涉及矩阵运算的3D矩阵转换公式的正确性
- 使用未知矩阵条目的值查找模型.
- Prove the correctness of 3D matrix transformation formulas involving matrix operations
- Find a model with the values of the unknown matrix entries.
- 使用矩阵运算来表达公式的最佳方法是什么
是否可以通过
z3解决? ( Z3Py的数独中使用的方式 例子不是 非常优雅，似乎不适合更复杂的矩阵 操作.)
- What's the best way to express formulas using matrix operations so
that they can be solved by
z3? (The way used in Z3Py's Sudoku Example isn't very elegant and doesn't seem suitable for more complex matrix operations.)
谢谢. -如果不清楚，请发表问题评论.
Thanks. - If anything's unclear, please leave a question comment.
推荐答案
Z3不支持此类矩阵，因此对其进行编码的最佳方法是对它们表示的公式进行编码.这与Sudoku示例对事物进行编码的方式大致相同.这是一个使用2x2实矩阵的简单示例(Z3py链接: http://rise4fun.com/Z3Py/MYnB ):
Z3 has no support for matrices like this, so the best way to encode them is to encode the formulas they represent. This is roughly the same as how the Sudoku example encodes things. Here is a simple example using e.g., a 2x2 real matrix (Z3py link: 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:获取完整模型).
To get Z3 to solve for the unknown matrix entities, uncomment the second line (with the symbolic names for a_11, a_12, etc.), comment the other symbolic definitions of x_1, x_2 on the fifth line, and comment the specific assignments to a_11 = 1, etc. You will then get Z3 to solve for any unknowns by finding satisfying assignments to these variables, but note that you may need to enable model completion for your purposes (e.g., if you need assignments to all of the unknown matrix parameters or x_i variables, see, e.g.: Z3 4.0: get complete model ).
但是，基于共享的链接，您有兴趣使用通常是先验的正弦曲线(旋转)执行操作，并且Z3目前不支持先验的(一般指数等).这对您来说将是具有挑战性的部分，例如，要证明操作有效的旋转角度的任何选择，甚至只是对旋转进行编码.缩放和翻译应该不会太难编码.
However, based on the link you shared, you are interested in performing operations using sinusoids (the rotations), which are in general transcendental, and Z3 at this point does not have support for transcendental (general exponentials, etc.). This will be the challenging part for you, e.g., to prove for any choice of angle for rotations that the operation works, or even just encoding the rotations. The scaling and translations should not be too hard to encode.
此外，关于如何对线性微分方程进行编码，请参见以下答案，线性微分方程是x'= Ax形式的方程，其中A是n * n矩阵，x是n维向量:
Also, see the following answer for how to encode linear differential equations, which are equations of the form x' = Ax, where A is an n * n matrix and x is an n-dimensional vector: Encoding of first order differential equation as First order formula
这篇关于Z3:执行矩阵运算的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
