z3中的單工通過所有

Question

SO上已經提出了非常類似的問題，但我找不到以下問題的答案。 線性最大化問題可以利用換所有量詞容易地指出：

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

像上面的查詢可以構成到Z3。 因此，我想問一下，z3是否足夠聰明，可以在識別LP問題時識別LP問題，並且它是否會應用單純形法來消除所有量詞？

我做了一些實驗，它似乎工作，但我沒有嘗試過更復雜的例子。

謝謝！

Answer 1

Z3不會將其識別爲LP優化問題。它很可能首先在量化公式上應用量詞消去，然後結果是無量詞的線性算術，並且出來的模型將爲目標提供最大值。 這當然不是解決優化問題的有效方法。 如果您有勇氣嘗試，那麼z3.codeplex.com下的「opt」分支包含Z3的擴展，可讓您用Z3制定 優化目標。有關如何使用它的說明將很快提供。