Z3中的单形求解器

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

2013-05-14 liyistc

是的，Z3有一个基于Simplex方法的求解器。它在文件src\smt\theory_arith*中执行。主要文件是src\smt\theory_arith.h和src\smt\theory_arith_core.h。该解算器对文件src\smt\theory_arith_aux.h中的优化提供了非常基本的支持。这个功能没有被解算器“暴露”。它在内部用于整数和非线性算术的扩展/启发式。

顺便说一句，记得Z3解算器是基于有理（精确）算术。所以它比基于浮点运算的求解器慢得多。而且，这个求解器不使用修正的单纯形法。

来源

2013-05-16 11:54:55

'theory_arith_aux.h'中有一组名为'max_min'的函数。他们在做全球优化吗？ – liyistc

我不确定全局优化是什么意思。方法'max_min（theory_var v，bool max）'是关于当前单纯形表格和断言边界使给定的内部理论变量'v'最大化/最小化。该函数忽略“v”是否是整数。它只是执行一个简单的算法来最大化（最小化）v。 –

非常感谢你！ – liyistc

Z3中的单形求解器

回答

相关问题