程序员经验分享-hwhale

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

2024-03-13

我已经使用探查器 gprof (statshere http://www.ccs.neu.edu/~jaideep/example2.stats包括调用图）并试图将所花费的时间分为两类：

I) SAT 求解部分（包括[纯]布尔传播和[纯]布尔冲突子句检测、回跳、任何其他命题操作）

II)理论求解部分（包括理论一致性检验、理论冲突子句生成和理论传播）。

执行第 3280-3346 行smt_context.cpp http://z3.codeplex.com/SourceControl/latest#src/smt/smt_context.cpp within bounded_search()构成顶层DPLL(X)环路？

我相信总结 SAT 求解器函数的时间会更容易（因为它们更少） 然后剩下的时间就可以视为理论求解者的时间了。我想弄清楚哪些函数应该被视为属于上面的 I 类？他们是吗smt::context::decide(), smt::context::bcp() within smt::context::propagate()？还有其他人吗？smt::context: resolve_conflict()似乎与理论求解器的调用混合在一起？

这是正确的吗smt::context::propagate()似乎主要是理论传播（第二类），除了它bcp()功能？还，smt::context::final_check()看来纯粹是II类的。

任何提示都非常感激。谢谢。


你是对的，bcp() and decide()是“SAT求解器”的一部分。 功能final_check()只是理论推理。它执行 Z3“声称”过于“昂贵”的程序。这resolve_conflict()过程是混合的：它执行引理学习和回溯。为了生成新的引理，Z3 使用布尔解析（位于“SAT 部分”）。在某些情况下，最昂贵的部分resolve_conflict正在回溯理论求解器的状态。

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

z3

SMT

dpll

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

  • 如何在线使用Z3Py解决运算放大器的问题

    求下列电路中R的值 使用以下代码可以解决此问题 R V1 V2 Vo Reals R V1 V2 Vo I1 V1 R 50 I2 V2 R 10 g R I1 I2 print g equations Vo g print equatio

  • Z3 返回型号不可用

    如果可能的话 我想要对我的代码有第二意见 问题的约束条件是 a b c d e f是非零整数 s1 a b c and s2 d e f 是集合 The sum s1 i s2 j for i j 0 2必须是一个完美的正方形 我不明白为什

  • 哪里可以找到 z3py 教程

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

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

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

  • Z3 量词支持

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

  • 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

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

    出于与此处描述相同的原因 用户定义的未解释函数 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 这是不能令人满意的 我对发生的情况的猜测是 如果第一个参数

  • 将 IR 转换为 Z3 公式？

    我在 IR 中有一些代码 并且该代码已经是 SSA 形式 现在我正在尝试将此代码转换为SMT公式 然后将其提供给Z3进行一些验证 我有一些疑问 有没有技术论文详细解释如何将SSA IR转换为SMT公式 我四处寻找 一无所获 对于那些计算指令

  • 在 SMTLIB v2 输入中使用 :pattern 不断获得“未知”结果

    我在 Z3 中使用 SMTLIBv2 输入格式和模式时遇到问题 通过以下输入 我不断得到 未知 结果 declare datatypes L L0 L1 declare fun path List L declare fun checkTr

  • Z3 的参考资料 - 它是如何工作的[内部理论]？

    我有兴趣阅读 Z3 背后的内部理论 具体来说 我想了解 Z3 SMT 求解器的工作原理 以及它如何找到不正确模型的反例 我希望能够手动计算出一些非常简单的示例的跟踪 然而 所有 Z3 参考文献似乎都是如何在其中编码 或对其算法的非常高级的描

  • 为什么 Z3 中的运算符“/”和“div”给出不同的结果？

    我试图用两个整数来表示一个实数 并将它们用作实数的分子和分母 我写了以下程序 declare const a Int declare const b Int declare const f Real assert f a b assert

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

    说给定一个公式 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 将数组的默认值设置为零

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

  • 目标没有战术支持

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

  • z3 中的函数声明

    在 z3 中是否可以声明一个以另一个函数作为参数的函数 例如 这个 declare fun foo Int Bool Int 似乎不太管用 谢谢 正如 Leonardo 提到的 SMT Lib 确实not允许高阶函数 这不仅仅是语法限制 使

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

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

  • Z3 Java API 定义函数

    我需要您帮助使用 Z3 Java API 定义函数 我尝试解决这样的问题 与 z3 exe 进程一起工作正常 declare fun a Real declare fun b Real declare fun c Bool define f

  • 使用SMT-LIB使用公式计算模块数量

    我不确定使用 SMT LIB 是否可以做到这一点 如果不可能 是否存在可以做到这一点的替代求解器 考虑方程 a lt 10 and a gt 5 b lt 5 and b gt 0 b lt c lt a with a b and c整数

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

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

随机推荐

  • 如何配置IntelliJ 11 +远程tomcat 6 + maven导入模块？

    这是我现在所拥有的 将多个maven模块导入到IntelliJ项目中 Maven 目标从 Maven 项目弹出窗口运行正常 创建一个 war 文件 从 Build Make Project 创建项目也可以 但这里没有创建战争 只是创建 cl

  • myBatis 中 ArrayList 的类型处理程序

    我正在尝试为 ArrayList 编写类型处理程序 但这给了我错误任何人都可以帮助我 我想将 ArrayList 作为 VARCHAR 存储在数据库中并将其作为 ArrayList 检索 package com someweb typeha

  • 如何在容器中存储不同类型的模板化对象？

    假设我有一个vector or list或任何可能更适合这里的容器 我想将模板化类型的多个对象 或指针 存储在 std vector

  • SCNMaterialProperty不是渲染层

    当分配 AVPlayerLayer 时 SCNMaterialProperty 的内容属性在 SCNMaterial 上无法呈现 请注意 这只是物理设备上的问题 在模拟器 Xcode 6 0 1 上运行良好 我正在这样创建我的 SCNode

  • 在谷歌地图上显示多条路线

    我试图在同一张地图上显示多条路线 但无法这样做 无论我做什么 我都只能得到一条路线 function calcRoute var start document getElementById start value var end docum

  • 从字典中获取特定值

    如何从Python中的字典中获取特定的键 我有一本字典 dict redorange 1 blackhawak 2 garlicbread 3 我想获取其键名称中包含大蒜的键的值 我怎样才能实现它 让我们调用你的字典d print v fo

  • 将 nodemon 与 docker 和 docker-compose 结合使用

    我将 nodemon 与 docker compose 一起使用 这是我的 Dockerfile FROM node 10 WORKDIR usr src app COPY package json RUN npm install COPY

  • 如何从 Apache .htaccess 创建虚拟主机？

    我在用Apache 之友 XAMPP http www apachefriends org en xampp html在 Windows 本地服务器 中 我将虚拟主机设置为httpd vhosts conf在 Apache 配置目录中 如下

  • Android - 在 AsyncTask onPostExecute() 中设置的共享首选项并不总是设置？

    我有一些代码在 98 的时间内有效 在我自己的测试中则为 100 因此除了让用户设备遇到此问题之外 我无法真正重现该问题 我在 onPostExecute 中所做的是设置如下参数 SharedPreferences prefs Prefer

  • 带有方角的 UISegmentedControl

    我想用子类修改 UISegmentedControl 以删除圆角 我似乎无法设置cornerRadius 使 SegmentedControl 比屏幕更宽 因此 切掉 角落 不是一个选择 因为我有 4 或 5 个段 然后它们的大小会有所不同

  • 如何使用 python 连接多个 .wav 文件 [重复]

    这个问题在这里已经有答案了 我看到一篇文章将两个 wav 文件连接在一起 但我想知道如何使用 python 连接多个 wav 文件 我正在使用 python 3 6 0 如果有人有办法做到这一点 请教我 我看到另一篇文章要求加入 2 个 w

  • 更改背景后手指绘画速度变慢

    在我的 Paint 应用程序中 我使用了自定义视图 该视图位于 Finger Paint API 演示中 代码如下 public class MyView extends View private static final float MI

  • NSDateFormatter 中的上午/下午问题

    我编写下面的代码将一种日期格式转换为另一种日期格式 但 AM 字符串有效 PM 无效 请帮忙 dateTime 2013 01 24 18 30 PM dateTime 2013 01 24 06 30 AM NSDateFormatter

  • 在活动组中添加新活动时出现 java.lang.StackOverflowError

    我正进入 状态stackoverflow error 我的布局结构如下

  • 如何使用C断言让代码更安全？

    阅读杂项 与SDL开发相关的教程我发现了两个不同的例子 做同样的事情 但以不同的方式 我想知道从代码 安全性 和可维护性的角度来看 您认为这两者中哪一个是正确的 在第一个示例中 程序员根本没有使用断言 但代码看起来不错 至少在我看来 int

  • 零 SQL 死锁设计 - 有编码模式吗？

    我在 MS SQL Server 2005 之上运行的 NET 2 0 Web 应用程序上遇到了非常罕见但烦人的 SQL 死锁 过去 我们一直以非常经验的方式处理 SQL 死锁 基本上是调整查询直到它起作用 然而 我发现这种方法非常不令人满

  • .net 中的固定块

    我对何时需要固定块有点困惑 我有一个例子 它给了我一个矛盾的场景 如下 enum RoomType Economy Buisness Executive Deluxe struct HotelRoom public int Number p

  • maven生成pom文件

    我使用maven 3 0 3并尝试为第三方jar生成pom 如下所示 mvn install 安装文件 Dfile cobra jar DgroupId com cobra DartifactId cobra Dversion 0 98 4

  • 动态更改函数的返回类型

    我正在编写一个具有返回类型的函数 该函数将根据我们传递的列动态更改 在下面的代码中 我传递列值 列数据类型 但我在运行代码时遇到错误 带有返回值的 RETURN 语句不能在此使用 语境 如果这是不可能的 那么如何动态更改返回类型 请提出解决

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

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

热门标签