Distribution-Aware Sampling and Weighted Model Counting for SAT


  • Supratik Chakraborty Indian Institute of Technology, Bombay
  • Daniel Fremont University of California, Berkeley
  • Kuldeep Meel Rice University
  • Sanjit Seshia University of Califonia, Berkeley
  • Moshe Vardi Rice University




Weighted model counting, weighted sampling, SAT, Probabilistic inference, machine learning


Given a CNF formula and a weight for each assignment of values tovariables, two natural problems are weighted model counting anddistribution-aware sampling of satisfying assignments. Both problems have a wide variety of important applications. Due to the inherentcomplexity of the exact versions of the problems, interest has focusedon solving them approximately. Prior work in this area scaled only tosmall problems in practice, or failed to provide strong theoreticalguarantees, or employed a computationally-expensive most-probable-explanation ({\MPE}) queries that assumes prior knowledge of afactored representation of the weight distribution. We identify a novel parameter,\emph{tilt}, which is the ratio of the maximum weight of satisfying assignment to minimum weightof satisfying assignment and present anovel approach that works with a black-box oracle for weights ofassignments and requires only an {\NP}-oracle (in practice, a {\SAT}-solver) to solve both thecounting and sampling problems when the tilt is small. Our approach provides strong theoretical guarantees, and scales toproblems involving several thousand variables. We also show that theassumption of small tilt can be significantly relaxed while improving computational efficiency if a factored representation of the weights is known.




How to Cite

Chakraborty, S., Fremont, D., Meel, K., Seshia, S., & Vardi, M. (2014). Distribution-Aware Sampling and Weighted Model Counting for SAT. Proceedings of the AAAI Conference on Artificial Intelligence, 28(1). https://doi.org/10.1609/aaai.v28i1.8990



Main Track: Novel Machine Learning Algorithms