A Circuit-Based Approach to Efficient Enumeration

TL;DR

This paper introduces an efficient enumeration algorithm for satisfying valuations of structured d-DNNF circuits, achieving linear delay proportional to valuation Hamming weight, with applications in database theory and MSO logic evaluation.

Contribution

It presents a novel enumeration algorithm with linear preprocessing and delay linear in Hamming weight for structured d-DNNF circuits, enabling efficient solution enumeration in various AI and database problems.

Findings

Enumeration with linear delay proportional to Hamming weight.

Constant delay enumeration for valuations of constant Hamming weight.

Framework applicable to problems like database query evaluation and MSO logic.

Abstract

We study the problem of enumerating the satisfying valuations of a circuit while bounding the delay, i.e., the time needed to compute each successive valuation. We focus on the class of structured d-DNNF circuits originally introduced in knowledge compilation, a sub-area of artificial intelligence. We propose an algorithm for these circuits that enumerates valuations with linear preprocessing and delay linear in the Hamming weight of each valuation. Moreover, valuations of constant Hamming weight can be enumerated with linear preprocessing and constant delay. Our results yield a framework for efficient enumeration that applies to all problems whose solutions can be compiled to structured d-DNNFs. In particular, we use it to recapture classical results in database theory, for factorized database representations and for MSO evaluation. This gives an independent proof of constant-delay enumeration for MSO formulae with first-order free variables on bounded-treewidth structures.

Figures