Geek asks and answers

Z3: matrix operations

My position

I am working on a project that should:

My question

  • What is the best way to express formulas using matrix operations that they can be solved with z3? (The method used in Z3Py Sudoku. The example is not very elegant and is not suitable for a more complex operation matrix.)

Thank. - If something is unclear, please leave a comment on the question.

+5
source share
1 answer

Z3 , , . , Sudoku. , , 22 ( 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- :

+3

More articles:


All Articles