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中的單形求解器

回答

相關問題