Uniform Solution Sampling Using a Constraint Solver As an Oracle

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.

Appears in Proceedings of the Twenty-Eighth Conference on Uncertainty in Artificial Intelligence (UAI2012)

Cited by in corpus (12)

• Adaptive Fog Configuration for the Industrial Internet of Things
• HoloClean: Holistic Data Repairs with Probabilistic Inference
• Constrained Sampling and Counting: Universal Hashing Meets SAT Solving
• A Scalable Approximate Model Counter
• Sampling Techniques for Boolean Satisfiability
• Constrained Counting and Sampling: Bridging the Gap between Theory and Practice
• Sound Probabilistic #SAT with Projection
• The Model Counting Competition 2020
• On Testing of Samplers
• On Scalable Testing of Samplers
• Approximate Model Counting by Partial Knowledge Compilation
• A New Probabilistic Algorithm for Approximate Model Counting