程序员经验分享-hwhale

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

2024-01-23

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

我试图搜索相关功能的源代码（例如，execute_min_max https://github.com/Z3Prover/z3/blob/8566d88b992610060a6523f28272d3384a2f2471/src/opt/opt_context.cpp#L394函数），但如果没有深入理解那里的术语，它对我来说没有太大意义......基本上是什么lex站在这里？似乎解决方案以某种方式保存在堆栈内。

任何建议或意见将非常感激。谢谢。


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

1. 尼古拉·比约纳 (Nikolaj Bjorner) 和潘英勇 (Anh-Dung Phan)。 νZ - 对 Z3 的最大满意度。Proc 软件科学符号计算国际研讨会，突尼斯 Gammart，2014 年 12 月。EasyChair 计算论文集 (EPiC)。[PDF] https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-scss2014.pdf

2. 尼古拉·比约纳 (Nikolaj Bjorner)、潘英勇 (Anh-Dung Phan) 和拉尔斯·弗莱肯斯坦 (Lars Fleckenstein)。 Z3 - 优化 SMT 求解器。在过程中。 TACAS，LNCS 第 9035 卷。 Springer，2015——如果这些还不够，还可以阅读与优化模理论主题相关的任何其他出版物。[施普林格] https://link.springer.com/chapter/10.1007/978-3-662-46681-0_14 [[PDF] https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-nuz.pdf

The z3优化模理论 (OMT) 求解器具有各种优化过程。其中一些技术比其他技术更有效，但只能处理某些类别的目标函数（即伪布尔/MaxSMT 目标）。如果是线性算术成本函数不能简化为伪布尔/MaxSMT，大多数 OMT 求解器采用的优化搜索的基本方法是运行linear- or 二分查找。有关两种方法之间的比较，请参阅

  • 罗伯托·塞巴斯蒂亚尼和西尔维娅·托马西 使用 LA(Q) 成本函数优化 SMT。IJCAR，LNAI 第 7364 卷，第 484-498 页。施普林格，2012 年 7 月。[PDF] http://disi.unitn.it/~rseba/papers/ijcar12.pdf

  • 罗伯托·塞巴斯蒂亚尼和西尔维娅·托马西. 具有线性有理成本的优化模理论。ACM 计算逻辑汇刊，16(2)，2015 年 3 月。[PDF] http://disi.unitn.it/~rseba/papers/a12-sebastiani.pdf

我不知道如何回答这个问题“怎么可以有效率的找出这里的最大/最小值..？”，因为第一个应该定义什么效率在此上下文中的意思。正如您可以从前两篇出版物中读到的那样，二分查找并不总是最好的选择，因为优化中的搜索步骤并不完全相同"cost".

的定义词典编法优化在整个互联网上都很容易实现，这是我最近使用的：

定义 4.6.4。 （字典顺序 OMT [BP14、BPF15、ST15b、ST15c]）。 Let <φ,O>是一个多目标 OMT 问题，其中φ是接地 SMT 公式，O = { obj_1 , ..., obj_N }是一个排序列表N目标函数。我们称之为字典序OMT问题, 寻找模型的问题M这满足φ并使每个obj_i最小值 1 按优先级降序排列。

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

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

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

本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)

z3

SMT

Z3 Optimize 最大和最小功能背后的理论是什么？ 的相关文章

  • Z3 上下文序列化/反序列化？

    是否可以序列化 反序列化 Z3 上下文 来自 C 如果没有 这个功能有计划吗 我认为这个功能对于现实世界的应用程序很重要 当前 API 不直接支持此功能 下一版本将支持多个求解器 我们将提供用于将断言从一个求解器复制到另一个求解器并检索断言

  • 检索 Z3Py 中的值会产生意外结果

    我想找到一个表达式的最大间隔e对所有人来说都是如此x 编写这样的公式的方法应该是 Exists d ForAll x in d d e and ForAll x not in d d e 为了得到这样一个d 公式f在 Z3 中 看上面的 可

  • Z3中数组的理论：（1）模型很难理解，（2）不知道如何实现功能，（3）与序列的区别

    继发布于的问题之后Z3 Py 中的数组的表现力如何 一个例子 https stackoverflow com questions 73778513 how expressive can we be with arrays in z3py a

  • 跟踪 z3::optimize unsat_core

    如何正确追踪z3 optimize未饱和核心 Z3 C z3 optimize当我添加时没有找到预期的解决方案不饱和核心跟踪 基于这些examples https github com Z3Prover z3 blob 9df6c10ad8

  • 正确 Dafny 方法的 Z3 模型

    对于正确的方法 Z3能否找到该方法验证条件的模型 我原以为不会 但这里有一个例子 该方法是正确的 但验证发现了一个模型 这是 Dafny 1 9 7 的情况 Malte 所说的是正确的 我发现它也得到了很好的解释 Dafny 是健全的 因为

  • (Z3Py) 函数声明有什么限制吗？

    函数声明有什么限制吗 例如 这段代码返回 unsat from z3 import def one op op arg1 arg2 if op 1 return arg1 arg2 if op 2 return arg1 arg2 if o

  • 如何将 Z3 与 C++ 结合使用

    我想将 Z3 与 C 一起使用 并且我遵循了安装指南 使用 Visual Studio 命令提示符在 Windows 上构建 Z3 https github com Z3Prover z3 building z3 on windows us

  • z3 中使用哪些技术来处理非线性整数实数问题？

    以下是 a 的 z3 统计数据problem http www ccs neu edu home jaideep example smt2在非线性整数实数片段中 我的许多问题与此类似 add rows 11062574 added eqs

  • 有人尝试过用Z3本身来证明Z3吗？

    有没有人尝试证明Z3 http research microsoft com en us um redmond projects z3 与Z3本身 是否有可能使用 Z3 来证明 Z3 是正确的 更理论化的是 是否有可能使用 X 本身来证明工

  • 如何将公式转换为析取范式？

    说给定一个公式 t1 gt 2 或 t2 gt 3 且 t3 gt 1 我希望得到它的析取范式 t1 gt 2 且 t3 gt 1 或 t2 gt 3 且 t3 gt 1 在Z3中如何实现这一点 Z3没有将公式转换为DNF的API或策略 然

  • 使用 Z3 SMT 解决谓词演算问题

    我想使用 Z3 来解决最自然地用原子 符号 集合 谓词和一阶逻辑表达的问题 例如 伪代码 A a1 a2 a3 A is a set B b1 b2 b3 C c1 c2 c3 def p a A b B c C gt Bool p is

  • 在使用和不使用推送调用的情况下对 UFBV 上的 Z3 进行增量调用

    我正在 UFBV 查询上运行 Z3 目前查询包含2个调用check sat 如果我把push 1刚过check sat Z3在30秒内解决了查询 如果我不放任何push 1根本没有 因此有两个电话check sat没有任何push 1他们之

  • Z3 将数组的默认值设置为零

    我正在尝试求解数组表达式的模型 其中数组的默认值等于 0 例如 我正在尝试解决这个例子 但我总是得到未知的结果 declare const arr Array Int Int declare const arr2 Array Int Int

  • 了解 z3 模型

    Z3Py 片段 x Int x fun Function fun IntSort IntSort IntSort phi ForAll x fun x x x print phi solve phi 永久链接 http rise4fun c

  • 将理论插件与求解器结合使用

    最新版本Z3 http z3 codeplex com解耦了以下概念Z3 context and Z3 solver The API http research microsoft com en us um redmond projects

  • 目标没有战术支持

    我有一些代码 我想在一些策略的帮助下检查它们 因为我有很多if then else声明 我要申请elim term ite tactic 我使用了以下策略 check sat using then simplify arith lhs tr

  • Z3：检查模型是否唯一

    Z3 有没有办法证明 表明给定模型是唯一的并且不存在其他解决方案 一个小例子来演示 declare const a1 Int declare const a2 Int declare const a3 Int declare const b

  • 能够删除特定约束的增量 SMT 求解器

    是否有增量 SMT 求解器或用于某些增量 SMT 求解器的 API 我可以在其中增量添加约束 在其中我可以通过某个标签 名称唯一地标识每个约束 我想唯一地标识约束的原因是这样我可以稍后通过指定标签 名称来删除它们 需要放弃约束是因为我之前的

  • 是否可以将一位的位向量转换为 SMTLib2 中的布尔变量？

    我想要一个布尔变量来测试 例如 位向量的第三位是否为 0 位向量的理论允许提取 1 位作为位向量 但不是布尔类型 我想知道我是否可以出演这个角色 谢谢 更新 如果我的问题不清楚 我很抱歉 但 Nikolaj Bjorner 的答案是如何测试

  • 通过 C/C++ API 对 Z3 中的 LIA 进行量词消除

    我想使用 Z3 通过 C C API 消除线性整数算术公式中的量词 考虑一个简单的例子 Exists x x 0 我尝试这样做 context ctx ctx set ELIM QUANTIFIERS true expr x ctx int

随机推荐

  • Azure kubernetes - python 读取configmap？

    我正在尝试对 python 应用程序进行 Dockerize 并希望从 configmap 中读取配置设置 如何在Python中读取configmap 使用配置文件创建 configMap kubectl create configmap

  • Xcode 4：构建失败，没有问题

    该应用程序在模拟器中运行良好 可以构建并运行 当我连接我的设备 运行 iOS 4 3 的 iPhone 3GS 并以 iPhone 为目标时 结果是 构建失败 和 没有问题 查看构建结果窗口 一切都是绿色的 有一个复选标记 包括构建失败通知

  • 无法编译json框架

    我使用 json framework 来解析 json 但是当我编译时出现以下错误 xxx SBJsonStreamParser h xxx SBJsonStreamParser h 105 错误 在 unsafe unretained 之

  • IBM Data Studio 无法浏览 SAMPLE (DB2 Express-C) 上的数据

    我无法浏览 SAMPLE DB 上的数据 设置如下 Windows 7 64 位 PRO IBM DB2 Express C 10 5 500 107 最新 IBM Data Studio 版本 4 1 1 管理安装 使用 IBM Inst

  • 检测到潜在危险的 Request.Form 值

    我有一个带有 wmd 编辑器的表单 输入文本区域使用以下方式呈现 每次我提交表格时我都会得到A potentially dangerous Request Form value was detected from the client 我尝

  • 使用 ssh2 exec 执行多个命令

    我有一个运行一个命令的脚本 根据该结果 我可以运行下一个命令 步骤 运行第一个脚本 它将我置于全局中 然后从全局中我将运行下一个命令 第一个命令 stream ssh2 exec connection 配置全局 在这个结果之后我应该运行这个

  • Firebase部署404找不到index.html

    我在跑firebase init它正在创造firebase json firebase json位于应用程序根目录中 指向我的公共目录app 看这里 firebase json firebase harrison public app ig

  • 如何在spring中使用jdbcTemplate传递多个值进行查询

    在我的 Spring Hibernate 应用程序中 我将所有 sql 查询都放在一个 common queries xml 文件中 其中某些查询需要 2 到 3 个参数 如下所示

  • HTML 查找并停止显示子表

    我已经这样做了 table tbody tr th row1 th td w td tr tr th row2 th td x td tr tbody tbody tr th row1 th td y td tr tr th row2 th

  • 按钮栏不会粘在屏幕底部

    我试图将我创建的按钮栏放在每个屏幕的底部 我很容易就成功地完成了第一个屏幕 现在我尝试把它放到其他屏幕上 但似乎无法粘在屏幕底部 当我查看 hiearchyviewer 时 看起来包裹在我的布局和按钮栏周围的相对布局并没有填充整个屏幕 但它

  • 使用金属的纹理画笔（绘图应用程序）

    I am trying to implement a metal backed drawing application where brushstrokes are drawn on an MTKView by textured squar

  • Haskell 函数反转函数调用

    我有一个 lambda x f gt f x正在使用foldM操作 其中x是一个值并且f a gt b 是否有内置函数可以执行此操作 我可以更换吗 foldM x f gt f x 和一些f foldM f 我以为flip会这样做 但需要三

  • 如何消除 MFMessageComposeViewController 呈现的延迟？

    if MFMessageComposeViewController canSendText MFMessageComposeViewController sms message vc MFMessageComposeViewControll

  • 用于旋转图表数据标签的 Python PPTX 解决方法函数

    I intend to create the following chart using Python PPTX 下面的代码实现了颜色设置 字体大小和数字格式 但是 我还无法旋转数据标签 因为我相信此 API 在 python pptx 0

  • 动态更新 AutoCompleteTextView 适配器

    我想通过从 RESTful Web 服务获取列表来定期更改 AutoCompleteTextview 给出的建议 但无法使其顺利工作 我设置了一个硬编码的建议列表以确保它有效 ArrayAdapter

  • 如何使用 EmbeddedNavigator 在 DevExpress GridView 中保存行更改

    我正在使用嵌入式导航器的添加 编辑和删除按钮 我已经订阅了gridControl1 EmbeddedNavigator ButtonClick事件 然后我检查单击了哪个按钮 问题是 当我编辑单元格并按保存更改时 EndEdit 我没有看到新

  • 如何在Wordnet中找到“词法文件”？

    如果你看一下并选择 显示选项 显示词汇文件信息 您将看到一个非常有用的单词分类 称为词汇文件 例如 对于 填充 我们有

  • 使用 Office Open XML 重复内容

    我一直在研究 Office Open XML 文档规范的可能性 我对能够将自定义 XML 内容添加到文档并将其绑定到内容控件特别感兴趣 我想知道是否可以有重复的内容控制类型 例如 假设我的 docx 文件中有一些自定义 XML 如下所示

  • 为什么使用 AsQueryable() 而不是 List()？

    我正在使用存储库模式进行数据访问实体框架 http en wikipedia org wiki ADO NET Entity Framework and LINQ http en wikipedia org wiki Language In

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

    我写这封信是为了询问 Z3 Optimize 功能背后的理论 算法 特别是它的maximum and minimum功能 这对我来说似乎很神奇 它是某种二分搜索吗 它如何有效地计算出这里的最大 最小值 我试图搜索相关功能的源代码 例如 ex

热门标签