pysmt: how to extract models uniformly at random?

Question

I am currently working on a project in which I need to sample n solutions of a given formula. For this I am using the pysmt library, relying on the z3 solver. What I am currently doing is, given a formula (as a pysmt.fnode.FNode), I use the get_model function to extract a solution, and add the negation to the formula and iterate.

The problem with this approach is that at the end of the process, the values of the variables (which are constrained to a finite number of values) are not well distributed, and this is important for the work I am doing.

Is there any way to have the n samples such that the values for all the variables are approximately uniformly distributed in the space of values?

Thank you!

Here is the code for sampling:

solutions = []

for s in range(n_samples):
        solution = []
        model = get_model(formula)

       if model is None:
            print("Not enough solutions")
            break

        sample = []
        for o in self.objects:
            attributes = {
                attr: [
                    x
                    for x in self.values[attr]
                    if model[self.get_attribute(attr, o, x)].is_true()
                ][0]
                for attr in self.values
            }
            sample.append(attributes)

        solutions.append(sample)

        # Exclude the current model by adding a negation of its assertions
        # to the problem, so the next iteration finds a different solution.
        negation = Not(And(EqualsOrIff(x, y) for (x, y) in model))
        formula = And(formula, negation)

Answer 1

If the number of solutions is reasonably small, you can enumerate all solutions in the way you describe and then sample from them randomly.

If you are able to formulate your problem as a SAT problem directly, you can use unigen, which also has python bindings. The resulting samples are provably almost uniform (check the paper for the exact mathematical guarantees).

Answer 2

Uniform sampling isn't something z3 supports. See https://stackoverflow.com/a/12746087/936310 for some comments from 2012; which I believe is still the case.

Uniform sampling (or sampling according to some distribution) is a difficult problem for SMT. There's some research along these lines though. For instance, see: https://github.com/RafaelTupynamba/SMTSampler

Another project to look at: https://github.com/RafaelTupynamba/GuidedSampler

So, this isn't something you can simply achieve using z3, or any other SMT solver, for the time being. At least not out-of-the-box.