我写这封信询问Z3优化功能背后的理论/算法，特别是它maximum和minimum功能。这似乎很神奇的给我。它是莫名其妙的二进制搜索或这样的吗？如何才能有效地就在这里找出最大/最小值..？
我试图寻找的相关功能（例如，在execute_min_max功能）的源代码，但没有对条款有深刻的理解，它没有太多的感觉，我...基本上什么呢lex站在这里？看来，在某种程度上解决方案保持堆栈内。
任何建议或意见，将不胜感激非常多。谢谢。
查看该主题等，例如出版物
1.尼古拉Bjorner和映-粪藩。 νZ - 最大满足与Z3。在PROC国际研讨会上的符号计算软件中的科学，Gammart，突尼斯，2014年12月EasyChair诉讼计算（EPIC）。 [PDF]
2.尼古拉Bjorner，映-粪藩，和Lars弗莱肯斯坦。 Z3 - 一个优化SMT求解。在PROC。 TACAS，LNCS的卷9035。施普林格，2015年 - 而且，如果这些是不够的，任何其他公布有关优化模理论的话题。 [Springer] [[PDF]
该z3优化模理论（OMT）求解具有不同的优化方法。这些技术的一些人比其他人更有效，但只能处理某些类别的目标函数（即伪布尔/ MaxSMT目标）。在的线性算术成本函数不能被减少到伪布尔/ MaxSMT，用于优化搜索的基本方法，通过最OMT解算器通过的情况下，是要么在直链或二进制搜索运行。对于这两种方法进行了比较，无论是看
我不知道怎么回答这个问题：“怎样才能有效地就在这里找出最大/最小值..？”，因为第一个应该界定什么效率在这种情况下指。你可以从以前的两个出版物阅读，二进制搜索并不总是因为在优化搜索步骤不具有完全相同的“成本”的最佳选择。
字典优化的定义是现成的在互联网上，这是我最近所使用的：
定义4.6.4。 （辞书OMT [BP14，BPF15，ST15b，ST15c]）。让
<φ,O>是一个多目标OMT问题，其中φ是接地SMT公式和O = { obj_1 , ..., obj_N }是N目标函数的排序列表。我们呼吁辞书OMT问题，寻找满足M，使每个φminimum¹以优先级递减顺序模型obj_i的问题。¹：在实践中的目标不需要被全部最小化，这仅仅是为了便于定义
据我所知，在z3实施的字典优化过程没有广泛在任何公开的论文中描述。然而，对于一个lex琐碎的方法是运行N单目标（增量）的优化，每次在固定在前一轮中得到的最佳值。
如果这还不足以回答你的问题，请大家看看，以与优化模理论的话题任何其他出版物。