z3Opt 使用 qfnra-nlsat 优化非线性函数 [英] z3Opt optimize non-linear function using qfnra-nlsat

问题描述

我正在尝试使用 z3Opt 来优化一个真正的非线性函数，但即使是像下面这样的简单情况

I'm trying to use z3Opt for optimizing a real non-linear function, but even for simple cases like the following one

http://rise4fun.com/Z3Opt/JbaU

结果不是预期的那样.就像z3它根本没有优化......任何人都可以帮助我理解吗?

the result is not what it is expected to be. It's like z3 it is not optimizing at all.... anyone can help me understand?

推荐答案

此时不支持非线性函数的优化，因此不保证结果.如果求解器在这种情况下返回 unknown(而不是 sat)可能会更好，这是我应该研究的问题.

Optimization of non-linear functions is not supported at this point, so no guarantee is given on results. It would probably be better if the solver returns unknown (and not sat) for this case, which is something I should look into.

这篇关于z3Opt 使用 qfnra-nlsat 优化非线性函数的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！