问题标签 [smt]

按照本教程，我尝试了本教程中的第一个示例。

我执行了这个命令

unknown不像unsat教程中那样。

这可能有什么问题？

我在 sat 求解器的背景下问这个问题。假设我有 100 个整数变量x1, x2, x3 ... x100，它们在1 to N. 我想确保至少一个变量x1 to x100应该具有来自1 to N.

现在我想在 sat 求解器约束中编码这个问题。由于在编写约束时我不知道值N，所以我很难编写如下代码 -

可以说，最后，我断言 N 的值为 2，那么上述约束将不起作用。除此之外，出于性能原因，我不想使用数组或未解释的函数。

更新 ：

简而言之，约束如下 -

1. N < 100
2. （假设 N = 20），那么有 20 个变量，它们可能是从 x_1 到 x_100 中的任何一个，它们是不同的。因此，此约束将确保为从 1 到 N 的每个值分配至少一个变量。
3. 其余变量 (100-N) 的值可以相互重叠。

谁能给我一些建议？

有没有办法使用 Z3 定理证明器从一组令人满意的作业中均匀采样？如果不是，那么最接近 Z3 且具有此功能的系统是什么？

我正在使用 Microsoft 的 Z3 SMT 求解器，并且正在尝试定义自定义排序的常量。默认情况下，这些常量似乎不是不相等的。假设您有以下程序：

这将给出“sat”，因为当然完全有可能两个相同类型的常数相等。由于我正在制作常量必须彼此不同的模型，这意味着我需要添加形式的公理

对于每一对相同类型的常数。我想知道是否有某种方法可以做到这一点，以便默认情况下每个排序常量都是唯一的。

如何访问参数化排序的值？

例如，如果我有以下声明：

如何访问x代表的对中的第一个元素？

我从模板生成问题，由于问题的性质，我不得不依赖量词。现在，求解器只能找到非常简单（可满足）问题的实例。在许多情况下，查找“未饱和”是有效的。找到“sat”很少奏效。

问题是，即使是像定义两个不相交集合这样简单的事情也必须用一些非常讨厌的公式来表达：

（在这里找到完整的问题）

为了找到实例，Z3 必须找到函数的解释in_1。所有其他功能都依赖于它。

到目前为止，我听到了以下与我的问题有关的陈述：

1. 每个量词都应该有一个模式
2. 如果有任何无限模型，则实例查找不起作用

我在网络或文献中找不到任何有用的信息来说明如何实现或避免这种情况。所以我的问题仍然存在：

如何有效地找到可满足公式的实例（使用 Z3）？我如何使用模式来实现这一点（如果有的话）？

我在 .NET API 中创建了一个现有的 Z3 4.1 上下文，其中包含许多函数声明、排序声明、断言假设等。

在此上下文中使用所有现有声明解析 SMT-LIB2 字符串的最简洁方法是什么？具体来说，有没有办法遍历上下文中的所有声明？我在 Context 中没有看到任何允许我访问声明的方法。

目前，我正在执行以下操作：

有没有办法从 z3 上下文本身获取所有这些声明和符号名称？它们都已经在 z3 对象中声明了。我宁愿这样做，也不愿遍历我的内部数据结构。

我可能错过了它，但我没有看到任何可以让我在 API 中执行此操作的内容。我正在成像类似于可通过 Solver.Assertions 获得的断言公式数组。

定理证明工具 z3 需要花费大量时间来解决一个公式，我相信它应该能够轻松处理。为了更好地理解这一点并可能优化我对 z3 的输入，我想查看 z3 在其求解过程中生成的内部约束。从命令行使用 z3 时，如何打印 z3 为其后端求解器生成的公式？

我想将一阶理论放入微软开发的 SMT 求解器 Z3 中。该理论包含两个对象obj1和obj2，一个函数move接受一个对象并返回一个动作，以及一个单一的谓词发生，它将一个动作作为参数。该理论包含公式发生(move(obj1))，我想确保这是发生谓词为真的唯一方式。我通过给出发生的定义来做到这一点：

这意味着从理论上可以推断出发生(move(obj1)) ，但发生(move(obj2))不能。为了证明这一点，我把它翻译成 Z3 如下：

问题是这给出了以下输出：

我不明白，因为发生的定义为谓词为真提供了所有必要和充分条件，所以我认为发生（move（obj2））在任何模型中都不能为真。我究竟做错了什么？

更新 感谢 de Moura，我已经能够找到解决问题的方法。我需要做的是为动作提供唯一的名称公理，在我的例子中就是move函数。我需要声明，当它有两个不同的参数时，它move永远不会返回相同的排序元素。Action这可以通过多种方式完成，但我发现这是最简洁的版本：

我试图在微软的 SMT 求解器 Z3 中证明一个归纳事实。我知道 Z3 通常不提供此功能，如Z3 指南（第 8 节：数据类型）中所述，但是当我们限制要证明事实的域时，这似乎是可能的。考虑以下示例：

求解器以 正确响应unsat，这意味着它(p 20)是有效的。问题是，当我们进一步放宽这个约束时（我们20在前面的例子中用任何大于 20 的整数替换），求解器的响应是unknown。

我觉得这很奇怪，因为 Z3 解决最初的问题并不需要很长时间，但是当我们将上限增加 1 时，它突然变得不可能了。我试图向量词添加一个模式，如下所示：

哪个似乎更好，但现在上限是 40。这是否意味着我可以更好地不使用 Z3 来证明这些事实，还是我错误地表述了我的问题？