wolfram-mathematica - 性能问题 : Solving an inequality with several assumptions in Mathematica

Question

我需要在给定几个假设(也是不等式)的情况下证明不等式(或找到一个反例)。不幸的是，要证明的不等式是一个相当长且复杂的表达式。大约有 15 个变量和 FullSimplify的输出填满了几页 A4 纸。对于变量较少的示例，FindInstance如果不等式为真，则有助于找到反例或给出 {} 的结果。我也尝试使用 Reduce以这种方式:

Reduce[
   Implies[
      assumtion1 && assumtion2,
      inequality
   ],
   Reals
]

对于简单的示例，如果不等式成立，则输出“True”。但就我而言，经过几个小时的运行时间后，Mathematica 需要 5-6 GB 的 RAM(和交换)，所以我不得不中止该过程。

我可以用 Mathematica 做些什么来提高性能？

Answer 1

你会发现一篇关于 Mma CAD 算法的非常好的论文 here

Mma 使用的圆柱代数分解 (CAD) 在变量数量上以双指数行为进行缩放。

较新的方法在量词交替的数量上是双指数的。

我认为仅使用 Mma 内部引擎您不会走运，但是您可以根据问题的对称性(如果有)推出自己的引擎