时间戳

首页 > 解决方案 > 为什么 z3py 求一个 4*4 矩阵的特征值要花这么多时间，却没有给出任何解？

matrix - 为什么 z3py 求一个 4*4 矩阵的特征值要花这么多时间，却没有给出任何解？

问题描述

我试图在我的代码中计算一个称为 A 的 4*4 矩阵的特征值（我知道特征值是实数值）。A 的所有元素都是 z3 表达式，需要从前面的约束中计算出来。下面的代码是一个长代码的最后一部分，它试图计算矩阵 A，然后是它的特征值。代码是作为一个整体编写的，但我将它分成两个单独的部分以便对其进行调试：第 1 部分代码试图找到矩阵 A，第 2 部分是特征值的计算。在第 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())

标签： matrixeigenvaluez3py

解决方案

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

Z3 可以以有限的方式使用浮点数，将它们转换为分数，但不能使用数值算法所需的近似值和精度。因此，结果通常不是您所希望的。

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

但是，如果您的A2矩阵包含一些符号表达式（并使用分数而不是浮点数），则 sympy的矩阵函数可能是一个有趣的选择。

推荐阅读