Z3：找到所有令人满意的模型

Question

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

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

在这种命题情况下，有两个令人满意的分配：f->true和f->false。由于Z3（通常是SMT求解器）只会尝试找到一个令人满意的模型，因此不可能直接找到所有解决方案。在这里，我找到了一个名为的有用命令(next-sat)，但似乎最新版本的Z3不再支持此命令。这对我来说有点不幸，总体而言，我认为该命令非常有用。还有另一种方法吗？

Answer 1

对于我使用此方法的示例，似乎很有意义，因为在初始模型之后找到下几个模型更快。以下是针对58个模型的特定情况的运行时间（以毫秒为单位）的列表： 8942 801 1663 5 599 320 450 2 2 3 1 5 1377 36 5 738 162 105 1639 3 5 16 2041 27 475 953 562 746 45 151 18 4206 3416 9 850 120 3 4 12 615 593 1219 449 154 987 3 10 1365 16 438 792 1686 743 46 5 8 412 126。请注意，第一个绝对是最长的，但是其他的则随机得多（可能取决于问题以及求解器获得的幸运程度）。