Sciweavers

Share
CAV
2009
Springer

A Markov Chain Monte Carlo Sampler for Mixed Boolean/Integer Constraints

10 years 8 months ago
A Markov Chain Monte Carlo Sampler for Mixed Boolean/Integer Constraints
We describe a Markov chain Monte Carlo (MCMC)-based algorithm for sampling solutions to mixed Boolean/integer constraint problems. The focus of this work differs in two points from traditional SAT Modulo Theory (SMT) solvers, which are aimed at deciding whether a given set of constraints is satisfiable: First, our approach targets constraint problems that have a large solution space and thus are relatively easy to satisfy, and second, it aims at efficiently producing a large number of samples with a given (e.g. uniform) distribution over the solution space. Our work is motivated by the need for such samplers in constrained random simulation for hardware verification, where the set of valid input stimuli is specified by a "testbench" using declarative constraints. MCMC sampling is commonly applied in statistics and numerical computation. We discuss how an MCMC sampler can be adapted for the given application, specifically, how to deal with non-connected solution spaces, effici...
Nathan Kitchen, Andreas Kuehlmann
Added 25 Nov 2009
Updated 25 Nov 2009
Type Conference
Year 2009
Where CAV
Authors Nathan Kitchen, Andreas Kuehlmann
Comments (0)
books