The mental model
Concepts
A short path from dynamic graph updates to the invariant Axiom protects: every edge remains covered by a matching edge.
What is a maximal matching?
A matching is a set of edges that share no vertices. It is maximal when no remaining graph edge can be added without breaking that rule. Maximal does not mean maximum: Axiom preserves a valid locally complete matching, not necessarily the largest possible one.
Why dynamic maintenance?
Recomputing a matching after every graph change wastes work. Axiom accepts an edge insertion or deletion, repairs the affected neighborhood, and then checks that the matching and its partner map still agree with the graph.
After an accepted update, the useful question is not “what was the matching from scratch?” but “what changed, and which invariant forced the repair?”
The update loop
- Validate the vertex and edge operation.
- Apply the graph change atomically.
- Repair local matching state and indexes.
- Rebuild a phase or level when its schedule requires it.
- Expose the new state only after validation succeeds.
z-systems in plain language
The implementation partitions the graph into structured regions so update work can stay local. The (A, B, U) partition, saturation set, and adjacency indexes provide the bookkeeping that lets the algorithm find affected vertices without scanning every edge.
These structures are implementation details until you need to reason about performance or contribute to the engine. Start with the public API; use the architecture guide when you need the invariants.
Maximality is a contract
Use matcher.maximal() as a diagnostic assertion in experiments. The returned matching is a snapshot for inspection; updates must go through the matcher so internal partner maps and indexes remain synchronized.