Practically Uniform Solution Sampling in Constraint Programming

Abstract

The ability to sample solutions of a constrained combinatorial space has important applications in areas such as probabilistic reasoning and hardware/software verification. A highly desirable property of such samples is that they should be drawn uniformly at random, or at least nearly so. For combinatorial spaces expressed as sat models, approaches based on universal hashing provide probabilistic guarantees about sampling uniformity. In this short paper, we apply that same approach to cp models, for which hashing functions take the form of linear constraints in modular arithmetic. We design an algorithm to generate an appropriate combination of linear modular constraints given a desired sample size. We evaluate empirically the sampling uniformity and runtime efficiency of our approach, showing it to be near-uniform at a fraction of the time needed to draw from the complete set of solutions.