为什么用z3py求4*4矩阵的本征值要花这么多时间，却没有给出任何解

Question

我试图在代码中计算一个名为a的4*4矩阵的特征值(我知道这些特征值是实值(。A的所有元素都是z3表达式，需要根据前面的约束进行计算。下面的代码是试图计算矩阵a及其特征值的长代码的最后一部分。代码是作为一个整体编写的，但为了调试它，我将其分为两个单独的部分：第一部分代码试图找到矩阵A，第二部分是特征值的计算。在第1部分中，代码运行速度非常快，不到一秒钟就能计算出A，但当我将第2部分添加到代码中时，它不会给我任何解决方案。

我想知道是什么原因？是因为多项式的阶数(4(还是什么？如果有人能帮我找到一种计算特征值的替代方法，或者给我一些关于如何重写代码的提示，让它解决问题，我将不胜感激。

(注意，actusl代码中的A2是一个矩阵，它的所有元素都是由代码中以前的约束定义的z3表达式。但是，在这里，我将元素定义为实数，只是为了使代码可执行。这样，代码给出的解决方案很快，但在实际情况下需要很长时间，比如几天。(。例如，A的一个元素几乎是这样的：

0 +
1*Vq0__1 +
2 * -Vd0__1 +
0 +
((5.5 * Iq0__1 - 0)/64/5) * 
(0 +
0 * (Vq0__1 - 0) +
-521702838063439/62500000000000 * (-Vd0__1 - 0)) +
((.10 * Id0__1 - Etr_q0__1)/64/5) * 
(0 +
521702838063439/62500000000000 * (Vq0__1 - 0) +
0.001 * (-Vd0__1 - 0)) +
0 +
0 + 0 +
0 +
((100 * Iq0__1 - 0)/64/5) * 0 +
((20 * Id0__1 - Etr_q0__1)/64/5) * 0 +
0 +
-5/64

本例中的所有变量都是z3变量。(

from z3 import *
import numpy as np

def sub(*arg):
counter = 0
for matrix in arg:
if counter == 0: 
counter += 1
Sub = [] 
for i in range(len(matrix)):
Sub1 = []
for j in range(len(matrix[0])):
Sub1 += [matrix[i][j]]
Sub += [Sub1]
else:
row = len(matrix)
colmn = len(matrix[0])
for i in range(row):
for j in range(colmn):
Sub[i][j] = Sub[i][j] - matrix[i][j]  
return Sub
Landa = RealVector('Landa', 2) # Eigenvalues considered as real values
LandaI0 = np.diag(  [ Landa[0] for i in range(4)]  ).tolist()
ALandaz3 = RealVector('ALandaz3', 4 * 4 )
############# Building ( A - lambda * I ) to find the eigenvalues ############
A2 = [[1,2,3,4],
[5,6,7,8],
[3,7,4,1],
[4,9,7,1]]
s = Solver()
for i in range(4):
for j in range(4):
s.add( ALandaz3[ 4 * i + j ] == sub(A2, LandaI0)[i][j] )
ALanda = [[ALandaz3[0], ALandaz3[1], ALandaz3[2], ALandaz3[3] ],
[ALandaz3[4], ALandaz3[5], ALandaz3[6], ALandaz3[7] ],
[ALandaz3[8], ALandaz3[9], ALandaz3[10], ALandaz3[11]],
[ALandaz3[12], ALandaz3[13], ALandaz3[14], ALandaz3[15] ]]
Determinant = (
ALandaz3[0] * ALandaz3[5] * (ALandaz3[10] * ALandaz3[15] - ALandaz3[14] * ALandaz3[11]) -
ALandaz3[1] * ALandaz3[4] * (ALandaz3[10] * ALandaz3[15] - ALandaz3[14] * ALandaz3[11]) +
ALandaz3[2] * ALandaz3[4] * (ALandaz3[9]  * ALandaz3[15] - ALandaz3[13] * ALandaz3[11]) -
ALandaz3[3] * ALandaz3[4] * (ALandaz3[9]  * ALandaz3[14] - ALandaz3[13] * ALandaz3[10]) )
tol = 0.001 
s.add( And( Determinant >= -tol, Determinant <= tol ) )   # giving some flexibility instead of equalling to zero
print(s.check())
print(s.model())

Answer 1

请注意，您似乎将Z3用于一种绝对不适用的方程类型。Z是sat/smt解算器。这样的求解器在内部处理大量的布尔方程。整数和分数可以转换为布尔表达式，但使用通用浮点，Z3很快就达到了极限。请参阅此处和此处以获取许多典型示例，并注意如何避免浮动。

Z3可以以有限的方式处理浮点运算，将其转换为分数，但不能处理数值算法中所需的近似和精度。因此，结果通常不是你所希望的。

求特征值是一个典型的数值问题，精度问题非常棘手。Python有numpy和scipy这样的库来有效地处理这些问题。参见例如numpy.linalg.eig。

然而，如果A2矩阵包含一些符号表达式(并使用分数而不是浮点(，sympy的矩阵函数可能是一个有趣的替代方案。