Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Kuldeep S. Meel, Alexis de Colnet

TL;DR

The paper resolves the open problem of designing a fully polynomial-time randomized approximation scheme (FPRAS) for #nFBDD, counting models of non-deterministic read-once branching programs. It introduces a bottom-up algorithm, approxMCnFBDD_core, that tracks per-node inverse model counts and uses a median-of-means approach on multiple sample sets, while carefully bounding sample dependence via derivation paths and a novel random-process coupling. The authors prove polynomial-time guarantees and error bounds, culminating in an FPRAS for #nFBDD when coupled with repetition and median aggregation. This work advances knowledge compilation for non-deterministic structures and provides a new technique to quantify dependence in sampling-based approximations, with potential extensions to related languages.

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.

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

TL;DR

The paper resolves the open problem of designing a fully polynomial-time randomized approximation scheme (FPRAS) for #nFBDD, counting models of non-deterministic read-once branching programs. It introduces a bottom-up algorithm, approxMCnFBDD_core, that tracks per-node inverse model counts and uses a median-of-means approach on multiple sample sets, while carefully bounding sample dependence via derivation paths and a novel random-process coupling. The authors prove polynomial-time guarantees and error bounds, culminating in an FPRAS for #nFBDD when coupled with repetition and median aggregation. This work advances knowledge compilation for non-deterministic structures and provides a new technique to quantify dependence in sampling-based approximations, with potential extensions to related languages.

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.
Paper Structure (16 sections, 19 theorems, 41 equations, 7 algorithms)

This paper contains 16 sections, 19 theorems, 41 equations, 7 algorithms.

Table of Contents

  1. Introduction
  2. Background
  3. Related Work
  4. Technical Overview
  5. Algorithm
  6. Derivation paths
  7. The Framework for the Analysis
  8. History
  9. Random Process
  10. Analysis
  11. Proof of Lemma \ref{['lemma:proba_p(q)']}
  12. Proof of Lemma \ref{['lemma:proba_S(q)']}
  13. Conclusion
  14. Appendix
  15. Proof of Lemma \ref{['lemma:not_so_black_magic']}
  16. ...and 1 more sections

Key Result

Theorem 1

Let $B$ be an nFBDD over $n$ variables, $\varepsilon > 0$ and $\delta > 0$. Algorithm $\textup{approxMCnFBDD}(B,\varepsilon,\delta)$ runs in time $O(n^{11}|B|^{10}\varepsilon^{-4}\log(\delta^{-1}))$ and returns $\mathsf{est}$ with the guarantee that

Theorems & Definitions (34)

  • Theorem 1
  • Lemma 1
  • proof : Proof sketch
  • Definition 1
  • Lemma 2
  • proof
  • Definition 2
  • Lemma 3
  • proof
  • Lemma 4
  • ...and 24 more