CODEWITHSUNDEEP
z3z3py
Amin
Amin

Reputation: 251

Model counting in Z3Py

I am trying to count the number of satisfying assignments by Z3. I am wondering if Z3 provides such information. If so, how can I count models in Z3 and particularly in Z3Py?

Upvotes: 1

Views: 1190

Answers (2)

user118967
user118967

Reputation: 5742

While Taylor's answer will give you the number of satisfying assignments, it will iterate over all of them. In principle, it is possible to do it without such an expensive iteration, but Z3 does not offer it.

There are efficient model counters for propositional logic, the same language used in SAT (search for sharpSAT to find such a system), but as far as I know there is no available model counter modulo theories.

Upvotes: 2

Taylor T. Johnson
Taylor T. Johnson

Reputation: 2884

No, such information is not available by default. However, you could easily implement this (assuming finite number of models) in any of the APIs by combining the model generation capability with adding assertions to prevent future assignments from being assigned the same values as past models. See the following answer for a Z3py script accomplishing this:

Z3: finding all satisfying models

To count the models, simply add a counter to the loop until it becomes unsat, and this will give you the number of models.

Upvotes: 2

Related Questions