Classified by Research TopicSorted by DateClassified by Publication Type

Constrained Sampling and Counting: Universal Hashing meets SAT Solving

Constrained Sampling and Counting: Universal Hashing meets SAT Solving .
Kuldeep S. Meel, Moshe Y. Vardi, Supratik Chakraborty, Daniel J. Fremont, Sanjit A. Seshia, Dror Fried, Alexander Ivrii and Sharad Malik.
In Proceedings of Workshop on Beyond NP(BNP), February 2016.

Download

[PDF] 

Abstract

Constrained sampling and counting are two fundamental problems in artificial intelligence with a diverse range of applications, spanning probabilistic reasoning and planning to constrained-random verification. While the theory of these problems was thoroughly investigated in the 1980s, prior work either did not scale to industrial size instances or gave up correctness guarantees to achieve scalability. Recently, we proposed a novel approach that combines universal hashing and SAT solving and scales to formulas with hundreds of thousands of variables without giving up correctness guarantees. This paper provides an overview of the key ingredients of the approach and discusses challenges that need to be overcome to handle larger real-world instances.

BibTeX

@inproceedings{MCVF15,
  title={
    Constrained Sampling and Counting: Universal Hashing meets SAT Solving
  },
  bib2html_dl_pdf={../Papers/BNP16.pdf},
  code={https://bitbucket.org/kuldeepmeel/unigen},
  author={
    Meel, Kuldeep S. and Vardi, Moshe Y. and Chakraborty, Supratik and Fremont,
    Daniel J. and Seshia, Sanjit A. and Fried, Dror and Ivrii, Alexander and
    Malik, Sharad
  },
  booktitle=BNP,
  year={2016},
  bib2html_rescat={Sampling,Counting},
  abstract={
    Constrained sampling and counting are two fundamental problems in
    artificial intelligence with a diverse range of applications, spanning
    probabilistic reasoning and planning to constrained-random
    verification. While the theory of these problems was thoroughly
    investigated in the 1980s, prior work either did not scale to
    industrial size instances or gave up correctness guarantees to achieve
    scalability. Recently, we proposed a novel approach that combines
    universal hashing and SAT solving and scales to formulas with hundreds
    of thousands of variables without giving up correctness
    guarantees. This paper provides an overview of the key ingredients of
    the approach and discusses challenges that need to be overcome to
    handle larger real-world instances.
  },
  month=feb,
  bib2html_pubtype={workshop},
}

Generated by bib2html.pl (written by Patrick Riley with layout from Sanjit A. Seshia ) on Tue Apr 28, 2026 01:27:21