Z3 Optimize 最大和最小功能背后的理论是什么? [英] What is the theory behind Z3 Optimize maximum and minimum functionality?

问题描述

我写信是想询问 Z3 Optimize 函数背后的理论/算法，尤其是它的 maximum 和 minimum 函数.这对我来说似乎很神奇.它是以某种方式进行二分搜索吗?它如何有效地计算出此处的最大值/最小值..?

I am writing to inquire the theory/algorithm behind the Z3 Optimize function, especially for its maximum and minimum function. This seems pretty magic to me. Is it somehow a binary search or so? How can it efficiently figure out the max/min value here..?

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

I tried to search for the source code of the related functions (e.g., the execute_min_max function), but without a deep understanding about the terms there, it does not make too much sense to me... Basically what does lex stand for here? It seems that somehow the solutions are maintained inside a stack.

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

Any suggestions or advices would be appreciated very much. Thanks.

推荐答案

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

See publications on the topic like, e.g.

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

1. Nikolaj Bjorner and Anh-Dung Phan. νZ - Maximal Satisfaction with Z3. In Proc International Symposium on Symbolic Computation in Software Science, Gammart, Tunisia, December 2014. EasyChair Proceedings in Computing (EPiC). [PDF]

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

2. Nikolaj Bjorner, Anh-Dung Phan, and Lars Fleckenstein. Z3 - An Optimizing SMT Solver. In Proc. TACAS, volume 9035 of LNCS. Springer, 2015 -- And, if those are not enough, any other publication related to the topic of Optimization Modulo Theories. [Springer] [[PDF]

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

The z3 Optimization Modulo Theories (OMT) solver has various optimization procedures. Some of these techniques are more efficient than others, but can only deal with certain classes of objective functions (i.e. Pseudo-Boolean/MaxSMT objectives). In the case of Linear Arithmetic cost functions which cannot be reduced to Pseudo-Boolean/MaxSMT, the basic approach for the optimization search, adopted by most OMT solvers, is to run either in linear- or binary-search. For a comparison among the two approaches, see either

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

• Roberto Sebastiani and Silvia Tomasi Optimization in SMT with LA(Q) Cost Functions. In IJCAR, volume 7364 of LNAI, pages 484–498. Springer, July 2012. [PDF]

Roberto Sebastiani 和 Silvia Tomasi.具有线性合理成本的优化模理论. ACM Transactions on Computational Logics，16(2)，2015 年 3 月.[PDF]

Roberto Sebastiani and Silvia Tomasi. Optimization Modulo Theories with Linear Rational Costs. ACM Transactions on Computational Logics, 16(2), March 2015. [PDF]

我不知道如何回答这个问题它如何有效地算出这里的最大值/最小值..?"，因为第一个应该定义什么效率在这种情况下意味着.正如您从前两篇文章中了解到的那样，二进制搜索 并不总是最佳选择，因为优化中的搜索步骤没有完全相同的成本".

I am not sure how to answer the question "How can it efficiently figure out the max/min value here..?", because first one should define what efficiency means in this context. As you can read from the previous two publications, binary-search is not always the best choice because search steps in optimization don't have all the same "cost".

词典优化的定义在互联网上随处可见，这是我最近使用的:

The definition of lexicographic optimization is readily available all over the internet, this is the one I used very recently:

定义 4.6.4.(词典 OMT [BP14, BPF15, ST15b, ST15c]). 让 <φ,O> 是一个多目标 OMT 问题，其中 φ 是一个地面 SMT 公式和 O = { obj_1 , ..., obj_N } 是一个 N 目标函数的排序列表.我们称词典OMT问题，即寻找满足φ并使每个obj_i最小¹的模型M的问题优先级递减.

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.

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

AFAIK，在z3 中实现的词典优化程序并未在任何公开可用的论文中进行广泛描述.然而，对于 lex 来说，一个简单的方法是运行 N 个单目标(增量)优化，每次都修复上一轮获得的最佳值.

AFAIK, the lexicographic optimization procedure implemented in z3 is not extensively described in any publicly available paper. However, a trivial approach for lex is to run N single-objective (incremental) optimizations, each time fixing the optimum value obtained at the previous round.

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

If this is not enough to answer your questions, please take a look to any other publication related to the topic of Optimization Modulo Theories.

这篇关于Z3 Optimize 最大和最小功能背后的理论是什么?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！