Я знаю, что в z3 реализован симплексный решатель. Можно ли использовать решатель для линейной оптимизации? Где находится интерфейс для решателя в исходном коде z3?
Симплексный решатель в Z3
Ответы (1)
Да, в Z3 есть решатель, основанный на симплексном методе. Он реализован в файлах src\smt\theory_arith*. Основные файлы src\smt\theory_arith.h и src\smt\theory_arith_core.h. Этот решатель имеет очень базовую поддержку оптимизации в файле src\smt\theory_arith_aux.h. Эта функциональность не «раскрывается» решателем. Он используется внутри расширений/эвристик для целочисленной и нелинейной арифметики.
Кстати, напомню, что решатель Z3 основан на рациональной (точной) арифметике. Таким образом, это намного медленнее, чем решатели, основанные на арифметике с плавающей запятой. Более того, этот решатель не использует переработанный симплекс-метод.
person
Leonardo de Moura
schedule
16.05.2013
В файле «theory_arith_aux.h» есть группа функций с именем «max_min». Они делают глобальную оптимизацию?
- person liyistc; 04.06.2013
Я не уверен, что вы подразумеваете под глобальной оптимизацией. Метод
max_min(theory_var v, bool max) максимизирует/минимизирует данную внутреннюю переменную теории v по отношению к текущей симплексной таблице и заявленным границам. Функция игнорирует, является ли v целым числом или нет. Это просто выполнение симплексного алгоритма максимизации (минимизации) v.
- person Leonardo de Moura; 05.06.2013
