In Z3 (Python), I found a way to see which are the models of a formula. See the post Z3: finding all satisfying models and a piece of code of it below:
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]))
Now, I would like to count how many models are there. Of course, I could add a counter in the loop:
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
However, I would like to know whether there is any native function to do so. Something like s.count_models. Any help?
>Solution :
No. This is the only way. The way to count models is to generate each one-by-one and add them up. Any internal method would essentially do the same.
Model counting is a difficult problem by itself: It is equivalent to finding satisfying assignments in the first place; so you can’t really do any better.
Keep in mind that if you have an unbounded domain (such as unbounded integers as you have in your example), there might be infinite number of models; thus your loop is not always guaranteed to terminate.
For model counting in the SAT context, see: https://www.cs.cornell.edu/~sabhar/chapters/ModelCounting-SAT-Handbook-prelim.pdf.
For model counting in the SMT context, see: https://link.springer.com/article/10.1007/s00236-017-0297-2