Z3(Python)用于计算模型数量的本机方法

Question

在Z3(Python(中，我找到了一种方法来查看公式的模型。见帖子Z3：找到所有令人满意的模型和下面的一段代码：

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]))

现在，我想统计一下有多少型号。当然，我可以在循环中添加一个计数器：

def count_models (s):
counter = 0
while s.check() == sat:
print s.model()
s.add(Or(a != s.model()[a], b != s.model()[b]))
counter = counter + 1
return counter

然而，我想知道是否有任何本地函数可以这样做。比如s.count_models。有什么帮助吗？

Answer 1

否。这是z3目前的唯一方式。计算模型的方法是逐个生成模型并将其相加。任何内部方法基本上都是一样的。

请记住，如果你有一个无界域(比如你的例子中的无界整数(，那么可能有无限数量的模型；因此，您的循环并不总是能够保证终止。

SAT和SMT中的模型计数都是研究问题。以下是一些参考资料供进一步阅读：

• 在SAT上下文中，请参阅：https://www.cs.cornell.edu/~sabhar/章节/ModelCounting-SAT-Handbook-prelim.pdf.

• 在SMT上下文中，请参阅：https://link.springer.com/article/10.1007/s00236-017-0297-2

关于生成模型的注意事项

在z3中生成所有模型的速度可以比您使用的算法更快。看见https://theory.stanford.edu/~nikolaj/programmingz3.html#sec阻止评估以获取详细信息。这个想法仍然是枚举，但使用更好的搜索空间分割，而不是随机遍历