Sample uniformly from set of satisfying assignments in Z3

Question

Is there a way to use the Z3 theorem prover to sample uniformly from the set of satisfying assignments? If not, what is the closest system to Z3 that has this capability?

Answer 1

There isn't a direct way to let Z3 do a sample for you uniformly.

It is an interesting question though. For example, it depends on what theories you use as to what uniform means.

The FORMULA tool implements randomized sampling on top of Z3 in a way that takes some properties of theories into account.