2026-08-17T19:25:28Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23746 2025-11-12T13:00:04Z ddc:004 open_access

SAT-Metropolis: Combining Markov Chain Monte Carlo with SAT/SMT Sampling Dall, Maja Aaslyng Pardo, Raúl Lumley, Thomas Wąsowski, Andrzej SAT/SMT sampling Probabilistic inference Markov Chain Monte Carlo 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Maja Aaslyng Dall and Raúl Pardo and Thomas Lumley and Andrzej Wąsowski 2025 Is Part Of LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.SAT.2025.12 urn:nbn:de:0030-drops-237462 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.12 eng https://creativecommons.org/licenses/by/4.0/legalcode