• Classified by Research Topic • Sorted by Date • Classified by Publication Type •
Distribution-Aware Sampling and Weighted Model Counting for SAT.
Supratik Chakraborty, Daniel J. Fremont, Kuldeep S. Meel, Sanjit A. Seshia and Moshe Y. Vardi.
In Proceedings of AAAI Conference on Artificial Intelligence (AAAI), July 2014.
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 maximum a posteriori probability (MAP) oracle that assumes prior knowledge of a factored representation of the weight distribution. We 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. Our approach works under mild assumptions on the distribution of weights of satisfying assignments, provides strong theoretical guarantees, and scales to problems involving several thousand variables. We also show that the assumptions can be significantly relaxed while improving computational efficiency if a factored representation of the weights is known.
@inproceedings{CFMSV14,
title={Distribution-Aware Sampling and Weighted Model Counting for {SAT}},
bib2html_dl_pdf={../Papers/AAAI14.pdf},
code={https://bitbucket.org/kuldeepmeel/weightmc},
author={
Chakraborty, Supratik and Fremont, Daniel J. and Meel, Kuldeep S. and
Seshia, Sanjit A. and Vardi, Moshe Y.
},
booktitle=AAAI,
year={2014},
month=jul,
bib2html_rescat={Counting,Sampling},
bib2html_pubtype={Refereed Conference},
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 maximum a posteriori probability (MAP) oracle that
assumes prior knowledge of a factored representation of the weight
distribution. We 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. Our approach
works under mild assumptions on the distribution of weights of satisfying
assignments, provides strong theoretical guarantees, and scales to problems
involving several thousand variables. We also show that the assumptions can
be significantly relaxed while improving computational efficiency if a
factored representation of the weights is known.
},
}
Generated by bib2html.pl (written by Patrick Riley with layout from Sanjit A. Seshia ) on Tue Apr 28, 2026 01:27:21