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

Question

我写这封信是为了询问Z3 Optimize函数背后的理论/算法，特别是它的最大值和最小值函数。这对我来说似乎很神奇。它是某种二分搜索吗？它如何有效地计算出这里的最大/最小值..？

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

如有任何建议或建议，我们将不胜感激。谢谢。

Answer 1

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

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

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

<小时/>

z3优化模理论 (OMT) 求解器具有各种优化过程。其中一些技术比其他技术更有效，但只能处理某些类别的目标函数(即伪 bool /MaxSMT 目标)。在线性算术成本函数无法简化为伪 bool /MaxSMT的情况下，大多数OMT求解器采用的优化搜索的基本方法是运行无论是线性搜索还是二进制搜索。有关两种方法之间的比较，请参阅

• 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]

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

词典优化的定义在互联网上很容易找到，这是我最近使用的:

Definition 4.6.4. (Lexicographic OMT [BP14, BPF15, ST15b, ST15c]). Let <φ,O> be a multi-objective OMT problem, where φ is a ground SMT formula and O = { obj_1 , ..., obj_N } is a sorted list of N objective functions. We call Lexicographic OMT problem, the problem of finding the model M which satisfies φ and makes each obj_i minimum¹ in decreasing order of priority.

¹: in practice objectives need not to be all minimized, this is just for ease of definition

AFAIK，在 z3 中实现的词典优化过程没有在任何公开发表的论文中进行广泛描述。然而，一个简单的方法 lex是运行N单目标(增量)优化，每次固定上一轮获得的最优值。

<小时/>

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