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

  • Nathan Kitchen
  • Andreas Kuehlmann
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5643)


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, efficiently process equality and disequality constraints, handle state-dependent constraints, and avoid correlation of consecutive samples. We present a set of experiments to analyze the performance of the proposed approach.


Markov Chain Monte Carlo Markov Chain Monte Carlo Method Conjunctive Normal Form Proposal Distribution Markov Chain Monte Carlo Sampler 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Iman, S., Joshi, S.: The e Hardware Verification Language. Kluwer Academic, Norwell (2004)zbMATHGoogle Scholar
  2. 2.
    Sutherland, S., Davidmann, S., Flake, P.: SystemVerilog for Design: A guide to using SystemVerilog for hardware design and modeling. Kluwer Academic Publisher, Norwell (2003)zbMATHGoogle Scholar
  3. 3.
    Kitchen, N., Kuehlmann, A.: Stimulus generation for constrained random simulation. In: IEEE/ACM Int’l Conf. on CAD, pp. 258–265 (November 2007)Google Scholar
  4. 4.
    Sebastiani, R.: Lazy satisfiability modulo theories. Journal on Satisfiability, Boolean Modeling and Computation (JSAT) 3, 141–224 (2007)MathSciNetzbMATHGoogle Scholar
  5. 5.
    Kroening, D., Strichman, O.: Decision Procedures. Springer, HeidelbergGoogle Scholar
  6. 6.
    Brémaud, P.: Markov Chains: Gibbs fields, Monte Carlo Simulation, and Queues. Texts in Applied Mathematics, vol. 31. Springer, New York (1999)CrossRefzbMATHGoogle Scholar
  7. 7.
    Metropolis, N., Rosenbluth, A.W., Rosenbluth, M.N., Teller, A.H., Teller, E.: Equations of state calculations by fast computing machines. J. Chem. Phys. 21, 1087–1092 (1953)CrossRefGoogle Scholar
  8. 8.
    Hastings, W.K.: Monte Carlo sampling methods using Markov chains and their applications. Biometrika 57, 97–109 (1970)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Geman, S., Geman, D.: Stochastic relaxation, Gibbs distributions, and the Bayesian restoration of images. IEEE Trans. Pattern Analysis and Machine Intelligence 6(6), 721–741 (1984)CrossRefzbMATHGoogle Scholar
  10. 10.
    Gelfand, A.E., Smith, A.F.M.: Sampling-based approaches to calculating marginal densities. J. Amer. Statist. Assoc. 85(410), 398–409 (1990)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Selman, B., Kautz, H.A., Cohen, B.: Local search strategies for satisfiability testing. In: Trick, M., Johnson, D.S. (eds.) Proc. 2nd DIMACS Challenge on Cliques, Providence RI (1993)Google Scholar
  12. 12.
    Wei, W., Erenrich, J., Selman, B.: Towards efficient sampling: Exploiting random walk strategies. In: Proc. Nat’l Conf. Artificial Intelligence, pp. 670–676 (July 2004)Google Scholar
  13. 13.
    Yuan, J., Shultz, K., Pixley, C., Miller, H., Aziz, A.: Modeling design constraints and biasing in simulation using BDDs. In: Digest Tech. Papers IEEE/ACM Int’l Conf. Computer-Aided Design, pp. 584–589 (November 1999)Google Scholar
  14. 14.
    Kim, H., Jin, H., Ravi, K., Spacek, P., Pierce, J., Kurshan, B., Somenzi, F.: Application of formal word-level analysis to constrained random simulation. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 487–490. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  15. 15.
    Iyer, M.A.: RACE: A word-level ATPG-based constraints solver system for smart random simulation. In: IEEE International Test Conference (ITC), Charlotte, NC, United States, pp. 299–308 (September 2003)Google Scholar
  16. 16.
    Chandra, A., Iyengar, V., Jameson, D., Jawalekar, R., Nair, I., Rosen, B., Mullen, M., Yoon, J., Armoni, R., Geist, D., Wolfsthal, Y.: AVPGEN— a test generator for architectural verification. IEEE Trans. Very Large Scale Int. 3(2), 188–200 (1995)CrossRefGoogle Scholar
  17. 17.
    Shimizu, K., Dill, D.L.: Deriving a simulation input generator and a coverage metric from a formal specification. In: Proc. 39th Design Automation Conf., New Orleans, LA, United States, pp. 801–806 (June 2002)Google Scholar
  18. 18.
    Mihail, M., Papadimitriou, C.H.: On the random walk method for protocol testing. In: Computer Aided Verification. LNCS, pp. 132–141. Springer, Heidelberg (1994)CrossRefGoogle Scholar
  19. 19.
    Sankaranarayanan, S., Chang, R.M., Jiang, G., Ivancic, F.: State space exploration using feedback constraint generation and Monte-Carlo sampling. In: Proc. ESEC-FSE 2007: – 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, pp. 321–330. ACM, New York (2007)Google Scholar
  20. 20.
    Bandyopadhyay, A., Aldous, D.J.: How to combine fast heuristic Markov chain Monte Carlo with slow exact sampling. Electronic Communications in Probability 6, 79–89 (2001)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Nathan Kitchen
    • 1
  • Andreas Kuehlmann
    • 1
    • 2
  1. 1.University of CaliforniaBerkeleyUSA
  2. 2.Cadence Research LabsBerkeleyUSA

Personalised recommendations