Z3: Performing Matrix Operations

Question

My Situation

I'm working on a project which needs to:

• Prove the correctness of 3D matrix transformation formulas involving matrix operations
• Find a model with the values of the unknown matrix entries.

My Question

• 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.

Answer 1

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))

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 ).

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.

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