程序员经验分享-hwhale

SMT 求解器中约束强化的效率

2023-11-30

解决优化问题的一种方法是使用 SMT 求解器来询问是否存在（坏）解决方案，然后逐步添加更严格的成本约束，直到命题不再可满足。例如，该方法在以下内容中进行了讨论：http://www.lsi.upc.edu/~oliveras/espai/papers/sat06.pdf and http://isi.uni-bremen.de/agra/doc/konf/08_isvlsi_optprob.pdf.

是这种做法吗高效的， 尽管？即，当尝试使用附加约束进行求解时，求解器是否会重复使用先前解决方案中的信息？


求解器可以重用在尝试解决先前查询时学到的引理。只要记住，无论何时执行 Z3pop所有引理（自相应的push）被遗忘。因此，要实现这一目标，您必须避免push and pop如果需要撤回断言，请使用命令并使用“假设”。在下面的问题中，我描述了如何在Z3中使用“假设”：Z3 中的软/硬约束

就效率而言，这种方法并不是对于每个问题域都是最有效的方法。另一方面，它可以在大多数 SMT 求解器之上实现。此外，伪布尔求解器（0-1 整数问题的求解器）成功地使用类似的方法来求解优化问题。

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

z3

SMT

SMT 求解器中约束强化的效率 的相关文章

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

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

  • 哪里可以找到 z3py 教程

    由于某些安全问题 rise4fun z3py 将在几周内不可用 我试图找到一些学习z3py的资源但徒劳无功 请推荐一些学习z3py的资源 我使用 Z3Py 教程源创建了一个 zip 文件 它基本上是一些 HTML 页面和一堆 python

  • Z3 量词支持

    我需要一个定理证明器来解决一些简单的线性算术问题 然而 即使是简单的问题我也无法让 Z3 工作 我知道它不完整 但是它应该能够处理这个简单的示例 assert forall t Int t 5 check sat 我不确定我是否忽略了某些事

  • 跟踪 z3::optimize unsat_core

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

  • 【无标题】SMT贴片加工过程中需要注意的事项

    1 SMT贴片加工 技术员在产线上应佩戴好检验OK的防静电手环 金属片紧贴手腕并保持良好双手交替作业 插件前检查每个订单的电子元器件无错 混料 破损 变形 划伤等不良现象 2 电路板插件需要提前把电子物料准备好 注意电容极性方向须确认无误

  • 正确 Dafny 方法的 Z3 模型

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

  • Z3/SMT：我什么时候应该选择推送/弹出来重置？

    我使用 Z3 来解决符号执行器产生的路径条件 该执行器以深度优先顺序探索状态空间 与 CUTE DART 或 可能 SAGE 非常相似 我们正在尝试使用 Z3 的不同方式 在一种极端情况下 我们将每个查询发送到 Z3 并在之后立即 重置 它

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

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

  • 任意长度的通用位向量类型

    出于与此处描述相同的原因 用户定义的未解释函数 https stackoverflow com questions 7740556 equivalent of define fun in z3 api 我想定义我自己的未解释函数 bvred

  • 为什么0=0.5？

    我注意到 Z3 4 3 1 在处理 smt2 文件时出现一些奇怪的行为 If I do assert 0 0 5 就会得到满足 但是 如果我改变顺序并执行 assert 0 5 0 这是不能令人满意的 我对发生的情况的猜测是 如果第一个参数

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

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

  • 如何估计在 z3 for SMT 中解决 SAT 部分所花费的时间？

    我已经使用探查器 gprof statshere http www ccs neu edu jaideep example2 stats包括调用图 并试图将所花费的时间分为两类 I SAT 求解部分 包括 纯 布尔传播和 纯 布尔冲突子句检

  • 在 Z3 中证明归纳事实

    我试图在 Microsoft 的 SMT 求解器 Z3 中证明一个归纳事实 我知道 Z3 一般不提供此功能 如Z3 guide http rise4fun com z3 tutorial guide 第 8 节 数据类型 但是当我们限制要证

  • Z3 实数算术和数据类型理论整合得不太好

    这与我之前问过的问题有关Z3 SMT 2 0 与 Z3 py 实现 https stackoverflow com questions 13826217 z3 smt 2 0 vs z3 py implementation我实现了无穷大正实

  • Z3 SMT 求解器中的常数相等

    我正在使用 Microsoft 的 Z3 SMT 求解器 并且我正在尝试定义自定义类型的常量 默认情况下 这些常量似乎并不不平等 假设您有以下程序 declare sort S 0 declare const x S declare con

  • 为什么 Z3 在这个简单的输入上返回“未知”？

    这是输入 set option auto config false set option mbqi false declare sort T6 declare sort T7 declare fun set23 T7 T7 Bool ass

  • (Z3Py) 声明函数

    我想在简单的 result x t c 公式中找到一些给定结果 x 对的 c 和 t 系数 from z3 import x Int x c Int c t Int t s Solver f Function f IntSort IntSo

  • 如何获取 Z3 上下文的所有可用配置设置的列表？

    net API 具有以下 Context 构造函数 Context Dictionary lt string string gt settings 如何获取所有可能设置的列表 具体来说 我对如何要求 Z3 生成 unsat 核心感兴趣 即相

  • Z3 python对待x**2与x*x不同？

    看来Z3 Python接口不喜欢 运算符 它可以处理x x但不能处理x 2 如下例所示 gt gt gt x y x y Reals x y gt gt gt z3 prove Implies x 6 0 x 2 36 0 failed t

  • 如何在Z3中使用四元数进行计算？

    In Z3 中的复数 http research microsoft com en us um people leonardo blog 2013 01 26 complex htmlLeonardo de Moura 能够在 Z3 中引入

随机推荐

热门标签