Z3中的单纯形求解器

Question

我知道在z3中实现了一个单纯形求解器。可以使用求解器进行线性优化吗？z3源代码中解算器的接口在哪里？

Answer 1

是的，Z3有一个基于单纯形法的求解器。它在文件src\smt\theory_arith*中实现。主要文件是src\smt\theory_arith.h和src\smt\theory_arith_core.h。此求解器对文件src\smt\theory_arith_aux.h中的优化提供了非常基本的支持。此功能不会被求解器“公开”。它在整数和非线性算术的扩展/启发式中内部使用。

顺便说一句，回想一下Z3求解器是基于有理(精确)算法的。因此，它比基于浮点运算的求解器慢得多。此外，此求解器不使用修改后的单纯形法。