Approximate Model Counting: Is SAT Oracle More Powerful than NP Oracle?

Abstract

Given a Boolean formula $\phi$ over $n$ variables, the problem of model counting is to compute the number of solutions of $\phi$. Model counting is a fundamental problem in computer science with wide-ranging applications in domains such as quantified information leakage, probabilistic reasoning, network reliability, neural network verification, and more. Owing to the #P-hardness of the problems, Stockmeyer initiated the study of the complexity of approximate counting and show that $\log n$ calls to an NP oracle are necessary and sufficient to achieve tight guarantees.

It is well known that an NP oracle does not fully capture the behavior of SAT solvers, as SAT solvers are also designed to provide satisfying assignments when a formula is satisfiable, without additional overhead. Accordingly, the notion of SAT oracle has been proposed to capture the behavior of SAT solver wherein given a Boolean formula, an SAT oracle returns a satisfying assignment if the formula is satisfiable or returns unsatisfiable otherwise.

The primary contribution of this work is to study the relative power of the NP oracle and SAT oracle in the context of approximate model counting. We develop a new methodology to achieve the main result: a SAT oracle is no more powerful than an NP oracle in the context of approximate model counting.

(Joint work with Diptarka Chakraborty, Sourav Chakraborty, and Kuldeep S Meel. Based on the ICALP 2023 paper: https://drops.dagstuhl.de/storage/00lipics/lipics-vol261-icalp2023/LIPIcs.ICALP.2023.123/LIPIcs.ICALP.2023.123.pdf).

Venue: A3 117

Speaker Bio

Gunjan Kumar did his B.Tech in Computer Science and Engineering from the Indian Institute of Technology, Guwahati. Thereafter, he pursued his MS and Ph.D. from Tata Institute of Fundamental Research, Mumbai, and currently, he is a postdoctoral researcher at the National University of Singapore. His broad area of interest is algorithms and combinatorial optimization with a focus on sublinear algorithms. Recently, his research has been centered on statistical estimation problems in small-sample regimes.

Webpage: https://sites.google.com/view/gunjankumar