问题标签 [z3]

我使用 Z3 作为有界程序验证的后端求解器。我在不同的操作系统 Windows 7 X64 和 SuSe 10.3 X64 上向 Z3 提供相同的公式，Z3 都是 3.2 版。

他们的输入是： run.z3，它包含嵌套的量词。

在没有启用任何显式选项（默认模式）的情况下，Z3 在 Windows 上运行良好，但是，它在 Linux 上给了我“分段错误”：

../solvers/z3/bin/z3：第 11 行：27951 分段错误

然后我添加唯一的选项

（设置选项：PULL_NESTED_QUANTIFIERS true）

到公式，然后重新运行它，这次它可以在 Linux 上运行，而在 Windows 上它仍然可以运行并且求解速度更快。该选项解决了我在 Linux 上的问题。

Windows 和 Linux 上的 3.2 版 Z3 是否提供不同的功能？这是真的，还有什么区别？提前致谢！

我在一个名为“knapsack.smt2”的文件中有以下背包问题的示例代码，我相信它是 smt2 格式，并且我有最新版本的 Z3：

但是，当我运行“z3 -m knapsack.smt2”时，我收到以下错误消息：

其中第 46 行是最后一行“（get-model）”。

谁能告诉我为什么这不起作用？

谢谢。

我必须将一个多重集划分为两个总和相等的集合。例如，给定多重集：

我会输出两组：

两者之和为 7。

我需要使用 Z3（smt2 输入格式）和“线性算术逻辑”来执行此操作，其定义为：

老实说，我不知道从哪里开始，任何建议都将不胜感激。

问候。

我编写了以下 Perl 脚本来生成 smt2 格式的逻辑约束，以解决给定输入文件的数独难题。输入文件格式如下：

又大又丑的 Perl 脚本是：

导致段错误的脚本部分是：

但是这个片段只是打印出这样的东西：

这在逻辑上应该等同于：

任何建议表示赞赏。

问候。

我希望就如何实现这一点提出建议：

定义：无向图 G 由顶点集 V 和边集 E 定义，其中每条边是大小为 2 的 V 的子集，即无序顶点对 {u, v}。G中长度为k的循环是不同顶点的序列v_1，...，v_k，其中{v_1，v_2}，{v_2，v_3}，...，{v_k-1，v_k}，{v_k，v_1 } 是 G 的所有边。G 中的哈密顿循环是长度为 n = |V| 的循环，即恰好通过图的每个顶点一次的 chcle。如果 G 有一个哈密顿循环，我们称它为 G 哈密顿量。

问题：提供以下决策问题的命题逻辑公式：给定一个无向图 G，G 是哈密顿量吗？配方将由 Z3 检查。

输入格式将是：

其中第一个数字表示顶点的数量，其余的对都是 G 中的边。

输出应该是：0 1 2 3

显然，输出将始终是数字 1、...、n-1 的某种排列，其中 n = |V| 但我看不到如何仅使用命题逻辑来处理整数。

任何建议表示赞赏。

问候。

这是适用于给定输入的解决方案。如果我可以编写一个 perl 例程来生成边的组合（n 选择 k），那么我可以将其推广到任意数量的输入：

我正在解决在无向图中找到哈密顿循环的问题。但最近的一项实验产生了本应是不可能的模型。这是输入：

下面的输出显示所有 e1、e2、e3、e4 和 e5 为真，尽管输入中的 xor 语句明确禁止这样做：

有人对这里出了什么问题有任何意见吗？

问候。

当 Z3 中的公式未满足并指定（get-proof）时，会出现一个输出，我找不到任何关于它是什么的信息。我在哪里可以找到有关此的任何文档？

在我看来，这很不可读，是否有任何工具可以将此作为输入？

干杯，马特

我在 QFBV 公式上使用 Z3。我想知道 Z3 是否可以在诸如 SAT 求解器之类的公式上逐步处理布尔子句。基本上我需要一种方法来实现以下循环：

Z3 是否维护学习到的信息？我可以增量使用 z3 吗？

谢谢。

我在 UFBV 查询上运行 Z3。目前该查询包含 2 个调用check-sat。如果我紧跟push 1在 之后check-sat，Z3 会在 30 秒内解决查询。如果我根本不放任何东西push 1，因此有两个电话之间check-sat没有任何电话push 1，那么 Z3 会在 200 秒内解决它。有趣的。有什么具体原因还是只是巧合？

让我用一个例子来解释我的问题：

假设我有一个可能的离散整数域，例如 -1、0、2、3、5 和 6 现在，我正在为变量 x 寻找满足以下约束的解决方案（或模型）：

(x > 0) && (x < 6) && (x != 3) && (x > 2)

答案将是（来自解决方案域）= 5，对吗？

我如何在 Z3 中做到这一点？

也就是说，我想使用离散实体定义解决方案空间，然后断言一些约束并要求 Z3 检查可满足性。如果满意，那就要模型。

谁能帮我举个例子？

谢谢，--伊什蒂亚克