optimization - 在 Z3 中支持三角函数(例如 : cos, tan)

Question

我想用 Z3 来优化一组方程。这里的问题是我的方程是非线性的，但最重要的是它们确实有三角函数。有没有办法在 z3 中处理这个问题？我正在使用 z3py API。

Answer 1

SMT 求解器通常不支持超越数和三角函数。

作为Christopher指出(谢谢!)，Z3 确实支持三角函数和超越函数；但支持相当有限。 (在实践中，这意味着您不应该期望 Z3 决定您向它抛出的每一个公式；在复杂的情况下，它很可能只是返回 unknown。)

参见 https://link.springer.com/chapter/10.1007%2F978-3-642-38574-2_12相关出版物。以下讨论线程中有一些示例可以帮助您入门:https://github.com/Z3Prover/z3/issues/680

另请注意，Z3 的优化求解器不处理非线性方程；所以你将无法优化它们。对于这类优化问题，传统的 SMT 求解器并不是正确的选择。

但是，如果您对 δ-可满足性(允许一定的误差因子)感到满意，那么请查看 dReal，它可以处理三角函数:http://dreal.github.io/然而，据我所知，它没有执行优化。