代码之家 › 专栏 › 技术社区 › lllllllllllll

Z3优化最大和最小功能背后的理论是什么?

smt z3

3

lllllllllllll · 技术社区 · 6 年前

maximum 和 minimum 作用这对我来说似乎很神奇。这是一种二进制搜索吗?它如何有效地计算出此处的最大/最小值。。?

execute_min_max 函数),但如果对其中的术语没有深入的理解,它对我来说就没有太多意义。。。基本上是什么 lex 站在这里?看起来这些解决方案不知何故被保存在一个堆栈中。

1 回复 | 直到 6 年前

1

2

Patrick Trentin 6 年前

请参阅有关该主题的出版物,例如。

1. 尼古拉·比约纳和安·邓潘。 2014年12月在突尼斯Gammart举行的Proc软件科学符号计算国际研讨会上。EasyChair计算程序(EPiC)。 [PDF]

尼古拉·比约纳、安·邓潘和拉尔斯·弗莱肯斯坦。 Z3-一个优化SMT求解器。 在过程中。塔卡斯,LNCS第9035卷。Springer,2015年——如果这些还不够的话,还有任何其他与优化模理论相关的出版物。 [Springer] [[PDF]

这个 z3 优化模理论(OMT)求解器有各种优化程序。其中一些技术比其他技术更有效,但只能处理某些类别的目标函数(即。 ).就 线性算法 不能简化为的成本函数 ,大多数OMT解算器采用的优化搜索的基本方法是在 线性的- 或 . 有关这两种方法之间的比较,请参见

我不知道如何回答这个问题 有效地 ,因为第一个应该定义什么效率在这方面意味着。正如您从前两份出版物中所看到的, 二进制搜索 并不总是最佳选择,因为优化中的搜索步骤并不完全相同 “成本” .

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

定义4.6.4。(词典OMT[BP14,BPF15,ST15b,ST15c])。 <Ï,O> 是一个多目标OMT问题,其中 Ï O = { obj_1 , ..., obj_N } N 词典OMT问题 M 而且每个 obj_i 按优先级降序排列的最小值。

就我所知 中实现的词典优化程序 z3 lex N 单目标(增量)优化,每次固定上一轮获得的最佳值。

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