Z3 中的单纯形求解器 [英] Simplex solver in Z3

问题描述

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

I'm aware that there is a simplex solver implemented in z3. Is it possible to use the solver for linear optimization? Where is the interface for the solver located in the z3 source code?

推荐答案

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

Yes, Z3 has a solver based on the Simplex method. It is implemented in the files src\smt\theory_arith*. The main files are src\smt\theory_arith.h and src\smt\theory_arith_core.h. This solver has very basic support for optimization in the file src\smt\theory_arith_aux.h. This functionality is not "exposed" by the solver. It is used internally in the extensions/heuristics for integer and nonlinear arithmetic.

顺便说一句，请记住 Z3 求解器基于有理(精确)算术.因此，它比基于浮点算法的求解器慢得多.此外，该求解器不使用修改后的单纯形法.

BTW, recall that Z3 solver is based on rational (precise) arithmetic. So, it is much slower than solvers based on floating point arithmetic. Moreover, this solver does not use the revised simplex method.

这篇关于Z3 中的单纯形求解器的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！