ReachabilityCompiler.h File Reference

Decomposition-aligned compilation of two-terminal reachability over bounded-treewidth data into a d-D. More...

#include <cstddef>
#include <stdexcept>
#include <string>
#include <vector>
#include "dDNNF.h"
#include "TreeDecomposition.h"

Include dependency graph for ReachabilityCompiler.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	ReachabilityCompilerException
	Exception thrown when reachability compilation fails. More...
class	ReachabilityCompiler
	Compiles s-t reachability over a probabilistic edge relation into a d-D, along a tree decomposition of the data graph. More...
struct	ReachabilityCompiler::EdgeRow
	One row of the edge relation. More...
struct	ReachabilityCompiler::Stats
	Structural statistics of a compilation, for diagnostics and tests. More...
struct	ReachabilityCompiler::Result
	A compiled reachability query: the d-D and its statistics. More...
struct	ReachabilityCompiler::VertexRoot
	One vertex's reachability circuit in an all-targets compilation. More...
struct	ReachabilityCompiler::AllResult
	An all-targets compilation: one shared d-D, one root per reachable vertex. More...
struct	ReachabilityCompiler::VertexHopRoot
	One (vertex, walk length) circuit of a bounded-hop compilation. More...
struct	ReachabilityCompiler::AllHopsResult
	A bounded-hop all-targets compilation. More...
struct	ReachabilityCompiler::AnyReachAllResult
	A multi-set any-reach compilation: one shared circuit, one root per target set. More...
struct	ReachabilityCompiler::SourceArc
	One source of a multi-source compilation. More...

Detailed Description

Decomposition-aligned compilation of two-terminal reachability over bounded-treewidth data into a d-D.

Implements the data-side counterpart of ProvSQL's circuit-side treewidth exploitation: instead of building a provenance circuit along the relational-algebra plan (whose treewidth can grow with the instance size) and decomposing it afterwards, the provenance of s-t reachability is built along a tree decomposition of the data graph itself, in the spirit of the provenance refinement of Courcelle's theorem (Amarilli, Bourhis & Senellart, ICALP 2015 / ICDT 2017).

The construction is a bag-by-bag dynamic program whose state at a decomposition node is the transitively-closed reachability relation over the bag's vertices augmented with the two terminals s and t (equivalently, the standard DP over the decomposition obtained by adding s and t to every bag). Each transition emits d-D gates directly:

• states at a node are mutually exclusive and exhaustive over the valuations of the edge variables introduced in its subtree, so every OR gate is deterministic by construction;
• each edge variable is introduced at exactly one node, so the children of every AND gate mention disjoint variable sets and the circuit is decomposable by construction.

No knowledge-compilation step is therefore needed: the result is fed straight to dDNNF::probabilityEvaluation(). For data of treewidth \(k\) the d-D has size linear in the number of edges (times a function of \(k\) only), which yields linear-time exact computation of two-terminal network reliability – a #P-hard problem in general – on bounded-treewidth probabilistic graphs, including cyclic graphs that the recursive-query fixpoint cannot handle.

Directed reachability and undirected connectivity are both supported: the DP state is a reachability relation (not a partition), so the undirected case is simply the directed case with each edge contributing both arcs.

Definition in file ReachabilityCompiler.h.