程序员经验分享-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 求解器中约束强化的效率 的相关文章

  • 如何使用 z3py 进行增量求解

    我正在使用 Z3 求解器的 python API 来搜索优化的时间表 它工作得很好 除了有时即使对于小图也非常慢 但有时非常快 原因可能是我的调度问题的约束相当复杂 我试图加快速度 并偶然发现了一些关于增量解决方案的文章 据我了解 您可以使

  • 有没有办法获取Z3中的默认上下文？

    我正在使用 z3py API 4 3 0 我可以轻松翻译一个表达expr从默认上下文到新上下文target ctx using expr translate target ctx 但是我如何从给定的上下文中进行翻译ctx进入默认的 Z3 上

  • 简化 CNF 公式，同时保留某些变量的所有解决方案

    有关的 CNF 简化 https stackoverflow com questions 23461191 cnf simplification 事实上 我认为这个问题的提交者可能是在追求我想要的东西 有许多工具可用于简化 或求解前 预处理

  • 如何让 z3 返回多个 unsat 核心、多个令人满意的作业

    我正在研究一个研究工具的一个组件 我有兴趣检索 对于 QF LRA 多个 最少或其他 UNSAT核心以及 多项 SAT 作业 我检查了论坛以获取有关此主题的早期讨论 例如 在逻辑 QF LRA 上使用 z3 时如何获得不同的 unsat 核

  • 跟踪 z3::optimize unsat_core

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

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

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

  • 在 Z3 中使用 SMT 约束时获取合法范围信息的（次）最佳方法

    这个问题与我之前的问题相关 在 Z3 中使用 SMT 约束时是否可以获得合法的范围信息 https stackoverflow com questions 53676016 is it possible to get a legit ran

  • z3 中如何定义 Int 排序（SMT-LIB 2.0 Ints 理论）和动态声明排序？

    这是我使用 z3 执行的 SMT LIB 2 0 基准测试 set logic AUFLIA declare sort PZ 0 declare fun MS Int PZ Bool assert forall x Int exists X

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

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

  • Z3Py 中最大值的模型不正确

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

  • (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

  • 在 Mac OS X 上构建 z3

    我正在尝试建立Z3 http z3 codeplex com releases view 95640在 Mac OS X 上 按照 README 文件 我刚刚执行了 autoconf configure make 收到错误 omp h 文件

  • Z3 支持非线性算术

    我知道 Z3 对非线性算术有一些支持 但想知道扩展到什么范围 是否可以指定支持和不支持 或可能超时 哪些类别的非线性算术 提前了解这些将帮助我尽早放弃我的任务 似乎不支持与电源相关的内容 如下所示 def pow2 x k Int k re

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

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

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

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

  • SMT中量化算术推理的局限性是什么？

    我在以下看似微不足道的基准测试中尝试了几种 SMT 求解器 CVC3 CVC4 和 Z3 set logic LIA set info smt lib version 2 0 assert forall x Int forall y Int

  • 根据求解器的决定执行 get-model 或 unsat-core

    我想知道 SMT LIB 2 0 脚本中是否有可能访问求解器的最后一个可满足性决策 sat unsat 例如 以下代码 set option produce unsat cores true set option produce model

  • Z3统计中内存使用量的单位是什么？

    z3 统计中测量内存使用情况的单位是什么 是MB还是KB 记忆到底意味着什么 是执行期间的最大内存使用量还是所有分配的总和 它是执行期间最大堆大小的近似值 并通过 cmd context cpp 中的以下函数将其添加到统计对象中 void

  • z3 中的列表串联

    有没有办法在 z3 中连接两个列表 类似于 ML 中的 运算符 我正在考虑自己定义它 但我不认为 z3 支持递归函数定义 即 define fun concat List l1 List l2 List ite isNil l1 l2 co

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

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

随机推荐

热门标签