Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Ranked Enumeration for MSO on Trees via Knowledge Compilation

Antoine Amarilli, Pierre Bourhis, Florent Capelli, Mikaël Monet

TL;DR

This work investigates ranked enumeration for MSO queries on trees using knowledge-compiled circuits. It develops efficient algorithms for enumerating satisfying assignments in nonincreasing order of a subset-monotone ranking, first for smooth multivalued DNNFs with no preprocessing and then for smooth multivalued d-DNNFs with linear preprocessing and logarithmic delay. The approach leverages Lawler-Murty style conditioning, Brodal queues, and a novel A⊙B enumeration primitive to support decomposition at ∧-gates, with direct application to MSO provenance circuits on trees. The results yield linear-time preprocessing and $O( ext{log}(K+1))$ enumeration delay, providing practical top-k and relevance-driven MSO query evaluation on trees under a fixed query, with extensions discussed for updates and broader ranking schemes.

Abstract

We study the problem of enumerating the satisfying assignments for circuit classes from knowledge compilation, where assignments are ranked in a specific order. In particular, we show how this problem can be used to efficiently perform ranked enumeration of the answers to MSO queries over trees, with the order being given by a ranking function satisfying a subset-monotonicity property. Assuming that the number of variables is constant, we show that we can enumerate the satisfying assignments in ranked order for so-called multivalued circuits that are smooth, decomposable, and in negation normal form (smooth multivalued DNNF). There is no preprocessing and the enumeration delay is linear in the size of the circuit times the number of values, plus a logarithmic term in the number of assignments produced so far. If we further assume that the circuit is deterministic (smooth multivalued d-DNNF), we can achieve linear-time preprocessing in the circuit, and the delay only features the logarithmic term.

Ranked Enumeration for MSO on Trees via Knowledge Compilation

TL;DR

This work investigates ranked enumeration for MSO queries on trees using knowledge-compiled circuits. It develops efficient algorithms for enumerating satisfying assignments in nonincreasing order of a subset-monotone ranking, first for smooth multivalued DNNFs with no preprocessing and then for smooth multivalued d-DNNFs with linear preprocessing and logarithmic delay. The approach leverages Lawler-Murty style conditioning, Brodal queues, and a novel A⊙B enumeration primitive to support decomposition at ∧-gates, with direct application to MSO provenance circuits on trees. The results yield linear-time preprocessing and enumeration delay, providing practical top-k and relevance-driven MSO query evaluation on trees under a fixed query, with extensions discussed for updates and broader ranking schemes.

Abstract

We study the problem of enumerating the satisfying assignments for circuit classes from knowledge compilation, where assignments are ranked in a specific order. In particular, we show how this problem can be used to efficiently perform ranked enumeration of the answers to MSO queries over trees, with the order being given by a ranking function satisfying a subset-monotonicity property. Assuming that the number of variables is constant, we show that we can enumerate the satisfying assignments in ranked order for so-called multivalued circuits that are smooth, decomposable, and in negation normal form (smooth multivalued DNNF). There is no preprocessing and the enumeration delay is linear in the size of the circuit times the number of values, plus a logarithmic term in the number of assignments produced so far. If we further assume that the circuit is deterministic (smooth multivalued d-DNNF), we can achieve linear-time preprocessing in the circuit, and the delay only features the logarithmic term.
Paper Structure (17 sections, 6 theorems, 1 equation, 3 algorithms)

This paper contains 17 sections, 6 theorems, 1 equation, 3 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Assignments.
  4. Multivalued circuits.
  5. Ranking functions.
  6. Brodal queues.
  7. Ranked Enumeration for Smooth Multivalued DNNFs
  8. Correctness of the algorithm.
  9. Ranked Enumeration for Smooth Multivalued d-DNNFs
  10. Preprocessing Phase
  11. $A\odot B$ Ranked Enumeration Algorithm
  12. Proof of Claim \ref{['clm:toycorrect']}
  13. Correctness of the Enumeration Phase (Section \ref{['subsec:enum']})
  14. Enumeration Phase
  15. Application to Monadic Second-Order Queries
  16. ...and 2 more sections

Key Result

Lemma 2

A $(D,X)$-ranking function $w$ is subset-monotone if and only if the following holds: for every partial assignments $\tau_1,\tau_2$ and $\sigma_1, \sigma_2$, if $\tau_i$ is disjoint from $\sigma_i$ for each $i \in \{1, 2\}$ and $w(\tau_1) \leq w(\tau_2)$ and $w(\sigma_1) \leq w(\sigma_2)$, then we h

Theorems & Definitions (17)

  • Definition 1
  • Lemma 2
  • Example 3
  • Theorem 4
  • Claim 5
  • Claim 6
  • Theorem 7
  • Definition 8
  • Claim 9
  • Claim 10
  • ...and 7 more