Constrained Counting and Sampling: Bridging the Gap Between Theory and Practice

Date
2017-09-29
Journal Title
Journal ISSN
Volume Title
Publisher
Description
Abstract

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 constrained counting, the task is to compute the total weight, subject to a given weighting function, of the set of solutions of the given constraints. In constrained sampling, the task is to sample randomly, subject to a given weighting function, from the set of solutions to a set of given constraints. Consequently, Constrained counting and sampling have been subject to intense theoretical and empirical investigations over the years. Prior work, however, offered either heuristic techniques with poor guarantees of accuracy or approaches with proven guarantees but poor performance in practice.

In this thesis, we introduce a novel hashing-based algorithmic framework for constrained sampling and counting that combines the classical algorithmic technique of universal hashing with the dramatic progress made in Boolean reasoning solving, in particular, {\SAT} and {\SMT}, over the past two decades. By exploiting the connection between definability of formulas and variance of the distribution of solutions in a cell defined by 3-universal hash functions, we introduced an algorithmic technique, {\MIS}, that reduced the size of XOR constraints employed in the underlying universal hash functions by as much as two orders of magnitude. The resulting frameworks for counting ( {\ScalApproxMC}) and sampling ({\UniGen}) can handle formulas with up to million variables representing a significant boost up from the prior state of the art tools' capability to handle few hundreds of variables. If the initial set of constraints is expressed as Disjunctive Normal Form (DNF), {\ScalApproxMC} is the only known Fully Polynomial Randomized Approximation Scheme (FPRAS) that does not involve Monte Carlo steps. We demonstrate the utility of the above techniques on various real applications including probabilistic inference, design verification and estimating the reliability of critical infrastructure networks during natural disasters. The high parallelizability of our approach opens up new directions for development of artificial intelligence tools that can effectively leverage high-performance computing resources.

Description
Degree
Doctor of Philosophy
Type
Thesis
Keywords
Constrained Counting, Constrained Sampling, #SAT, universal hashing, SAT, SMT
Citation

Meel, Kuldeep Singh. "Constrained Counting and Sampling: Bridging the Gap Between Theory and Practice." (2017) Diss., Rice University. https://hdl.handle.net/1911/105480.

Has part(s)
Forms part of
Published Version
Rights
Copyright is held by the author, unless otherwise indicated. Permission to reuse, publish, or reproduce the work beyond the bounds of fair use or other exemptions to copyright law must be obtained from the copyright holder.
Link to license
Citable link to this page