我写信是为了询问 Z3 Optimize 功能背后的理论/算法，特别是它的maximum和minimum功能。这对我来说似乎很神奇。它是某种二分搜索吗？它如何有效地计算出这里的最大/最小值..？
我试图搜索相关函数（例如，函数execute_min_max）的源代码，但是如果没有深入理解那里的术语，它对我来说没有太大意义......基本上lex这里代表什么？似乎解决方案以某种方式保存在堆栈内。
任何建议或建议将非常感激。谢谢。
请参阅有关该主题的出版物，例如
\n\n1. Nikolaj Bjorner 和 Anh-Dung Phan。 \xce\xbdZ - 对 Z3 的最大满意度。Proc 软件科学符号计算国际研讨会，Gammart，突尼斯，2014 年 12 月。EasyChair 计算论文集 (EPiC)。[PDF]
\n\n2. Nikolaj Bjorner、Anh-Dung Phan 和 Lars Fleckenstein。 Z3 - 优化 SMT 求解器。在过程中。TACAS，LNCS 第 9035 卷。Springer，2015——如果这些还不够，还可以阅读与优化模理论主题相关的任何其他出版物。[施普林格] [[PDF]
\n\n优化z3模理论 (OMT) 求解器具有各种优化过程。其中一些技术比其他技术更有效，但只能处理某些类别的目标函数（即伪布尔/MaxSMT 目标）。对于无法简化为Pseudo-Boolean/MaxSMT的线性算术成本函数，大多数 OMT 求解器采用的优化搜索的基本方法是在线性搜索或二分搜索中运行。有关两种方法之间的比较，请参阅
Roberto Sebastiani 和 Silvia Tomasi 使用 LA(Q) 成本函数优化 SMT。在 IJCAR，LNAI 第 7364 卷，第 484\xe2\x80\x93498 页。施普林格，2012 年 7 月。[PDF]
罗伯托·塞巴斯蒂亚尼和西尔维娅·托马西。具有线性有理成本的优化模理论。ACM 计算逻辑学报，16(2)，2015 年 3 月。[PDF]
我不知道如何回答这个问题“如何有效地计算出这里的最大/最小值......？” ，因为第一个应该定义效率在这种情况下意味着什么。正如您从前两篇出版物中所读到的那样，二分搜索并不总是最佳选择，因为优化中的搜索步骤并不具有完全相同的“成本”。
\n\n词典优化的定义在互联网上很容易找到，这是我最近使用的：
\n\n\n\n\n定义 4.6.4。（字典顺序 OMT [BP14、BPF15、ST15b、ST15c]）。让
\n\n<\xcf\x86,O>是一个多目标 OMT 问题，其中\xcf\x86是基本 SMT 公式，O = { obj_1 , ..., obj_N }是目标函数的排序列表N。我们称之为词典 OMT 问题M，即找到满足\xcf\x86并使每个obj_i最小值\xc2\xb9 按优先级降序排列的模型的问题。\xc2\xb9：在实践中目标不需要全部最小化，这只是为了便于定义
\n
AFAIK中实现的词典优化过程z3在任何公开的论文中都没有得到广泛的描述。然而，一个简单的方法lex是运行N单目标（增量）优化，每次都固定上一轮获得的最佳值。
如果这还不足以回答您的问题，请查看与优化模理论主题相关的任何其他出版物。
\n