Constrained Sampling and Counting: Universal Hashing Meets SAT Solving
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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Constrained Counting and Sampling: Bridging the Gap between Theory and Practice
Constrained counting and sampling are two fundamental problems in Computer Science with numerous applications, including network reliability, privacy, probabilistic reasoning, and constrained-random verification. In cons…
A New Probabilistic Algorithm for Approximate Model Counting
Constrained counting is important in domains ranging from artificial intelligence to software analysis. There are already a few approaches for counting models over various types of constraints. Recently, hashing-based ap…
modelOn Hashing-Based Approaches to Approximate DNF-Counting
Propositional model counting is a fundamental problem in artificial intelligence with a wide variety of applications, such as probabilistic inference, decision making under uncertainty, and probabilistic databases. Conse…
Decision MakingDecision Making Under UncertaintyRounding Meets Approximate Model Counting
The problem of model counting, also known as #SAT, is to compute the number of models or satisfying assignments of a given Boolean formula $F$. Model counting is a fundamental problem in computer science with a wide rang…
modelSparse Hashing for Scalable Approximate Model Counting: Theory and Practice
Given a CNF formula F on n variables, the problem of model counting or #SAT is to compute the number of satisfying assignments of F . Model counting is a fundamental but hard problem in computer science with varied appli…