Z3(Python)native 模型数统计方法

Question

在 Z3 (Python) 中，我找到了一种查看公式模型的方法。请参阅 post Z3: finding all satisfying models 和下面的一段代码：


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/chapters/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-blocking-evaluations。这个想法仍然是枚举，但是使用更好的搜索拆分 - space 而不是随机遍历它。

Z3(Python)native 模型数统计方法

Z3 (Python) native method for counting the number of models

python

z3

smt

z3py

theorem-proving

生成模型注意事项