Abstract
In this paper we address the question of drawing elements from the set of solutions of a constraint satisfaction problem with well defined probability. A distribution over solutions can be specified with the level of precision appropriate for the information on hand. This has application in functional verification, where CSPs are often used to specify the set of legal test programs that a verifier might try to run. With this technique, the probability that a randomly generated test program has any particular properties can be precisely controlled.