Probability Evaluation

ProvSQL computes probabilities by reducing a provenance circuit to Boolean form and then dispatching to one of several evaluation methods. This page explains the dispatch architecture, gives the background on the central data structures (d-DNNF, Tseytin encoding, weighted model counting, tree decomposition), and ends with a step-by-step guide for adding a new method. See Probabilities for the user-facing description of the existing methods.

The continuous-random-variable surface layers an analytical / hybrid path on top of this Boolean machinery; the architecture of that layer is documented separately in Continuous Distributions. The sections below cross-link to the relevant arms of the hybrid evaluator and the conditional inference path.

Architecture

The entry point is the SQL function probability_evaluate, which calls provenance_evaluate_compiled on the C++ side. That function builds a BooleanCircuit object from the persistent circuit store and then calls probability_evaluate_internal (in probability_evaluate.cpp).

probability_evaluate_internal receives the method name (or the requested guarantee) and dispatches through the MethodCatalog singleton: each method is a ProbabilityMethod subclass registered with MethodCatalog::registerMethod at static-initialisation time, and the catalog either resolves an explicitly named method or runs its cost-based chooser over the admissible ones. Two declarative flags shape the dispatch: handlesMultivalued() (the BID → Boolean rewrite of gate_mulinput blocks is applied centrally before any method that does not handle blocks natively – only independent opts out), and producesDD() / buildDD() for the d-DNNF constructors the makeDD auto route selects among. Two gate types short-circuit the chooser entirely: a gate_conditioned root is evaluated as the conditional P(target ∧ evidence) / P(evidence), and a gate_mobius root is non-Boolean and routes directly to the mobius method (see below).

Background: d-DNNF, Tseytin, Knowledge Compilation

Computing the probability that a Boolean formula evaluates to true when its variables are assigned independently is $\#\mathrm{P}$ -hard in general, but tractable for structured representations. The two structures ProvSQL exploits are d-DNNF and tree decomposition, both of which give linear-time probability evaluation in the size of the structure. The methods that ship with ProvSQL all reduce to one or the other.

d-DNNF

A deterministic decomposable negation normal form (d-DNNF) is a Boolean circuit built from AND, OR, NOT, and variable leaves, satisfying two structural properties:

Decomposability: for every AND gate, the variable sets of its children are pairwise disjoint. This means the children represent independent events, and the probability of the AND is the product of the children’s probabilities.
Determinism: for every OR gate, the children represent mutually exclusive events. This means the probability of the OR is the sum of the children’s probabilities – no inclusion- exclusion correction is needed.

Together these two properties make a single bottom-up traversal sufficient to compute the probability: dDNNF::probabilityEvaluation does exactly that. The implementation in dDNNF.cpp uses an explicit stack instead of recursion to avoid blowing the call stack on very deep circuits, and memoises intermediate results so that shared sub-circuits are evaluated only once.

A general Boolean formula is not a d-DNNF. Producing a d-DNNF from an arbitrary formula – knowledge compilation – is the expensive part; once you have it, evaluation is cheap. The compilation and tree-decomposition branches of the dispatcher both end in a dDNNF object that dDNNF::probabilityEvaluation then walks.

Tseytin Encoding

External knowledge compilers (d4, c2d, dsharp, minic2d) and the weightmc model counter all consume Boolean formulas in DIMACS CNF format. Producing CNF from a ProvSQL Boolean circuit is the job of BooleanCircuit::TseytinCNF (in BooleanCircuit.cpp), whose string output each caller writes into its own @c provsql::ScopedTempDir before invoking the tool.

The Tseytin transformation introduces one fresh variable per internal gate of the circuit, then writes a small set of clauses that encode the gate’s semantics. For an AND gate $g = s_1 \wedge s_2 \wedge \dots \wedge s_n$ , that’s one binary clause $(\neg g \vee s_i)$ for every child, plus one big clause $(g \vee \neg s_1 \vee \neg s_2 \vee \dots \vee \neg s_n)$ . OR is dual. NOT becomes two two-literal clauses. A unit clause forcing the root variable true is added at the end.

For weighted model counting (and the d4 compiler when built with weight support), Tseytin also emits one w line per leaf variable giving the probability of the corresponding ProvSQL input gate – so the SAT-side of the pipeline knows the weights to multiply through.

The output is dumped to a temporary file under /tmp; BooleanCircuit::compilation then invokes the chosen compiler with that file and reads the result back. The invocation goes through run_external_tool (external_tool.cpp), which honours the provsql.tool_search_path GUC by prepending its value to PATH for the duration of the call. The tool runs via /bin/sh -c in its own process group: while it runs the backend polls for a pending cancel, and on statement_timeout / pg_cancel_backend it SIGKILLs the whole group (so a tool that ignores SIGINT or forks a worker into another process group, as KCBox/Panini does, is still stopped) and then raises the interrupt via CHECK_FOR_INTERRUPTS. Before composing the command line, the same call site pre-flights the binary with find_external_tool, so a missing tool fails with an actionable error rather than letting the shell return exit 127. After the call, the wait status is decoded by format_external_tool_status to distinguish “not found”, “killed by signal”, and “ran and exited nonzero”. The same trio is used by BooleanCircuit::wmcCount for the weighted model counters and by DotCircuit::render for graph-easy.

Knowledge Compilers and the NNF Format

All four supported external compilers (d4, c2d, dsharp, minic2d) produce a d-DNNF in the NNF text format – a line-oriented representation where each line is one node:

L lit – a leaf literal (positive or negative).
A k c1 c2 ... – an AND of $k$ children, given by their node indices.
O k c1 c2 ... – an OR of $k$ children.

Modern d4 also emits a few extra node kinds (a / o / f / t for constants, and a decision-tree variant); the parser in BooleanCircuit::compilation handles both the legacy and the d4-extended dialects. The result is a BooleanCircuit (with the d-DNNF invariants) that gets returned to the caller and walked by dDNNF::probabilityEvaluation.

The Panini compiler from KCBox ships with five target-language modes (OBDD, OBDD[AND], Decision-DNNF, R2-D2, CCDD) selected by the --lang flag. ProvSQL exposes the first three; the R2-D2 and CCDD languages are rejected upstream because both emit K (kernelize) nodes encoding literal-equivalence constraints over a shared kernel variable, breaking the decomposability invariant of the resulting d-DNNF. Panini’s output is not the NNF text format but a CDD-style DOT-like syntax; the panini-* registry records run the same generic compile path as the other compilers but tag their output panini-dd, so BooleanCircuit::compilation reads them back with BooleanCircuit::parsePaniniDD instead of the NNF parser. It translates each C / D line into a decomposable AND and each v ? t : f decision into an explicit OR-of-AND-NOT structure over the corresponding input gate. A K node, if seen, raises an explicit error.

After any external-compiler call, dDNNF::simplify runs a single canonical pass over the result: empty-constant folding, short-circuiting on opposite-type empty children, and single-child AND / OR collapse. The same pass is run on the in-process tree-decomposition route and on BooleanCircuit::interpretAsDD, so callers see a structurally canonical d-DNNF regardless of which backend produced it.

Helper Surfaces (Studio and SQL Introspection)

Four small SQL helpers expose intermediate pipeline artifacts to the user and to Studio:

tseytin_cnf.cpp (tseytin_cnf) returns the DIMACS CNF that the external compilers would otherwise receive.
tree_decomposition_dot.cpp (tree_decomposition_dot) renders the min-fill tree decomposition as GraphViz DOT, with the treewidth and a per-bag input map embedded as comment lines so consumers can resolve a bag variable back to its provenance UUID.
compile_to_ddnnf_dot.cpp (compile_to_ddnnf_dot) goes one step further: it runs the requested compiler (or the meta-routes tree-decomposition, interpret-as-dd, default – all dispatched through BooleanCircuit::makeDD) and returns the resulting d-DNNF itself as DOT.
tool_available.cpp (tool_available) is a thin wrapper around find_external_tool so a SQL client can check whether a given tool resolves on the backend’s PATH plus provsql.tool_search_path – used by Studio to grey out unselectable compilers in the picker.

None of these helpers participate in the probability dispatcher; they are purely introspection surfaces sharing the same Tseytin / NNF / tree-decomposition primitives as the production methods.

Weighted Model Counting

BooleanCircuit::wmcCount drives every weighted model counter through one registry-selected path: it looks the named tool up in the external-tool registry (or, with no tool named, picks the highest-preference counter whose binary resolves on PATH), writes the weighted CNF in the dialect the record’s parser implies, runs the record’s command template, and reads the count back the same way. Two conventions are understood: MCC-2024 weighted DIMACS with a c s exact result line (ganak, sharpsat-td, dpmc), and the WeightMC approximate counter’s own dialect, whose "delta;epsilon" precision argument is turned into a --pivotAC value controlling how many random hash constraints it samples. Unlike a knowledge compiler none of these produce a d-DNNF; each returns a single probability the function parses as a double.

Tree Decomposition

The tree-decomposition path is ProvSQL’s “no external tool” route to a d-DNNF. Conceptually, a tree decomposition of a Boolean circuit is a tree of bags (sets of variables) such that every constraint of the circuit is captured by at least one bag, and the bags containing each variable form a connected subtree. The treewidth is one less than the size of the largest bag; the smaller it is, the more amenable the formula is to dynamic programming.

TreeDecomposition.cpp builds a tree decomposition of the circuit’s primal graph using a min-fill elimination heuristic, then normalises it (TreeDecomposition::makeFriendly) so that every bag has at most two children and every leaf bag introduces exactly one variable. dDNNFTreeDecompositionBuilder.cpp then walks the bag tree bottom-up, enumerating per-bag truth assignments and gluing them into a d-DNNF whose decomposability and determinism follow from the bag-cover structure of the decomposition. The worst-case cost is $O(2^{w+1} \cdot |\mathit{circuit}|)$ , which is why ProvSQL caps the treewidth at TreeDecomposition::MAX_TREEWIDTH (currently 10) and falls back to compilation with d4 when that bound is exceeded. The two treewidth heuristics ProvSQL relies on – the cheap degeneracy lower bound (used for the cost estimate that drives the chooser, see below) and the min-fill upper bound (the elimination ordering that builds the decomposition here) – are chosen following the experimental study of real-world graph treewidth of [Maniu et al., 2019].

Both the min-fill elimination loop in the TreeDecomposition constructor and the bottom-up d-DNNF construction in dDNNFTreeDecompositionBuilder::builddDNNF call CHECK_FOR_INTERRUPTS in their hot loops so that statement_timeout and pg_cancel_backend interrupt the build promptly when the heuristic struggles on circuits close to MAX_TREEWIDTH. The macro is conditionally compiled to a no-op in the standalone tdkc binary via a TDKC guard.

Currently Supported Methods

Method string	Implementation
`"independent"`	`BooleanCircuit::independentEvaluation` – exact, linear time when every input gate appears at most once.
`"possible-worlds"`	`BooleanCircuit::possibleWorlds` – exact enumeration of all $2^n$ worlds; capped at 64 inputs.
`"monte-carlo"`	`BooleanCircuit::monteCarlo` – approximate via random sampling. The argument is a fixed count (`samples=N` or a bare integer) or an additive `(eps,delta)` target, for which `N = ceil(ln(2/delta)/(2*eps^2))` (Hoeffding, independent of the estimated probability).
`"karp-luby"`	The Karp-Luby `#DNF` FPRAS, whose sample complexity is independent of the estimated probability (accurate on rare events, unlike naive Monte Carlo). `BooleanCircuit::dnfShape` first checks the circuit is a monotone OR-of-ANDs over input leaves (cross-clause leaf sharing allowed) and extracts the clause supports; the dispatcher errors, rather than falling back, on any other shape. Two estimators, selected by the argument (`evaluate_karp_luby` does the routing): a fixed `samples=N` runs the stratified fixed-budget estimator `BooleanCircuit::karpLuby` (rounds allocated across clauses proportionally to $p_i/S$ , removing the categorical clause-draw variance); an adaptive `epsilon=E[,delta=D][,max_samples=M]` target (default `epsilon=0.1, delta=0.05`) runs the Dagum-Karp-Luby-Ross self-adjusting stopping rule `BooleanCircuit::karpLubyStopping` (sample until the accept count reaches $\Upsilon_1 = 1+(1+\epsilon)\,4(e-2)\ln(2/\delta)/\epsilon^2$ , so the round count adapts to the true acceptance probability $\Pr[F]/S \in [1/m,1]$ – up to `m` times fewer rounds than the fixed worst-case bound). The cap defaults to that fixed bound ( $\lceil\Upsilon_1 m\rceil$ ); reaching it before the target downgrades the guarantee to the relative `eps` achieved at the spent budget.
`"wmc"`	`BooleanCircuit::wmcCount` – weighted model counting via the registered counter named in the argument (`tool[;tool_args]`: `ganak`, `sharpsat-td`, `dpmc`, `weightmc`, or any registered `wmc` tool). With no tool named it selects the highest-preference available counter.
`"weightmc"`	Backward-compatible alias for `"wmc"` with the `weightmc` tool. Takes `epsilon=E[,delta=D]` (validated through the same `parse_eps_delta` as the sampling methods) or, as a legacy alias, the `delta;epsilon` pair.
`"tree-decomposition"`	Builds a `TreeDecomposition` (bounded by `TreeDecomposition::MAX_TREEWIDTH`) and uses `dDNNFTreeDecompositionBuilder` to construct a d-DNNF, then calls `dDNNF::probabilityEvaluation`. Speculative execution: the cost estimate uses the degeneracy lower bound, which under-costs; the min-fill build then discovers the exact treewidth, so before the `2^w` d-DNNF step the method recomputes the real cost and – if it exceeds the next-best method’s (`cost_budget`) – throws so the chooser escalates (the `MAX_TREEWIDTH` cap remains the hard ceiling). By-name calls run unbounded.
`"d-tree"`	The Olteanu-Huang-Koch anytime interval-bounds engine ([Olteanu et al., 2010], `src/DTree.cpp`): a cheap certified leaf bound refined by independent-component decomposition and Shannon expansion until `upper-lower <= max_width` – exact at width 0, a certified additive / relative interval otherwise, and deterministic (the only non-exact method admissible for a `delta = 0` request). A monotone DNF takes the optimised clause path `dtreeBounds` (leaf bound `BooleanCircuit::dnfBounds`); any other circuit (negation / `EXCEPT`, nested `AND`/`OR`, arbitrary sharing) takes the general DAG recursion `dtreeBoundsCircuit`, whose leaf bound generalises `dnfBounds` soundly to any gate – independent components (disjoint input cones) compose exactly, an entangled `AND` uses a Bonferroni lower / `min` upper, an `OR` a `max` lower / union upper, and `NOT` the exact flip `[1-U, 1-L]`. Exact mode adds component memoisation over the canonical subproblem; a multivalued (`MULIN` / BID) gate makes it throw, so the chooser falls back. In the default chain it competes for exact only on the monotone-DNF path (and where tree-decomposition bails); the general recursion serves the approximate / `delta = 0` paths and explicit by-name calls. Speculative execution: because d-tree cost is treewidth-driven and not predictable from cheap features (a calibration sweep confirmed depth / `S` / `N` do not track it, and the approximate cost is nearly `eps`-independent), the chooser runs it under a subproblem budget set to the next-best admissible method’s estimated cost (`EvalContext::cost_budget` → a count via `kCostDTreeMsPerStep`); a counter in the recursion throws `"cost budget exceeded"` on overrun and the chooser’s `catch` escalates – bounding wasted work at ~the safe fallback’s cost (deterministic, so selection is reproducible). The debug GUC `provsql.dtree_max_subproblems` adds a hard cap.
`"compilation"`	`BooleanCircuit::compilation` – invokes the registered knowledge compiler named in the argument (`d4`, `d4v2`, `c2d`, `minic2d`, `dsharp`, `panini-*`), or, with no compiler named, the highest-preference available one, to produce a `dDNNF`, then `dDNNF::probabilityEvaluation`.
`"mobius"`	`mobius_evaluate.cpp` – exact route for a `gate_mobius`-rooted token (the safe-UCQ Möbius-inversion route): one linear sweep evaluates each certified-independent island read-once and combines the island probabilities with the persisted signed integer coefficients. A Möbius root is non-Boolean, so the dispatcher routes it here directly; naming `mobius` on any other token is an error, while naming any other method on a Möbius root evaluates the transparent lineage child instead (same value, no shortcut).
`""` (default)	Fallback chain: try `independent`; then, when the root carries an inversion-free certificate and `provsql.inversion_free` is on, the `inversion-free` structured-d-DNNF builder (see The Inversion-Free UCQ(OBDD) Path); then `BooleanCircuit::interpretAsDD` (interpret the circuit structure directly as a d-D circuit), then `tree-decomposition`, then `compilation` with the preference-ranked fallback compiler (`provsql.fallback_compiler` when available, otherwise the highest-preference compiler whose binary resolves on PATH).

The branches for "compilation", "tree-decomposition", and the default all funnel through BooleanCircuit::makeDD, which dispatches further on the d-DNNF construction strategy.

The external-compiler choice inside compilation resolves the named tool against the external-tool registry, which supplies its executable, command template and output parser. Once a dDNNF has been produced, probability evaluation is a single linear-time pass (dDNNF::probabilityEvaluation), because the d-DNNF structure guarantees decomposability and determinism.

Cost-selecting the d-DNNF construction route (makeDD `auto`)

Callers that need the d-DNNF artifact rather than a probability – shapley / banzhaf / shapley_all_vars (and ProvSQL Studio’s Contributions mode) – historically asked BooleanCircuit::makeDD for a fixed interpret-as-dd → tree-decomposition → compiler ladder. Those three routes are already first-class, cost-modelled members of the probability method catalog (InterpretAsDdMethod / TreeDecompositionMethod / CompilationMethod), so rather than carry a second optimizer they share the catalog’s chooser: each d-D method overrides producesDD() and factors its build into buildDD() (with evaluate() reduced to buildDD(ctx).probabilityEvaluation()), and MethodCatalog::chooseAndBuildDD runs the same uniform-cost search as chooseAndRun over the producesDD() portfolio, returning the artifact. provsql::makeDDAuto is the thin entry point (it builds an EvalContext from the Boolean view alone, since these routes need no generic-circuit state). interpret-as-dd – the artifact twin of independent, same O(S) computation – carries the same O(S) cost so it is ranked first and falls through (by throwing, dropped by the chooser) on a non-read-once circuit, exactly as the ladder did.

This is the default route for the d-D-artifact callers (the empty method, default and auto all map to it); the old fixed ladder stays reachable as ladder. It is not wired into the KC-inspection surfaces (compile_to_ddnnf / ddnnf_stats / compile_to_ddnnf_dot): those serialise via toNNF / report compiler stats and require a compiler-style d-DNNF in negation normal form, which interpret-as-dd’s internal NOTs violate, so they keep the external-compilation default.

Per-gate d-DNNF certificates and the island discipline

A gate_plus / gate_times gate whose info1 carries the persisted certificate bits is deterministic / decomposable by construction – stamped by the reachability and joint-width compilers and by the certified HAVING enumerations. independent and interpret-as-dd consume the certificates through an island discipline: inside a certified region, sharing is licensed (the gate is evaluated once and its probability reused), while an input shared across two distinct islands – cross-island entanglement the certificates cannot vouch for – throws, falling back to the general methods. The island walk is iterative (path-like certified circuits are as deep as the data) and registers a BID block’s key variable once per island, so repair_key circuits stay on the linear route.

The approximate methods (monte-carlo, karp-luby, and weightmc / wmc with an approximate counter) return an estimate that carries an (eps, delta) error guarantee. probability_evaluate.cpp surfaces it as a single machine-readable NOTICE so a UI can render it without re-deriving the bound:

ProvSQL: approximation-guarantee: kind=<relative|additive> eps=<E> \
    [delta=<D>] [samples=<N>] [clauses=<M>] [tool=<name>]

emitted by the emit_guarantee helper. kind=relative is a multiplicative guarantee (the estimate is within a factor 1 ± eps of the true probability with probability at least 1 - delta), used by karp-luby (over M clauses) and the approximate weighted counters; kind=additive is the absolute Hoeffding bound (|estimate - p| <= eps) used by monte-carlo. samples is the actual sample count: a fixed budget, the Hoeffding count on monte-carlo’s adaptive path, or – for karp-luby’s stopping rule – the number of rounds the run actually took before the accept count crossed the threshold. The fields are omitted when not applicable (no delta for the weighted counters, no samples / clauses for the external tools).

The NOTICE is gated on provsql.verbose_level >= 5 so plain SQL evaluation and the regression suite stay quiet; ProvSQL Studio raises the level to 5 for evaluation and parses the NOTICE into the eval-strip bound, but its probability benchmark drops it (it is per-method UI metadata, not a benchmark row).

Cmp-Probability Pre-Passes

Before the methods above run, probability_evaluate.cpp walks the circuit through a chain of pre-passes that resolve specific gate_cmp shapes to a Bernoulli gate_input carrying a closed-form probability. Resolving a cmp here shrinks the circuit fed to the downstream method ; in the best case the whole HAVING comparator collapses to a single leaf, bypassing DNF construction entirely.

The chain (in order) :

runRangeCheck (also runs at load time when provsql.simplify_on_load is on) : support-interval propagation through gate_arith and decision of every gate_cmp decidable from the support alone. Universal across semirings, so it lives both at load time and inside probability_evaluate.
runHybridDecomposer (gated by provsql.hybrid_evaluation) : base-RV-footprint partitioning + per-island marginalisation for continuous-RV cmps (see the hybrid section below).
runAnalyticEvaluator : closed-form CDF for trivial RV cmp shapes (singleton bare gate_rv vs gate_value, or two bare normals). Probability-specific (the resulting gate_input carries a numeric probability with no semiring meaning), so it runs here and not at load time.
runCountCmpEvaluator (gated by provsql.cmp_probability_evaluation, hidden diagnostic default on) : recognises HAVING gate_cmp(gate_agg(COUNT, semimod children), gate_value(C)) and replaces the cmp with a Bernoulli carrying the Poisson-binomial CDF Pr(B op C) over the per-row contributor marginals. Each semimod’s K child is that row’s contributor sub-circuit – a single gate_input, or (for a join) a times / plus / monus of several leaves; a small read-once recursion (contributorProb) computes its probability. Soundness condition : every structural gate inside a contributor (input / times / plus / monus) has ref_count == 1 – a single check that makes the contributors’ leaf sets pairwise disjoint, unshared with the rest of the circuit, and read-once, so the Poisson-binomial trials are independent (plus ref_count(gate_agg) == 1, catching multi-cmp HAVING over a shared COUNT). The DP dispatches on the smaller side of C (lower tail directly, or upper tail via inverted Bernoullis) for O(N x min(C, N - C)) total cost per cmp. See src/CountCmpEvaluator.{h,cpp}.
runMinMaxCmpEvaluator (same gate provsql.cmp_probability_evaluation) : recognises HAVING gate_cmp(gate_agg(MIN|MAX, semimod children), gate_value(C)) and replaces the cmp with a Bernoulli carrying the closed-form Pr(MIN/MAX(a) op C). Where the COUNT path needs a Poisson-binomial DP, MIN / MAX need none : partition the children on their per-row value m_i against C, and the answer is a product of (1 - p_i) factors (MAX >= C is 1 - prod(1 - p_i) over m_i >= C, MIN >= C is prod(1 - p_i) over m_i < C times the non-empty factor, and so on for all twelve (MIN|MAX, op) combinations, the empty group excluded as in COUNT). Same shape match and independence certification as runCountCmpEvaluator – both share src/CmpEvaluatorCommon.{h,cpp} (matchAggCmp / computeRefCounts / contributorProb). See src/MinMaxCmpEvaluator.{h,cpp}.
runSumCmpEvaluator (same gate provsql.cmp_probability_evaluation) : recognises HAVING gate_cmp(gate_agg(SUM, semimod children), gate_value(C)) and replaces the cmp with a Bernoulli carrying Pr(SUM(a) op C). The running sum of the present rows’ integer weights m_i is a weighted Poisson-binomial ; its full distribution dp[s] = Pr(sum = s) is built by a subset-sum convolution over the reachable range [sum of negative m_i, sum of positive m_i], and the answer is sum_{s : s op C} dp[s] minus the empty-group world (whose empty sum is 0). Cost O(N x R) with R the range – pseudo-polynomial (R is linear in the weight magnitudes, hence exponential in their bit-length), so the pass declines above a range cap and falls back to the general path. Same shape match and independence certification as the COUNT / MIN-MAX evaluators (shared CmpEvaluatorCommon). See src/SumCmpEvaluator.{h,cpp}.

Adding another closed-form cmp resolver (future discrete-RV distributions…) follows the same shape : a runXxxEvaluator function that walks gate_cmp gates, checks shape + independence (reusing CmpEvaluatorCommon), computes the probability, calls GenericCircuit::resolveCmpToBernoulli. Gate it on provsql.cmp_probability_evaluation so all such evaluators share one diagnostic switch.

HAVING Query Complexity: the Ré–Suciu Trichotomy

The closed-form HAVING evaluators above (runCountCmpEvaluator, runMinMaxCmpEvaluator, runSumCmpEvaluator) realise the tractable corner of a complexity classification due to Ré and Suciu [Ré and Suciu, 2009] for a HAVING predicate α(y) θ k over a tuple-independent probabilistic database, with α ∈ {MIN, MAX, COUNT, SUM, AVG, COUNT(DISTINCT)} and θ ∈ {=, ≠, <, ≤, >, ≥}. This section is the standing reference for that classification; it outlives any single evaluator.

Two safety properties drive everything:

Skeleton safety – whether sk(Q), the conjunctive query feeding the aggregate (the FROM / WHERE body with the group-by and aggregated variables as head), is a self-join-free hierarchical CQ (Dalvi–Suciu safe, [Dalvi and Suciu, 2012]) – the same property the safe-query rewriter detects (find_hierarchical_root_atoms in src/safe_query.c).
α-safety – a stricter, per-aggregate plan property. For MIN / MAX / COUNT it coincides with skeleton safety; for SUM / AVG (Def. 15) and COUNT(DISTINCT) (Def. 14) it is strictly stronger (e.g. even a single-table SUM is #P-hard – Prop. 5).

The classification is best read as two layers.

Layer 1 – exact computation – is complement-symmetric. Because Pr(α ≠ k) = Pr(nonempty) − Pr(α = k) and likewise Pr(α < k) = Pr(nonempty) − Pr(α ≥ k), Pr(α ≤ k) = Pr(nonempty) − Pr(α > k) – with Pr(nonempty) trivially poly – each operator has the same exact complexity as its complement ([Ré and Suciu, 2009], p. 1102). So = ≡ ≠, < ≡ ≥, ≤ ≡ >, and the exact verdict depends only on the aggregate’s safety, not on θ:

Layer 1 – exact evaluation (all six operators, including `≠`)
Aggregate	`sk(Q)` safe	`sk(Q)` not safe
`EXISTS`	P (read-once; safe-query rewriter)	#P-hard
`MIN` / `MAX` / `COUNT`	P (Thm 1)	#P-hard (Thm 2)
`COUNT(DISTINCT)`	P if CD-safe, else #P-hard (Thm 3/4)	#P-hard (Thm 4)
`SUM` / `AVG`	P if α-safe, else #P-hard (Thm 5/6, Prop 5)	#P-hard (Thm 6)

Layer 2 – approximation – applies only where exact is #P-hard, and is direction-asymmetric. An FPTRAS gives relative error, and a relative approximation of p is not one of 1 − p (a rare event near 0 is the hard one), so complements with identical exact complexity get different approximation verdicts. This is the trichotomy proper – safe / apx-safe (an FPTRAS exists) / hazardous (no FPRAS):

Layer 2 – approximation overlay (only when exact is #P-hard)
`(α, θ)`	verdict	reference
`EXISTS` (third class empty)	apx-safe (always; karp-luby)	1093
`MIN` `<,≤` · `MAX` `>,≥`	apx-safe (any unsafe `sk`)	Thm 8
`MIN` `>,≥,=` · `MAX` `<,≤,=`	hazardous	Lemma 8 / Thm 11
`COUNT` `<,≤,=`	apx-safe / hazardous (decidable)	Thm 11
`COUNT` `>,≥`	open	pp. 1094, 1111
`SUM` `<,≤,>,≥` (`sk` safe, not SUM-safe)	apx-safe	Thm 10
`SUM` `<,≤` (`sk` unsafe)	hazardous	Thm 11
`SUM` `>,≥` (`sk` unsafe)	open	1094
`SUM` `=`	hazardous	1091
`AVG` (all `θ`), `COUNT(DISTINCT)` (all `θ`)	open (§6 covers only MIN/MAX/SUM)	1107
any `≠`	open (excluded from the approximation analysis)	1110

Reading the two layers together (the source figure is Fig. 7, p. 1111, tabulating MIN/MAX/COUNT):

≠ is not open for exact computation – it equals = – but is unclassified for approximation (the paper omits ≠ from §6, p. 1110).
= lies in Θ≤ ∩ Θ≥ (Θ≤ = {≤,<,=}, Θ≥ = {≥,>,=}); for MIN / MAX it resolves to the hazardous side because Thm 8 (the only blanket FPTRAS) lists only the one-sided operators.
MIN / MAX unsafe verdicts are blanket (Thm 8 / Lemma 8); COUNT / SUM with Θ≤ are per-query decidable (Thm 11); COUNT / SUM with {≥, >} and unsafe sk are open.
The trichotomy is proven “for many” – not all – (α, θ) pairs (p. 1093); the open cells above are precisely that gap.

EXISTS is the degenerate baseline, and ProvSQL already implements all of it. The paper’s sixth aggregate, EXISTS, only tests group non-emptiness – i.e. the plain Boolean conjunctive query – so it carries no operator at all and its third (hazardous) class is empty: every Boolean CQ has an FPTRAS (p. 1093). In ProvSQL this is not a gate_cmp case but the default provenance of any grouped / projected tuple: the gate_plus (OR) over the contributing tuples’ tokens, whose probability is just Pr(lineage is true). Its HAVING form COUNT(*) >= 1 is provably true on any non-empty group and is collapsed straight back to that OR by the always-true rewriter (runHavingAlwaysTrueRewriter -> GenericCircuit::resolveCmpToPlusOfKGates). So EXISTS is covered end-to-end by the core pipeline – safe-query rewriter then independentEvaluation when sk(Q) is safe (P), tree-decomposition / d4 when it is not (#P-hard exact), and karp-luby for the always-available FPTRAS (apx-safe) – with no dedicated HAVING evaluator. It is the baseline the other five aggregates generalise.

What ProvSQL implements. The closed-form pre-passes (runCountCmpEvaluator / runMinMaxCmpEvaluator / runSumCmpEvaluator) compute the P / α-safe corner exactly for independent private contributors (the read-once independence certification in CmpEvaluatorCommon, a sufficient condition for α-safety on a per-instance basis). runAggMarginalEvaluator (src/AggMarginalEvaluator.cpp) extends this exact corner to the hierarchical (laminar) join: a recursive marginal-vector engine that, at each level, factors a block’s common root event (the ⊥ mixture), convolves independent blocks (⊛⁺), and at a common-less Cartesian product node R(a),S(a,b),T(a,c) multiplies the per-factor counts. There a SUM whose value lives on one factor is S_f · M; a branch-spanning but additively separable value (e.g. sum(b+c)) is Σ_f sum_f · ∏_{g≠f} cnt_g, folded exactly from the per-factor joint (sum,count) distributions (sumCountPMF); a multiplicatively separable value (e.g. sum(b*c)) is ∏_f sum_f, the product of the per-factor weighted sums (mulSeparableSumPMF, via a pivot identity so no explicit factorisation is needed). A value that is neither (sum(b*c+b+c)) and a non-laminar shape (the triangle) self-gate back to enumeration. Pinned by test/sql/having_safe_join_{count,agg}.sql.

The same evaluator also covers BID blocks for every aggregate (COUNT / SUM / AVG / MIN / MAX): a repair_key block surfaces as gate_mulinput contributors sharing a block-key child (mutually exclusive, per-alternative probabilities), so each block is handled as a categorical (at most one alternative present, the null arm contributing 0), independent of the TID part. COUNT / SUM / AVG convolve the block’s count / weighted-sum distribution; MIN / MAX fold a per-block factor 1-Σ_{pred} p_alt into each pAllAbsent over a value-thresholded subset. No planner certificate is needed, since the block is visible in the circuit. This is the value-0-present-vs-empty-group corner of test/sql/having_sum_zero.sql, now exercised exactly rather than by enumeration; pinned by test/sql/having_bid.sql. The one residual is a declared key on a plain TID table (mutual exclusion in block_key metadata only, no mulinput), which still falls back.

Finally, a UNION / EXCEPT over a join that re-uses a base tuple yields a non-read-once contributor – (r∧s)∨(r∧t) (a gate_plus) or (r∧s)∖(r∧t) (a gate_monus) repeating the shared r – which the read-once contributorProb rejects. When the contributor’s footprint is private (independent of every other contributor), contributorExactMarginal computes its exact marginal by brute force over its private leaves (resolving the internal sharing exactly) and models it as an independent one-alternative block, reusing the categorical machinery; pinned by test/sql/having_union.sql. A base tuple shared across a group’s contributors is genuinely $\#P$ -hard and falls back to enumeration.

The enumeration itself is certified when it can be. A comparator that reaches provsql_having’s possible-worlds expansion is, when the group’s contributors are independent base literals, a d-DNNF by construction: the complete world terms partition the worlds (a deterministic OR) and each is an AND over distinct literals (decomposable). The Boolean-circuit construction (semiring::BoolExpr, via the Semiring certification hooks) builds it that way and stamps the persisted d-DNNF certificate – the same mark the bounded-treewidth reachability route emits – with the missing-side monus(one, plus(...)) De Morgan-expanded into per-literal negations so the whole enumeration forms one certified island whose contributor sharing across world terms is licensed. The certificate-aware independent method then evaluates these tokens linearly in the enumeration size; this is what makes AVG op constant, arithmetic over several aggregates (sum(a) > 3*count(*)), and choose() = 'text' exact without any dedicated evaluator – shapes the closed-form pre-passes above do not cover. Certification requires the complete enumeration (the upset shortcut and the monotone MIN / MAX skips produce overlapping disjuncts), so the certifying path requests it explicitly, capped at 16 contributors; correlated contributors are never certified and keep their existing routes. Pinned by test/sql/having_certified.sql.

The trichotomy classification above is the standing complexity reference; ProvSQL acts on it only through the evaluators (the exact corner) and the sampler (the apx-safe corner), not through any read-only verdict surface.

The apx-safe corner, in practice. runSumCmpEvaluator is pseudo-polynomial: it declines a SUM whose reachable range exceeds a cap (kMaxSumRange), and the sparse marginal-vector engine declines when the number of distinct aggregate values exceeds kMaxSumSupport. When both decline – a large-magnitude aggregate over many incommensurate values – the comparator survives, and its only exact route, provsql_having’s threshold-lineage expansion, does not terminate in practice. For an (eps,delta) request (relative / additive / monte-carlo) probability_evaluate_internal detects this case with circuitHasUnresolvedSampleableAgg and routes it straight to the GenericCircuit world-sampler (src/MonteCarloSampler.cpp) instead of building the (non-terminating) Boolean view: the relative path runs the DKLR stopping rule monteCarloRVStopping – a relative FPRAS when Pr >= 1/poly – and additive / monte-carlo run fixed-sample monteCarloRV. The sampler’s gate_agg arm pushes each kept contributor’s value into the matching aggregator, reproducing SQL semantics exactly for every aggregate – the value gate is the row’s contribution (the summed term for SUM; the 0/1 indicator for COUNT, 0 for a NULL row so count(x) does not count NULLs; the compared value for AVG / MIN / MAX), so NULL rows are handled and an empty group finalises to the value the exact evaluator uses (0 for SUM / COUNT, NaN -> comparison false for the others) – and for gate_arith over them. In practice only SUM / AVG / MIN / MAX ever reach here: COUNT’s value-support is small (0/1 per row) so it is always resolved exactly and never bails – but it is sample-faithful as well (the arm sums the contributor value gate, not a hard 1), so it is not excluded. The exact (delta = 0) route is unchanged. This realises the apx-safe corner of the trichotomy table above (and, since the sampler evaluates the aggregate per world regardless of join shape, the branch-spanning / shared-tuple residuals too); the rounding-based rejection FPTRAS (Thm 9) would add only rare-event sample efficiency. Pinned by test/sql/having_agg_fptras.sql.

Block-Independent Databases and Multivalued Inputs

By default, add_provenance associates one input gate per tuple (created lazily on first reference), so each row of a provenance-tracked base table is an independent Bernoulli variable. That is the tuple-independent probabilistic database (TID) model.

ProvSQL additionally supports the strictly more general block-independent database (BID) model, in which input tuples are partitioned into blocks:

tuples within a block are pairwise disjoint – at most one of them is present in any possible world;
blocks are independent;
each tuple of a block has its own probability, with the per-block sum $\le 1$ ; the residual $1 - \sum_i p_i$ is the probability that no tuple from the block is present (the “null outcome”).

A TID is the special case where each block has exactly one tuple. BIDs are the natural circuit-level model for tables with key uncertainty: “exactly one of these rows is the real row, we don’t know which, and here are the weights”.

The `gate_mulinput` Gate

ProvSQL represents each BID block in the persistent circuit by a group of gate_mulinput gates that share a common child, an input gate acting as the block key. Each mulinput gate corresponds to one alternative of the block and carries its own probability (set with set_prob). mulinput gates are not first-class leaves of the provenance DAG: semiring evaluators do not know how to interpret them and will refuse any circuit that contains one, and the probability pipeline handles them only after rewriting the blocks into standard Boolean gates – as described below.

The canonical way to create such gates from SQL is repair_key, which takes a table with duplicate key values, allocates one fresh input gate per key group, and turns each member of the group into a mulinput whose child is that block key. When no probabilities are attached, repair_key defaults them to a uniform distribution over the block members.

Rewriting Blocks into Independent Booleans

Most probability-evaluation algorithms require a purely Boolean circuit: AND, OR, NOT, and independent Bernoulli leaves. A BID block is not directly such a structure – its elements are mutually exclusive, not independent. BooleanCircuit::rewriteMultivaluedGates (in BooleanCircuit.cpp) reduces every block to an equivalent Boolean subcircuit by introducing $O(\log n)$ fresh independent Bernoulli variables per block of size $n$ whose joint distribution reproduces the original discrete weights.

The construction is divide-and-conquer. Given a block with alternatives carrying cumulative probabilities $P_0 \le P_1 \le \cdots \le P_{n-1}$ , the recursive helper BooleanCircuit::rewriteMultivaluedGatesRec splits the range $[\mathit{start}, \mathit{end}]$ at the midpoint $\mathit{mid}$ , creates one fresh input gate g with probability

$\frac{P_{\mathit{mid}+1} - P_{\mathit{start}}} {P_{\mathit{end}} - P_{\mathit{start}}}$

– the conditional probability of landing in the left half – and recurses twice: the left half gets g pushed onto its prefix, the right half gets NOT g. At a leaf ( $\mathit{start} = \mathit{end}$ ), the mulinput gate is rewritten into the AND of the accumulated prefix, so its truth value becomes the conjunction of the fresh-variable decisions that lead to it. If the block’s probabilities do not sum to 1, the outer call wraps the whole construction in one more fresh input of probability $P_{n-1}$ to carry the “none of them” residual.

After rewriting, the block’s mulinput gates have been turned into ordinary AND gates over fresh independent Boolean inputs, and the circuit is ready for any TID-based probability method. The dispatcher in probability_evaluate_internal calls BooleanCircuit::rewriteMultivaluedGates lazily: the "independent" method handles mulinput gates natively and runs on the raw circuit; every other method falls through to the rewrite first. This is the pivot point referenced in Step-by-Step: Adding a New Probability Evaluation Method below.

Shapley and Banzhaf Values

ProvSQL also exposes expected Shapley values and expected Banzhaf values, which quantify the individual contribution of each input tuple to the truth of a provenance circuit. The user-facing interface is described in Shapley and Banzhaf Values; this section covers the implementation in shapley.cpp and dDNNF.cpp.

Expected Shapley values are #P-hard in general but become polynomial-time computable when the provenance is represented as a decomposable and deterministic (d-D) Boolean circuit – essentially a d-DNNF. The algorithm ProvSQL uses is Algorithm 1 of Karmakar, Monet, Senellart, and Bressan (PODS 2024, [Karmakar et al., 2024]), specialised to the two coefficient functions that define the Shapley and Banzhaf scores. Both scores are computed in expectation: the random subset of variables is drawn according to the per-variable probabilities of the circuit, and when no probabilities have been set, each defaults to 1 and the computation collapses to the standard deterministic Shapley / Banzhaf value.

Entry Point

shapley / banzhaf (and their set-returning variants shapley_all_vars / banzhaf_all_vars) are thin wrappers that unpack their arguments and call shapley_internal in shapley.cpp. That helper performs the following sequence:

Build a BooleanCircuit from the persistent store via getBooleanCircuit.
Build a dDNNF by calling BooleanCircuit::makeDD. This is the same d-DNNF construction used for ordinary probability evaluation, and obeys the same method / args conventions.
dDNNF::makeSmooth – ensure that every OR gate’s children mention the same variable set. The paper’s algorithm assumes a smooth d-DNNF.
For Shapley (but not Banzhaf): dDNNF::makeGatesBinary on AND – binarise AND gates so each has at most two children. Together, the previous two steps turn the d-DNNF into a tight d-D circuit in the paper’s sense.
Call dDNNF::shapley or dDNNF::banzhaf on the target variable’s gate.

The Shapley Recurrence

The paper’s algorithm conditions the circuit on the target variable being fixed to true (call the result $C_1$ ) and to false (call it $C_0$ ), computes a pair of per-gate arrays on each conditioned circuit, and combines them into the final score. ProvSQL’s dDNNF::shapley mirrors that structure:

double dDNNF::shapley(gate_t var) const {
  auto cond_pos = condition(var, true);   // C_1
  auto cond_neg = condition(var, false);  // C_0

  auto alpha_pos = cond_pos.shapley_alpha();
  auto alpha_neg = cond_neg.shapley_alpha();

  double result = 0.;
  for (size_t k = ...; k < alpha_pos.size(); ++k)
    for (size_t l = 0; l <= k; ++l) {
      double pos = alpha_pos[k][l];
      double neg = alpha_neg[k][l];
      result += (pos - neg) / comb(k, l) / (k + 1);
    }
  result *= getProb(var);
  return result;
}

dDNNF::condition returns a copy of the circuit in which the target input gate has been replaced by an AND / OR-with-no-children acting as the constant true / false respectively. The private helper dDNNF::shapley_alpha then performs a single bottom-up pass computing a two-dimensional array $\beta^g_{k,\ell}$ (called result[g] in the code) at every gate $g$ , where $k$ is the number of variables under $g$ in the current cofactor and $\ell$ is the number of them that are positively assigned. The recurrences follow the IN / NOT / OR / AND cases of Algorithm 1 of the paper:

At a leaf, the array encodes the Bernoulli distribution of that single variable.
At an OR gate, the arrays of the children are summed coordinatewise (valid because the d-DNNF is smooth, so all children have the same variable set).
At a binary AND gate, the arrays are convolved via a double sum over $(k_1, \ell_1)$ pairs – the decomposability of AND makes this the Cauchy product of two independent distributions. This convolution is the reason AND gates have to be binarised before the algorithm runs.
A standalone bottom-up pass (dDNNF::shapley_delta) precomputes the $\delta^g_k$ polynomials, which the algorithm uses at NOT gates to turn negation into a coefficient flip.

The final score is $p_x \cdot \sum_{k, \ell} c_{\text{Shapley}}(k+1, \ell) \cdot (\beta^{g_{\text{out}}}_{k,\ell} - \gamma^{g_{\text{out}}}_{k,\ell})$ , where $\beta^{g_{\text{out}}}$ comes from $C_1$ and $\gamma^{g_{\text{out}}}$ from $C_0$ , and $c_{\text{Shapley}}(k+1, \ell) = \binom{k}{\ell}^{-1} / (k+1)$ is the Shapley coefficient – i.e.exactly the formula implemented above. The overall complexity is $O(|C| \cdot |V|^5)$ arithmetic operations, dominated by the double-sum convolution at AND gates over the $|V|^2$ -sized arrays.

The if (isProbabilistic()) guards inside dDNNF::shapley_alpha and dDNNF::shapley_delta short-circuit the polynomials to a single top-level coefficient when all input probabilities are 1, so that the same code path computes classical (deterministic) Shapley values without paying the expected-score overhead.

Banzhaf

The expected Banzhaf value admits a much simpler formula [Karmakar et al., 2024]:

$\operatorname{EScore}_{\text{Banzhaf}}(\varphi, x) = p_x \cdot \bigl( \mathrm{ENV}(C_1) - \mathrm{ENV}(C_0) \bigr)$

where $\mathrm{ENV}(\varphi) = \sum_{Z \subseteq V} \Pi_V(Z) \sum_{E \subseteq Z} \varphi(E)$ can be computed in a single linear pass over a smooth d-D circuit without binarising AND gates. dDNNF::banzhaf runs dDNNF::banzhaf_internal on the two conditioned circuits $C_1$ and $C_0$ and returns the difference times $p_x$ ; the overall complexity is $O(|C| \cdot |V|)$ , one factor of $|V|$ less than Shapley. This is why shapley_internal skips the dDNNF::makeGatesBinary call in the Banzhaf branch.

Hybrid Evaluation for Continuous Distributions

When the circuit being evaluated contains continuous gates (gate_rv, gate_arith, gate_mixture), a hybrid evaluator runs before the Boolean dispatch above. Its job is to fold every sub-circuit that has a closed-form analytical answer into a Bernoulli leaf so the resulting circuit is a normal Boolean circuit ready for any of the Boolean methods.

The hybrid evaluator has three passes:

Peephole pruning (runRangeCheck): support intervals propagate through gate_arith, every gate_cmp is tested against the propagated interval, and every comparator decidable from the support alone collapses to a Bernoulli gate_input with probability 0 or 1.
Family-closure simplifier (runHybridSimplifier): linear combinations of independent normals fold into a single normal; sums of i.i.d. exponentials with the same rate fold into an Erlang; identity / single-child arith gates and semiring identities collapse.
Island decomposition (runHybridDecomposer): the remaining cmps are partitioned by base-RV footprints into islands; single-cmp islands marginalise via runAnalyticEvaluator’s closed-form CDF; multi-cmp islands with shared base RVs go through the joint table.

See Continuous Distributions for the full simplifier rule set and the island-decomposition algorithm.

Conditional Evaluation

expected / variance / moment / central_moment / support / rv_sample / rv_histogram all accept an optional prov uuid argument that conditions the moment, sample, or histogram on the provenance event prov. When prov resolves to anything other than gate_one, evaluation routes through the joint-circuit loader getJointCircuit (MMappedCircuit.cpp), which performs a multi-rooted BFS over the union of the reachable gates from both input and prov so shared gate_rv leaves between the two are loaded into a single GenericCircuit and consequently couple correctly in the Monte Carlo sampler’s rv_cache_. The closed-form truncated-distribution table is exhaustive for Normal (Mills ratio), Uniform (intersected support), and Exponential (memorylessness); other shapes fall back to MC rejection sampling at provsql.rv_mc_samples budget. See Continuous Distributions for depth.

The Inversion-Free `UCQ(OBDD)` Path

The 'inversion-free' method (and the default-chain rung that follows independent) evaluates the inversion-free class of Jha and Suciu [Jha and Suciu, 2011]: hierarchical, tuple-independent queries – including self-joins – whose lineage admits a polynomial-size OBDD. On these the generic 'tree-decomposition' / compilation fallbacks can blow up (the lineage is not low-treewidth), yet a structured d-DNNF built over a query-derived variable order stays linear in the lineage.

This path is a sibling of the Safe-Query Rewriter, and the two are complementary:

The safe-query rewriter (provenance class 'boolean') restructures the query so the planner emits a read-once circuit, which independent then evaluates almost for free. It applies only to the read-once (safe) class and changes the produced circuit.
The inversion-free path leaves the lineage intact and evaluates the naive circuit – which, even for a safe query, is generally not read-once (e.g. q(x) :- B(x), A(x,y) yields ⋁_y (B(x) ∧ A(x,y)), repeating B(x)), so independent rejects it. It also covers the strictly larger inversion-free-but-not-read-once self-join class. It is decoupled from boolean_provenance and gated on its own GUC, provsql.inversion_free (on by default).

The pipeline has four stages.

Detection (src/safe_query.c)

detect_inversion_free checks the four preconditions (hierarchical, strictly tuple-independent atoms, positional consistency, acyclic precedence) and, on success, builds a SafeCert recipe describing the query-derived (Prop. 4.5) variable order. It reuses the candidate gate and union-find machinery of the safe-query rewriter but is not gated on boolean_provenance: process_query runs it on the lineage query whenever provsql.inversion_free is on, after (and only when) the read-once rewrite did not already fire.

A non-tracked base relation (no provsql column and no metadata entry) is deterministic: it contributes only probability-1 tuples and anchors no provenance variable, so the detector erases it from the root, positional, precedence and marker passes while keeping its join equalities (it still filters the cross product). This mirrors the read-once path’s dissociation transparency, with the same soundness guards (a plain table, not a matview / foreign table / partitioned parent / inheritance child), and only enlarges the certified class.

Flattening pre-pass (src/provsql.c)

build_inversion_free_ctx runs the detector on a flattened copy of the lineage query so that SPJ subqueries and views are recognised. flatten_spj_subqueries inlines every non-lateral SPJ subquery slot (no aggregation, grouping, DISTINCT, set operation, sublink, CTE or LIMIT; flat RangeTblRef FROM over base relations; target list all plain base Vars) into its base atoms – substituting the parent’s column references, pulling the subquery WHERE up and rebuilding a flat FROM – and recurses, so a view-over-view or nested derived table collapses to base atoms first. A view referenced k times inlines to k copies of its base atoms: a structured self-join the inversion-free path handles natively. On PostgreSQL 18 the synthetic RTE_GROUP of a GROUP BY query is stripped from the copy first. The original query is left intact; only transparent markers and a root certificate are added.

Certificate and per-input markers (src/safe_query_cert.{h,c})

The recipe and the order are carried into the circuit on transparent gate_annotation gates (see Architecture Overview):

the serialised SafeCert is stamped on the per-row root as a C-prefixed extra payload;
each certified atom’s input is wrapped (via annotate) in an annotation carrying a K-prefixed order key (root, sec, factor) (SafeCertKey), emitted by the planner (build_inversion_free_marker in src/provsql.c) via the inversion_free_key SQL function. An atom binding only the head class is root-only (no secondary column); a relation whose occurrences span two or more secondary classes is the shared self-join guard (factor = SAFE_CERT_GUARD_FACTOR).

The root and sec class values are carried as length-prefixed value text (the column type’s I/O output), so the key works for any scalar key column – text (including spaces / colons), uuid, date, numeric … – not just integers. The builder uses them only for grouping (equal text ⇒ same block / tile) and a consistent total order, both of which any injective type rendering satisfies.

For a view inlined by the flattening pre-pass the markers wrap the base inputs inside the subquery, threaded down through the recursive rewrite by a per-query InvFreeMarkerCtx context tree (the certificate stays on the parent’s per-row root).

Both markers are inert at evaluation: the annotation gate is identity for every evaluator, so a query carrying them evaluates identically whether or not the analysis ran.

Structured d-DNNF builder (src/StructuredDNNF.{h,cpp})

StructuredDNNFBuilder compiles the monotone lineage top-down into a ProvSQL dDNNF: it expands the circuit to a canonical DNF and recurses with decomposable AND at independence points (variable-disjoint factors) and deterministic OR at Shannon decisions on the supplied variable order, threading a false-sink through OR-chains and sharing equal sub-d-DNNFs through a component cache. The order affects only the d-DNNF size, never correctness, so the builder is sound on any monotone lineage; the Prop. 4.5 order is what keeps it polynomial on the certified class. Multivalued (BID) and NOT gates are out of scope and rejected with a CircuitException.

Dispatch (src/probability_evaluate.cpp)

collect_inversion_free_keys walks the circuit for the K-marker annotations and maps each wrapped input to its InputKey; inversion_free_rank flattens those keys into a total rank (root value, then secondary value, then guard-before-payload, then factor) for the order-only builder. The explicit 'inversion-free' method requires the certificate and errors without it; the default chain takes this rung only when a certificate is present and provsql.inversion_free is on, after independent and before tree-decomposition, catching CircuitException to fall through.

Shapes the analysis does not model cause detection to decline (no certificate): a BID/gate_mulinput atom, a subquery the flattening pre-pass cannot inline (an aggregating view, a set-operation / UNION view, a correlated or LATERAL subquery), or a flattened conjunction that is genuinely non-hierarchical (the H-query R(x),S(x,y),T(y)). A malformed C-prefixed payload fails to parse and is treated as an inert annotation. In every case evaluation falls back to the normal chain and stays correct. These declines – and the positive cases (self-joins, non-integer key columns, deterministic-relation filters, single- and multi-relation SPJ views, views-over-views) – are covered by test/sql/safe_query_inversion_free.sql.

Step-by-Step: Adding a New Probability Evaluation Method

The work is almost entirely in two files. Pick a short, descriptive method string – it is the value the user passes to probability_evaluate.

Declare the method on BooleanCircuit.h:

double myMethod(gate_t g, const std::string &args) const;

Implement it in BooleanCircuit.cpp. The method receives the root gate and the user-supplied args string (may be empty) and must return a probability in $[0, 1]$ . Check provsql_interrupted periodically if the computation is long so that the user can cancel with Ctrl-C:
```
double BooleanCircuit::myMethod(gate_t g, const std::string &args) const {
  // Parse args if needed.
  // Run the algorithm, respecting provsql_interrupted.
  // Return the probability.
}
```
Register the method in the catalog: subclass ProbabilityMethod (interface in ProbabilityMethod.h) in probability_evaluate.cpp next to MonteCarloMethod and friends, overriding name(), evaluate(), guaranteeKind() and the cost model, and add a registerMethod(std::make_unique<MyMethod>()) line to the one-time registration block. Three optional overrides matter:
- handlesMultivalued(): return true only if the algorithm reads gate_mulinput blocks natively (like independent); otherwise the dispatcher rewrites multivalued gates to Boolean before calling you (see Block-Independent Databases and Multivalued Inputs).
- applicable(): structural preconditions (e.g. mobius requires a gate_mobius root); keeps the method out of the chooser where it cannot run.
- producesDD() / buildDD(): implement these if the method constructs a d-DNNF, so the makeDD auto route (Shapley / Banzhaf) can select it too.
(Optional) Join the default chain by overriding inDefaultChain() and estimatedCost(): the chooser is a uniform-cost search over the registered methods’ estimates, so a well-calibrated cost model is what ranks the method – there is no hand-kept fallback order to edit.
Add a regression test under test/sql/ and register it in test/schedule.common. Follow the skip-if-missing pattern from the other external-tool tests (see Testing) if the new method depends on an external binary.
Update the user documentation in Probabilities and add a row for the new method to the “Currently supported methods” table above.