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, Sharad Malik

Research output: Chapter in Book/Report/Conference proceedingConference contribution

22 Scopus citations

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.

Original languageEnglish (US)
Title of host publicationWS-16-01
Subtitle of host publicationArtificial Intelligence Applied to Assistive Technologies and Smart Environments; WS-16-02: AI, Ethics, and Society; WS-16-03: Artificial Intelligence for Cyber Security; WS-16-04: Artificial Intelligence for Smart Grids and Smart Buildings; WS-16-05: Beyond NP; WS-16-06: Computer Poker and Imperfect Information Games; WS-16-07: Declarative Learning Based Programming; WS-16-08: Expanding the Boundaries of Health Informatics Using AI; WS-16-09: Incentives and Trust in Electronic Communities; WS-16-10: Knowledge Extraction from Text; WS-16-11: Multiagent Interaction without Prior Coordination; WS-16-12: Planning for Hybrid Systems; WS-16-13: Scholarly Big Data: AI Perspectives, Challenges, and Ideas; WS-16-14: Symbiotic Cognitive Systems; WS-16-15: World Wide Web and Population Health Intelligence
PublisherAI Access Foundation
Pages344-351
Number of pages8
ISBN (Electronic)9781577357599
StatePublished - Jan 1 2016
Event30th AAAI Conference on Artificial Intelligence, AAAI 2016 - Phoenix, United States
Duration: Feb 12 2016Feb 13 2016

Publication series

NameAAAI Workshop - Technical Report
VolumeWS-16-01 - WS-16-15

Other

Other30th AAAI Conference on Artificial Intelligence, AAAI 2016
CountryUnited States
CityPhoenix
Period2/12/162/13/16

All Science Journal Classification (ASJC) codes

  • Engineering(all)

Fingerprint Dive into the research topics of 'Constrained sampling and counting: Universal hashing meets SAT solving'. Together they form a unique fingerprint.

  • Cite this

    Meel, K. S., Vardi, M. Y., Chakraborty, S., Fremont, D. J., Seshia, S. A., Fried, D., Ivrii, A., & Malik, S. (2016). Constrained sampling and counting: Universal hashing meets SAT solving. In WS-16-01: Artificial Intelligence Applied to Assistive Technologies and Smart Environments; WS-16-02: AI, Ethics, and Society; WS-16-03: Artificial Intelligence for Cyber Security; WS-16-04: Artificial Intelligence for Smart Grids and Smart Buildings; WS-16-05: Beyond NP; WS-16-06: Computer Poker and Imperfect Information Games; WS-16-07: Declarative Learning Based Programming; WS-16-08: Expanding the Boundaries of Health Informatics Using AI; WS-16-09: Incentives and Trust in Electronic Communities; WS-16-10: Knowledge Extraction from Text; WS-16-11: Multiagent Interaction without Prior Coordination; WS-16-12: Planning for Hybrid Systems; WS-16-13: Scholarly Big Data: AI Perspectives, Challenges, and Ideas; WS-16-14: Symbiotic Cognitive Systems; WS-16-15: World Wide Web and Population Health Intelligence (pp. 344-351). (AAAI Workshop - Technical Report; Vol. WS-16-01 - WS-16-15). AI Access Foundation.