python - 在 Python 中求解具有正交约束的不等式系统

Question

我需要为 n 个变量解决一个不等式系统，其中一个不等式具有正交性约束。不等式如下。

在我的特定问题中，已经证明解决系统总是会产生一个精确的解决方案。由于正交性，我认为我不能使用线性规划。任何人都对在 Python 中解决问题的有效方法有建议吗？Wolfram alpha 能够做到！（您可以在此处和此处查看示例）我知道 sympy 无法解决，因为它只能解决单变量情况。请在您给出的任何答案中包含运行时！

编辑：就在发布这个之后，我找到了 z3。它可以在某种程度上做我想要的。但我认为这可能有点矫枉过正，而且可能效率不高（希望 n:= 要解决的变量数是线性的）。

from z3 import Solver, Real
def solve_inequalities(z):
    n = len(z)
    s = Solver()
    ys = [Real(f'y{i}') for i in range(n)]
    s.add(sum(ys) == 0)
    for i in range(1, n):
        s.add(sum(ys[:i]) >= 0)
    s.add(sum([(z[i]-ys[i])*ys[i] for i in range(n)]) == 0)
    for i in range(n-1):
        s.add(z[i]-ys[i] <= z[i+1]-ys[i+1])
    s.check()
    return s.model()

标签： pythonmachine-learningsympymathematical-optimizationsymbolic-math