Constrained Sampling and Counting: Universal Hashing Meets SAT Solving

TL;DR

This paper presents a scalable approach for constrained sampling and counting by integrating universal hashing with SAT solving, enabling handling of large industrial-sized instances while maintaining correctness guarantees.

Contribution

It introduces a novel method combining universal hashing and SAT solving that scales to large formulas without sacrificing correctness.

Findings

Scales to formulas with hundreds of thousands of variables

Maintains correctness guarantees in large-scale instances

Provides insights into challenges for real-world applications

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.