Z3 Optimize 最大和最小功能背后的理论是什么？

Question

我写信是为了询问 Z3 Optimize 功能背后的理论/算法，尤其是它的maximum 和minimum 功能。这对我来说似乎很神奇。它是某种二进制搜索吗？它如何有效地计算出这里的最大值/最小值..？

我试图搜索相关函数的源代码（例如，execute_min_max 函数），但是对那里的术语没有深入了解，这对我来说没有太多意义......基本上是什么lex 代表这里？似乎解决方案以某种方式保存在堆栈中。

任何建议或意见将不胜感激。谢谢。

Answer 1

查看有关该主题的出版物，例如

1. Nikolaj Bjorner 和 Anh-Dung Phan。 νZ - Z3 的最大满意度。 在 Proc 国际软件符号计算研讨会上科学，Gammat，突尼斯，2014 年 12 月。EasyChair Proceedings in Computing (EPiC)。 [PDF]

2. Nikolaj Bjorner、Anh-Dung Phan 和 Lars Fleckenstein。 Z3 - 优化 SMT 求解器。 在 Proc. TACAS，LNCS 第 9035 卷。 Springer，2015 年——而且，如果这些还不够的话，还有与优化模理论主题相关的任何其他出版物。 [Springer][[PDF]

---

z3 优化模理论 (OMT) 求解器具有各种优化程序。其中一些技术比其他技术更有效，但只能处理某些类别的目标函数（即 Pseudo-Boolean/MaxSMT 目标）。对于无法简化为 Pseudo-Boolean/MaxSMT 的 线性算术 成本函数，大多数 OMT 求解器采用的优化搜索的基本方法是运行在 linear- 或 binary-search 中。有关这两种方法的比较，请参阅

• Roberto Sebastiani 和 Silvia Tomasi 使用 LA(Q) 成本函数优化 SMT。 在 IJCAR，LNAI 的第 7364 卷，第 484-498 页。施普林格，2012 年 7 月。[PDF]

• 罗伯托·塞巴斯蒂安尼和西尔维娅·托马西。 具有线性理性成本的优化模理论。 ACM Transactions on Computational Logics，16(2)，2015 年 3 月。[PDF]

我不知道如何回答这个问题“它如何有效地找出这里的最大值/最小值..？”，因为第一个应该定义什么效率在这种情况下意味着。正如您从前两篇出版物中看到的那样，binary-search 并不总是最佳选择，因为优化中的搜索步骤并不具有完全相同的“成本”。

字典序优化的定义在互联网上随处可见，这是我最近使用的一个：

定义 4.6.4。 （字典式 OMT [BP14, BPF15, ST15b, ST15c]）。 设<φ,O> 是一个多目标 OMT 问题，其中φ 是地面 SMT 公式，O = { obj_1 , ..., obj_N } 是 @987654330 的排序列表@ 目标函数。我们称词典 OMT 问题，即找到满足 φ 的模型 M 并使每个 obj_i 按优先级降序最小¹的问题。

¹：在实践中目标不需要全部最小化，这只是为了便于定义

AFAIK，在z3 中实现的字典优化过程在任何公开可用的论文中都没有广泛描述。但是，lex 的一种简单方法是运行 N 单目标（增量）优化，每次都固定上一轮获得的最佳值。

---

如果这不足以回答您的问题，请查看与优化模数理论主题相关的任何其他出版物。