Factorized counting
mnestic
Specific to mnestic 0.10.5. Opt-in and default off this release (a Db-wide
kill switch, set_query_factorization) so it can soak before any default-on
consideration. The always-on ::explain advisory ships regardless. When it
does fire, result sets are unchanged.
The problem
A count() over a join pays for every homomorphic match of its body, even
though the caller only wants one number. The engine evaluates an aggregate rule
by driving the compiled join pipeline and streaming each projected match into a
per-group += 1 accumulator: memory stays flat at O(#groups), but CPU is
O(#matches).
?[count(person)] :=
*member[group, person],
*knows[friend, person],
*lives_in[person, city]There is no cost-based optimizer and no automatic factorization of general shapes — the human is expected to be the optimizer. On a standard social-network join workload, an external benchmark measured naive count-over-join CozoScript running 4–342× slower than a columnar engine whose optimizer factorizes count aggregation automatically. At tens of millions of matches that gap is seconds; at billions of matches the naive form is not runnable at all, even though the answer is a single integer.
What changed
mnestic adds a normal-form pre-pass (query/factorize.rs) that rewrites an
eligible single-clause count()-over-positive-join into Yannakakis-style
per-key counting sub-rules — the classical counting DP on an acyclic join.
Instead of enumerating matches, it propagates per-key counts bottom-up along the
join tree and sums products across a central edge, so a body with 1.65 × 10⁹
matches is counted without ever materializing them.
The rewrite is exact by construction, not an approximation:
- Bit-identical answer. The result is the same number, same
Inttype, as naive evaluation — verified by a 400-case differential harness (naive vs factorized, mem + sqlite, exact row-and-type equality). - No Float cliff. The rewrite accumulates in an internal
int_sum_prodaggregate that stays in exacti64and errors, never silently wraps, on overflow. (The hand-authored patterns route their partials throughsum, which isf64and exact only below2⁵³— the automatic path has no such caveat.)
When it fires
The pass is conservative: it fires only on shapes it can prove exact and
declines everything else to unchanged naive evaluation. Eligible means a single
non-recursive clause whose head is exactly one count() (with optional group
keys) over an all-positive, alpha-acyclic body.
It declines — falling back to exact naive evaluation — on:
- cyclic and non-free-connex bodies (no separator splits them),
- repeated-variable bodies,
- negated atoms and recursive rules,
- bitemporal reads,
count_uniqueand mixed-aggregate heads,- and any body containing a
!=predicate.
That last exclusion is deliberate. An engine-side != inclusion–exclusion
auto-rewrite was drafted and then cut before release because it miscounted
on mixed Int/Float data. So a query like the one below is not rewritten
automatically:
?[count(p2)] :=
*knows[p1, p2],
*knows[p2, p3],
*member[group, p3],
p1 != p3The !=, anti-join, and count_unique cases still have exact hand-authored
rewrites — they live in the
cardinality-algebra spec,
which is the reference for every shape the automatic pass declines. The manual
patterns and the automatic pass agree on every result; the pass simply removes
the boilerplate for the subset it can prove safe.
Enabling it
The rewrite is gated behind a Db-wide kill switch, off by default:
use cozo::DbInstance;
let db = DbInstance::new("mem", "", "")?;
db.set_query_factorization(true); // opt in; default is false in 0.10.5
// Eligible count()-over-join now rewrites transparently — same answer, no
// join materialization.
let out = db.run_default(
"?[count(person)] := *member[group, person], *knows[friend, person], *lives_in[person, city]",
)?;Because it is a whole-Db switch, you turn it on for a workload you have measured and leave it off elsewhere. When off, every query evaluates exactly as it did before.
mnestic
Specific to mnestic 0.10.7. The kill switch is now exposed on the Python
binding — db.set_query_factorization(True) flips it and
db.query_factorization() reads it back. Earlier releases could toggle it only
from Rust. The default is still off.
The always-on ::explain advisory
Independent of the switch, a companion detector always runs and annotates plans it recognizes as factorizable. So you can see whether a query would benefit before you flip the switch on:
::explain { ?[count(person)] := *member[group, person], *knows[friend, person], *lives_in[person, city] }An eligible count-over-join carries a factorization advisory in the ::explain
output (also emitted via log::info!). A body the pass would decline — a !=,
a cycle, a count_unique — carries no advisory, which is itself the signal that
you are on the naive path and should consult the hand-authored patterns.
See also
- Join reorder — the companion 0.10.5 pre-pass that
fixes a naively-ordered join's atom order (this pass fixes how its
countis aggregated). - Equality pushdown — the other rewrite in
query/reorder.rs; a pure optimization with unchanged results. - Aggregations —
count/count_unique/sumsemantics (inherited engine behavior). - What mnestic adds