Z3:找到所有满意的模型 [英] Z3: finding all satisfying models

问题描述

我正在尝试使用 Z3(一种由 Microsoft Research 开发的 SMT 求解器)检索某些一阶理论的所有可能模型.这是一个最小的工作示例:

I am trying to retrieve all possible models for some first-order theory using Z3, an SMT solver developed by Microsoft Research. Here is a minimal working example:

(declare-const f Bool)
(assert (or (= f true) (= f false)))

在这个命题情况下，有两个令人满意的赋值:f->true 和 f->false.由于 Z3(以及一般的 SMT 求解器)只会尝试找到一个令人满意的模型，因此无法直接找到所有解决方案.此处我发现了一个有用的命令，称为(next-sat)，不过好像最新版的Z3已经不支持了.这对我来说有点不幸，总的来说我认为这个命令非常有用.还有其他方法吗?

In this propositional case there are two satisfying assignments: f->true and f->false. Because Z3 (and SMT solvers in general) will only try to find one satisfying model, finding all solutions is not directly possible. Here I found a useful command called (next-sat), but it seems that the latest version of Z3 no longer supports this. This is bit unfortunate for me, and in general I think the command is quite useful. Is there another way of doing this?

推荐答案

实现此目的的一种方法是使用其中一种 API 以及模型生成功能.然后，您可以使用从一次可满足性检查生成的模型来添加约束，以防止在后续可满足性检查中使用先前的模型值，直到没有更多令人满意的分配为止.当然，您必须使用有限排序(或有一些限制来确保这一点)，但是如果您不想找到所有可能的模型(即，在生成一堆后停止)，您也可以将其与无限排序一起使用.

One way to accomplish this is using one of the APIs, along with the model generation capability. You can then use the generated model from one satisfiability check to add constraints to prevent previous model values from being used in subsequent satisfiability checks, until there are no more satisfying assignments. Of course, you have to be using finite sorts (or have some constraints ensuring this), but you could use this with infinite sorts as well if you don't want to find all possible models (i.e., stop after you generate a bunch).

这是一个使用 z3py 的示例(链接到 z3py 脚本:http://rise4fun.com/Z3Py/a6MC):

Here is an example using z3py (link to z3py script: http://rise4fun.com/Z3Py/a6MC ):

a = Int('a')
b = Int('b')

s = Solver()
s.add(1 <= a)
s.add(a <= 20)
s.add(1 <= b)
s.add(b <= 20)
s.add(a >= 2*b)

while s.check() == sat:
  print s.model()
  s.add(Or(a != s.model()[a], b != s.model()[b])) # prevent next model from using the same assignment as a previous model

一般来说，使用所有涉及的常量的析取应该可以工作(例如，这里的 a 和 b).这枚举了 a 和 b(在 1 和 20 之间)满足 a > 的所有整数赋值.= 2b.例如，如果我们将 a 和 b 限制在 1 和 5 之间，则输出为:

In general, using the disjunct of all the involved constants should work (e.g., a and b here). This enumerates all integer assignments for a and b (between 1 and 20) satisfying a >= 2b. For example, if we restrict a and b to lie between 1 and 5 instead, the output is:

[b = 1, a = 2]
[b = 2, a = 4]
[b = 1, a = 3]
[b = 2, a = 5]
[b = 1, a = 4]
[b = 1, a = 5]

这篇关于Z3:找到所有满意的模型的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！