Using SMT solvers to generate random solutions to given predicate

Question

I am interested in generating random solutions to predicates. I only need SMT for integers with the following predicates/functions <, >, <=, >=, ==, !=, +, *

The algorithm I want should produce a random assignment of variables to values (a substitution) such that applying the substitution to the given predicate yields a true statement. In the UNSAT case I just need to know that it is UNSAT.

It is probably important to clarify what I mean by random. I think a sufficient definition is that there might be an extra parameter that acts as a seed. If I give a different seed the algorithm should give me a very different solution rather than the same solution. Frankly I'm not sure how to cash this out but it much the same way that a typical random number generator generates an integer between X and Y (well with a modulus and an addition anyhow) I'd like to generate to a wider class of predicates.

I would like to use existing SMT solvers ideally in either Haskell or the JVM stack (more ideally Haskell however). I have thought of basically just randomizing the DPLL algorithm and translating the SMT problems into SAT my self but that sounds like a terrible idea when really good existing SMT solvers exist.

Answer 1

Let $\varphi(x)$ be the SMT instance, so the task is to find $x$ such that $\varphi(x)$ is true.

One approach is to fix a hash function $h$ that maps a value of $x$ to an element of some small set $S$. Then, you randomly select a value $s \in S$, and ask your SMT solver to find a satisfying assignment for the formula $\varphi(x) \land h(x)=s$.

If you want to generate $k$ random satisfying assignments to $\varphi(x)$, you might choose $S$ to have size a bit bigger than $k$; that will probably suffice.

You probably want to make the hash function $h$ as simple as possible. There is a tradeoff between a simpler hash function (easier for the SMT solver to find satisfying assignments to $\varphi(x) \land h(x)=s$) and a better hash function that mixes the bits better (leads to more random solutions $x$). In practice, often surprisingly simple hash functions suffice. For instance, sometimes your hash function can be chosen via the following simple procedure: pick a random subset of the variables in $x$, project to just those variables, and then hash those variables in some simple way. The hash function itself can be a relatively simple function, e.g., a random linear function: for example, select a random boolean matrix and multiply it with the bit vector obtained from $x$, so that $h(x)=Mx$ for some boolean matrix $M$).

There may be other ways to do it, but this is one way that allows you to use an existing SMT solver, unmodified, as a black box.

Answer 2

A simple approach would be to simply generate a solution, and then ask for a "different" one, surely? Since you mentioned Haskell, you can use the SBV library to implement this easily, and use the allSat function to generate "different" assignments. Here's an example; not quite the same question as yours but somewhat similar, coded in that style: https://hackage.haskell.org/package/sbv-7.2/docs/Data-SBV-Examples-Queries-FourFours.html