Phase C of the joint-width UCQ compiler: a UCQ-specialised homomorphism-type DP that runs directly over a tree decomposition of the joint encoding, emitting a certified d-D (deterministic, decomposable circuit) by construction. More...

#include <cstddef>
#include <map>
#include <unordered_map>
#include <utility>
#include <vector>
#include "JointEncoding.h"
#include "TreeDecomposition.h"
#include "dDNNF.h"

Include dependency graph for UCQJointCompiler.h:

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

Go to the source code of this file.

Classes
struct	Atom
	One atom of a conjunctive query: a relation symbol applied to query variables. More...
struct	CQ
	One conjunctive query (a disjunct of the UCQ). More...
struct	UCQ
	A union of conjunctive queries. More...
class	UCQJointCompiler
	Compiles a Boolean UCQ over a joint encoding into a certified d-D, along a tree decomposition of the joint graph. More...
struct	UCQJointCompiler::Stats
	Structural statistics of a compilation, for diagnostics and tests. More...
struct	UCQJointCompiler::Result
	A compiled UCQ: the d-D and its statistics. More...
struct	UCQJointCompiler::AnswerRoot
	Per-answer evaluation by a single top-down DP (data-graph regime). More...
struct	UCQJointCompiler::AnswerCircuit

Detailed Description

Phase C of the joint-width UCQ compiler: a UCQ-specialised homomorphism-type DP that runs directly over a tree decomposition of the joint encoding, emitting a certified d-D (deterministic, decomposable circuit) by construction.

This is the data-side counterpart of ProvSQL's circuit-side treewidth exploitation, and the UCQ counterpart of ReachabilityCompiler: a bag-by-bag dynamic program whose state carries, for each disjunct, the set of partial homomorphisms realised by the facts of the processed subtree (the correlated regime additionally carries in-bag gate valuations). It is the operational form of the thesis's \(\exists T\, q''(T) \wedge q_{wf}(T)\) rewriting (Amarilli, PhD thesis tel-01345836, Prop. 4.2.9): rather than guessing the set T of true gates with a second-order variable, the DP enumerates per-bag valuations, with mutual exclusivity giving determinism for free.

Each transition emits d-D gates directly:

states at a node are mutually exclusive and exhaustive over the valuations of the world variables introduced in its subtree (every world induces exactly one (hom-set, sat) state), so every OR gate is deterministic by construction;
each world 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 feeds straight to dDNNF::probabilityEvaluation() (the marginal of an irrelevant world variable folds to a unit factor, exactly as in the reachability compiler, so the strictly-non-smooth circuit still evaluates correctly). For a joint encoding of width \(k\) and a UCQ whose disjuncts have at most \(e\) enumerating variables, the DP state is bounded by a function of \(k\) and \(e\) alone, giving exact probability of a #P-hard UCQ in time linear in the data.

The exponential parameter is the number of enumerating variables (existential join variables outside the key/FD determination closure), not n_vars; the design target is queries with at most 4-5 of them.

Definition in file UCQJointCompiler.h.

Classes

Detailed Description