Distribution-Aware Sampling and Weighted Model Counting for SAT

Authors

  • 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

DOI:

https://doi.org/10.1609/aaai.v28i1.8990

Keywords:

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

Abstract

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.

Downloads

Published

2014-06-21

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

Issue

Section

Main Track: Novel Machine Learning Algorithms