Citation
Supratik Chakraborty, Daniel J. Fremont, Kuldeep S. Meel, Sanjit Seshia, Moshe Y. Vardi. "Distribution-Aware Sampling and Weighted Model Counting for SAT". Proc. of AAAI, 1722-1730, 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.

Electronic downloads

• 8364-38522-1-PB.pdf · application/pdf · 941 kbytes
• http://escholarship.org/uc/item/2hv2j2df. (link to eScholarship site)
• http://escholarship.org/uc/item/2hv2j2df. (link to eScholarship site)
• http://www.eecs.berkeley.edu/~sseshia/pubdir/aaai14.pdf. ("camera ready" version)
• http://www.aaai.org/ocs/index.php/AAAI/AAAI14/paper/view/8364/8801. (published OA version)

• HTML

  Supratik Chakraborty, Daniel J. Fremont, Kuldeep S. Meel,
  Sanjit Seshia, Moshe Y. Vardi. <a
  href="http://www.terraswarm.org/pubs/306.html"
  >Distribution-Aware Sampling and Weighted Model Counting
  for SAT</a>, Proc. of AAAI, 1722-1730, 2014.

• Plain text

  Supratik Chakraborty, Daniel J. Fremont, Kuldeep S. Meel,
  Sanjit Seshia, Moshe Y. Vardi. "Distribution-Aware
  Sampling and Weighted Model Counting for SAT". Proc. of
  AAAI, 1722-1730, 2014.

• BibTeX

  @inproceedings{ChakrabortyFremontMeelSeshiaVardi14_DistributionAwareSamplingWeightedModelCountingForSAT,
      author = {Supratik Chakraborty and Daniel J. Fremont and
                Kuldeep S. Meel and Sanjit Seshia and Moshe Y.
                Vardi},
      title = {Distribution-Aware Sampling and Weighted Model
                Counting for SAT},
      booktitle = {Proc. of AAAI},
      pages = {1722-1730},
      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.},
      URL = {http://terraswarm.org/pubs/306.html}
  }
  

Posted by Daniel J. Fremont on 22 Apr 2014.
Groups: tools