Distribution-Aware Sampling and Weighted Model Counting for SAT

Supratik Chakraborty, Daniel J. Fremont, Kuldeep S. Meel, Sanjit A. Seshia, and Moshe Y. Vardi. Distribution-Aware Sampling and Weighted Model Counting for SAT. In Proceedings of the 28th AAAI Conference on Artificial Intelligence (AAAI), pp. 1722–1730, July 2014.

Download

[pdf] 

Abstract

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

BibTeX

@inproceedings{chakraborty-aaai14,
  author    = {Supratik Chakraborty and Daniel J. Fremont and Kuldeep S. Meel and Sanjit A. Seshia and Moshe Y. Vardi},
  title     = {Distribution-Aware Sampling and Weighted Model Counting for {SAT}},
 booktitle = {Proceedings of the 28th AAAI Conference on Artificial Intelligence (AAAI)},
 month = "July",
 year = {2014},
 pages = {1722--1730},
 abstract = {Given a CNF formula and a weight for each assignment 
of values to variables, two natural problems are weighted 
model counting and distribution-aware sampling of satisfying 
assignments. Both problems have a wide variety of important 
applications. Due to the inherent complexity of the 
exact versions of the problems, interest has focused on solving 
them approximately. Prior work in this area scaled only to 
small problems in practice, or failed to provide strong theoretical 
guarantees, or employed a computationally-expensive 
most-probable-explanation (MPE) queries that assumes prior 
knowledge of a factored representation of the weight distribution. 
We identify a novel parameter, tilt, which is the ratio 
of the maximum weight of satisfying assignment to minimum 
weight of satisfying assignment and present a novel approach 
that works with a black-box oracle for weights of assignments 
and requires only an NP-oracle (in practice, a SAT-solver) to 
solve both the counting and sampling problems when the tilt 
is small. Our approach provides strong theoretical guarantees, 
and scales to problems involving several thousand variables. 
We also show that the assumption of small tilt can be significantly 
relaxed while improving computational efficiency if a 
factored representation of the weights is known.},
}