optimization - “最小化”在 Z3 中是如何工作的

Question

我在 Z3 中经常使用最小化功能，我担心一些可伸缩性问题（当我最小化的变量数量增加时）。“最小化”的底​​层算法是什么，有没有一种通用的方法来加快速度？

Answer 1

有关 Z3 中使用的优化算法的详细信息，请参阅本文。关于您关于“加快速度的一般方法”的问题：如果没有确切地看到您正在尝试做什么以及如何对其进行编码，就不可能说出。发布一个事情不会“扩展”的具体示例可能会有所帮助。