An FPRAS for Model Counting for Non-Deterministic Read-Once Branching Programs

TL;DR

This paper introduces the first Fully Polynomial Randomized Approximation Scheme (FPRAS) for model counting in non-deterministic read-once branching programs, advancing the efficiency of approximate counting in complex Boolean function representations.

Contribution

The paper presents the first FPRAS for #nFBDD, utilizing novel analysis techniques to improve approximation methods for non-deterministic read-once branching programs.

Findings

First FPRAS for #nFBDD problem

New analysis techniques for sampling dependence

Improved efficiency in approximate model counting

Abstract

Non-deterministic read-once branching programs, also known as non-deterministic free binary decision diagrams (nFBDD), are a fundamental data structure in computer science for representing Boolean functions. In this paper, we focus on #nFBDD, the problem of model counting for non-deterministic read-once branching programs. The #nFBDD problem is #P-hard, and it is known that there exists a quasi-polynomial randomized approximation scheme for #nFBDD. In this paper, we provide the first FPRAS for #nFBDD. Our result relies on the introduction of new analysis techniques that focus on bounding the dependence of samples.