z3 - Z3 中的单纯形求解器

Question

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

Answer 1

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

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