通过全部功能在z3中进行单工 [英] Simplex in z3 via for-all

问题描述

已经在SO上提出了非常类似的问题，但是我找不到以下问题的答案. 线性最大化问题可以通过使用全部量词轻松地陈述:

A very similar questions were asked on SO already, but I couldn't find answer to the following problem. A linear maximization problem can be easily stated using for-all quantifier:

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

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

可以将以上查询置于z3. 因此，我想问z3看到一个LP问题时是否足够聪明以识别LP问题，并会采用单纯形方法来消除所有量词吗?

The queries like above can be posed to z3. Consequently I want to ask whether z3 is smart enough to recognize an LP problem when it sees one and will it apply a simplex method to eliminate a for-all quantifier?

我做了一些实验，它似乎可以工作，但是我还没有在更复杂的例子上尝试过.

I did a few experiments and it seemed to work, but I haven't tried it on more complex examples.

谢谢！

推荐答案

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

Z3 does not recognize it as an LP optimization problem. It most likely applies quantifier elimination first on the universally quantified formula, then the result is quantifier-free linear arithmetic and the model that comes out will provide the maximal value for the objective. This is of course not an efficient way to solve optimization problems. If you have courage to experiment, then the branch called "opt" under z3.codeplex.com contains an extension to Z3 that lets you formulate optimization objectives with Z3. A description of how to use it will be available soon.

这篇关于通过全部功能在z3中进行单工的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！