z3中的单工通过for-all

Question

已经在 SO 上提出了非常相似的问题，但我找不到以下问题的答案。 使用 for-all 量词可以很容易地说明线性最大化问题：

obj = f(x) AND \forall x . Ax <= b => f(x) <= obj

上面的查询可以提交给z3。 因此，我想问一下 z3 是否足够聪明，可以在遇到 LP 问题时识别它，它是否会应用单纯形法来消除 for-all 量词？

我做了一些实验，它似乎有效，但我还没有尝试过更复杂的例子。

谢谢！

Answer 1

Z3 不将其识别为 LP 优化问题。它很可能首先在全称量化公式上应用量词消除，然后结果是无量词线性算术，并且出来的模型将为目标提供最大值。 这当然不是解决优化问题的有效方法。 如果您有勇气尝试，那么 z3.codeplex.com 下名为“opt”的分支包含 Z3 的扩展，可让您制定公式 Z3 的优化目标。关于如何使用它的说明将很快提供。