@COMMENT This file was generated by bib2html.pl version 0.94
@COMMENT written by Patrick Riley
@COMMENT This file came from Sanjit Seshia's publication pages at http://www.eecs.berkeley.edu/~sseshia
@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},
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.},
note = "To appear.",
}