Uniform Solution Sampling Using a Constraint Solver As an Oracle

TL;DR

This paper introduces a novel uniform solution sampling method using a constraint solver as an oracle, effectively handling complex constrained spaces and enabling accurate approximate model counting.

Contribution

The paper presents a new sampling technique that leverages a constraint solver for uniform exploration and introduces an accurate approximate model counting approach.

Findings

Outperforms standard methods like Simulated Annealing and Gibbs Sampling in complex domains

Effectively handles energy barriers and asymmetric spaces

Provides accurate approximate model counts on benchmark problems

Abstract

We consider the problem of sampling from solutions defined by a set of hard constraints on a combinatorial space. We propose a new sampling technique that, while enforcing a uniform exploration of the search space, leverages the reasoning power of a systematic constraint solver in a black-box scheme. We present a series of challenging domains, such as energy barriers and highly asymmetric spaces, that reveal the difficulties introduced by hard constraints. We demonstrate that standard approaches such as Simulated Annealing and Gibbs Sampling are greatly affected, while our new technique can overcome many of these difficulties. Finally, we show that our sampling scheme naturally defines a new approximate model counting technique, which we empirically show to be very accurate on a range of benchmark problems.