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 inartificial intelligence with a diverse range of applications, spanningprobabilistic reasoning and planning to constrained-randomverification. While the theory of these problems was thoroughlyinvestigated in the 1980s, prior work either did not scale toindustrial size instances or gave up correctness guarantees to achievescalability. Recently, we proposed a novel approach that combinesuniversal hashing and SAT solving and scales to formulas with hundredsof thousands of variables without giving up correctnessguarantees. This paper provides an overview of the key ingredients ofthe approach and discusses challenges that need to be overcome tohandle 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 Sun Apr 14, 2024 11:15:51