Document Open Access Logo

SAT-Metropolis: Combining Markov Chain Monte Carlo with SAT/SMT Sampling

Authors Maja Aaslyng Dall, Raúl Pardo , Thomas Lumley, Andrzej Wąsowski

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.SAT.2025.12.pdf
  • Filesize: 1.09 MB
  • 18 pages
HTML5 Logo HTML (experimental)
LIPIcs.SAT.2025.12.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Mathematics of computing
Keywords
  • SAT/SMT sampling
  • Probabilistic inference
  • Markov Chain Monte Carlo

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

Probabilistic inference via Markov Chain Monte Carlo (MCMC) is at the core of statistical analysis and has a myriad of applications. However, probabilistic inference in the presence of hard constraints, so constraints that must hold with probability one, remains a difficult task. The reason is that hard constraints make the state space of the target distribution sparse, and may even divide it into disjoint areas separated by probability-zero states. As a consequence, the random walk performed by MCMC algorithms fails to effectively sample from the complete set of states in the target distribution. In this paper, we propose the use of SAT/SMT sampling to adapt a classic and widely used MCMC algorithm, namely Metropolis sampling. We use SAT/SMT samplers as proposal distributions. In this way, the algorithm ignores probability-zero states. Our method, sat-metropolis, effectively works in problems with multivariate polynomial hard constraints where regular Metropolis fails. We evaluate the convergence and scalability of sat-metropolis using three different state-of-the-art SAT/SMT samplers: SPUR, CMSGen, and MegaSampler. The evaluation shows how different features of the SAT/SMT sampling tools affect the effectiveness of probabilistic inference. We conclude that SAT/SMT sampling is a viable and promising technology for probabilistic inference under hard constraints.

Cite As Get BibTex

Maja Aaslyng Dall, Raúl Pardo, Thomas Lumley, and Andrzej Wąsowski. SAT-Metropolis: Combining Markov Chain Monte Carlo with SAT/SMT Sampling. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 12:1-12:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.SAT.2025.12

Author Details

Maja Aaslyng Dall
  • IT University of Copenhagen, Denmark
Raúl Pardo
  • IT University of Copenhagen, Denmark
Thomas Lumley
  • University of Auckland, New Zealand
Andrzej Wąsowski
  • IT University of Copenhagen, Denmark

Funding

This work was partially funded by DIREC (Digital Research Centre Denmark), a collaboration between the eight Danish universities and the Alexandra Institute supported by the Innovation Fund Denmark.

Supplementary Materials

References

  1. Oriol Abril-Pla, Virgile Andreani, Colin Carroll, Larry Dong, Christopher J. Fonnesbeck, Maxim Kochurov, Ravin Kumar, Junpeng Lao, Christian C. Luhmann, Osvaldo A. Martin, Michael Osthege, Ricardo Vieira, Thomas Wiecki, and Robert Zinkov. PyMC: a modern, and comprehensive probabilistic programming framework in Python. PeerJ Comput. Sci., 9, 2023. URL: https://doi.org/10.7717/peerj-cs.1516.
  2. Dimitris Achlioptas, Zayd Hammoudeh, and Panos Theodoropoulos. Fast sampling of perfectly uniform satisfying assignments. In Proceedings of Theory and Applications of Satisfiability Testing (SAT'18), volume 10929 of LNCS, pages 135-147. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94144-8_9.
  3. Satoshi Aoki, Hisayuki Hara, and Akimichi Takemura. Markov bases in algebraic statistics, volume 199. Springer Science & Business Media, 2012. Google Scholar
  4. Steve Brooks, Andrew Gelman, Galin Jones, and Xiao-Li Meng. Handbook of markov chain monte carlo. CRC press, 2011. Google Scholar
  5. Maja Aaslyng Dall, Raúl Pardo, Thomas Lumley, and Andrzej Wąsowski. SAT-Metropolis. Software, (visited on 2025-07-28). URL: https://github.com/itu-square/sat-metropolis
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.24207
  6. Leonardo Mendonça de Moura and Nikolaj S. Bjørner. Z3: an efficient SMT solver. In Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'08), volume 4963 of LNCS, pages 337-340. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-78800-3_24.
  7. Adrian Dobra. Dynamic markov bases. Journal of Computational and Graphical Statistics, 21(2):496-517, 2012. Google Scholar
  8. Simson Garfinkel, John Abowd, and Christian Martindale. Understanding database reconstruction attacks on public data: These attacks on statistical databases are no longer a theoretical danger. Commun. ACM, 62:46-53, 2019. URL: https://doi.org/10.1145/3287287.
  9. Stuart Geman and Donald Geman. Stochastic relaxation, gibbs distributions, and the bayesian restoration of images. IEEE Transactions on Pattern Analysis and Machine Intelligence, PAMI-6(6):721-741, 1984. URL: https://doi.org/10.1109/TPAMI.1984.4767596.
  10. Priyanka Golia, Mate Soos, Sourav Chakraborty, and Kuldeep S. Meel. Designing samplers is easy: The boon of testers. In Proceedings of Formal Methods in Computer Aided Design, (FMCAD'21), pages 222-230. IEEE, 2021. URL: https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_31.
  11. W. K. Hastings. Monte carlo sampling methods using markov chains and their applications. Biometrika, 57(1):97-109, 1970. Google Scholar
  12. Martin Hazelton, M Mcveagh, and Bruce van Brunt. Geometrically Aware Dynamic Markov Bases for Statistical Linear Inverse Problems. Biometrika, 108:609-626, October 2020. Google Scholar
  13. Martin Hazelton, Michael McVeagh, Christopher Tuffley, and Bruce van Brunt. Some rapidly mixing hit-and-run samplers for latent counts in linear inverse problems. Bernoulli, 30(4):2676-2699, 2024. Google Scholar
  14. Matthew D Hoffman, Andrew Gelman, et al. The no-u-turn sampler: adaptively setting path lengths in hamiltonian monte carlo. J. Mach. Learn. Res., 15(1):1593-1623, 2014. URL: https://doi.org/10.5555/2627435.2638586.
  15. Daniel Kroening and Ofer Strichman. Decision Procedures: An Algorithmic Point of View. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-74105-3.
  16. David J.C. MacKay. Information Theory, Inference, and Learning Algorithms. Cambridge University Press, 2003. Google Scholar
  17. R. McElreath. Statistical Rethinking: A Bayesian Course with Examples in R and Stan. A Chapman & Hall book. CRC Press, 2020. Google Scholar
  18. Michael McVeagh. Efficient Markov bases for Z-polytope sampling: a thesis presented in partial fulfilment of the requirements for the degree of Doctor of Philosophy in Mathematics at Massey University, Manawatū, New Zealand. PhD thesis, Massey University, 2021. Google Scholar
  19. Nicholas Metropolis, Arianna W. Rosenbluth, Marshall N. Rosenbluth, Augusta H. Teller, and Edward Teller. Equation of state calculations by fast computing machines. The Journal of Chemical Physics, 21(6):1087-1092, 1953. Google Scholar
  20. Raúl Pardo, Willard Rafnsson, Christian W. Probst, and Andrzej Wąsowski. Privug: Using probabilistic programming for quantifying leakage in privacy risk analysis. In Proceedings of European Symposium on Research in Computer Security (ESORICS'21), volume 12973 of LNCS, pages 417-438. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-88428-4_21.
  21. Matan I. Peled, Bat-Chen Rothenberg, and Shachar Itzhaky. SMT sampling via model-guided approximation. In Proceedings of International Symposium on Formal Methods (FM'23), volume 14000 of LNCS, pages 74-91. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-27481-7_6.
  22. Hoifung Poon and Pedro Domingos. Sound and efficient inference with probabilistic and deterministic dependencies. In Proceedings of the AAAI Conference on Artificial Intelligence (AAAI'06), volume 1, pages 458-463. AAAI Press, 2006. URL: http://www.aaai.org/Library/AAAI/2006/aaai06-073.php.
  23. Matthew Richardson and Pedro Domingos. Markov logic networks. Machine learning, 62:107-136, 2006. URL: https://doi.org/10.1007/s10994-006-5833-1.
  24. Wei Wei, Jordan Erenrich, and Bart Selman. Towards efficient sampling: Exploiting random walk strategies. In Proceedings of the AAAI Conference on Artificial Intelligence (AAAI'04), pages 670-676. AAAI Press / The MIT Press, 2004. URL: http://www.aaai.org/Library/AAAI/2004/aaai04-106.php.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact