5
$\begingroup$

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.

$\endgroup$
4
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ It sounds like you have used this in practice. Out of curiosity what did you use this for? $\endgroup$ – Jake Dec 4 '14 at 7:25
  • $\begingroup$ also what is meant by small? I want k to be like 1000 or so. $\endgroup$ – Jake Dec 4 '14 at 7:30
  • $\begingroup$ @Jake, you'll have to try it on the kinds of formulas that arise in your situation to see how well it works. It's a standard trick in the literature on using SAT solvers (for instance, it has been used to estimate the number of satisfying assignments to $\varphi(x)$). $\endgroup$ – D.W. Dec 4 '14 at 7:35
  • $\begingroup$ Sounds goods. Any link to this "literature" you might be able to point me to? Or perhaps a general name for this? $\endgroup$ – Jake Dec 4 '14 at 7:37
  • $\begingroup$ @Jake, alas, I'm afraid I don't recall the citation right now, and I can't remember any buzzword or term you could search under. If you searched the literature on estimating the number of satisfying assignments to a formula (basically, approximate #SAT solvers) you might find it, though I know those are pretty broad search parameters. $\endgroup$ – D.W. Dec 4 '14 at 7:38
1
$\begingroup$

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.