unjam

RTGS gridlock resolution: given a queue of interbank payments and the balances behind them, compute the greatest set that can settle simultaneously without overdrawing anybody.

Three things are established here, in rising order of how hard they were to get:

1. The solver returns the greatest feasible settlement plan, not merely a maximal one, so the answer is a function of the input rather than of the order the sweep happened to run in.
2. That fixed point does not depend on the removal order. Sixteen removal policies are run over every generated instance and must land on the identical plan, and the removal order is exposed so that invariance can be observed rather than assumed.
3. A lower bound on a net position preserves the guarantee; an upper bound destroys it. Overdraft protection and intraday credit are lower bounds, so they cost nothing. Bilateral limits bound a difference that moves the right way in both coordinates, so they survive too. Exposure caps are an upper bound, and an instance carrying one can have several incomparable maximal plans and no greatest one. The solver refuses those rather than returning one of them and letting the caller assume it is the maximum.

The third is the one worth stealing. It draws a line through the space of constraints an operator might want, says which side of it a design falls on, and is why this crate says no to a question it cannot answer honestly.

Zero dependencies. The solver and its data model are 832 lines of Rust and the independent oracle that checks them is another 196; parsing and the CLI account for the rest. There are 1416 lines of test code, and their entire job is to establish that the word "greatest" is not a lie.

(Counting rule, so those numbers are reproducible rather than decorative: non-blank, non-comment lines, excluding inline #[cfg(test)] modules. The solver figure is engine.rs + model.rs + money.rs; the test figure is every inline test module plus everything in tests/.)

The problem

In a real-time gross settlement system every payment settles individually and immediately, so a bank can only pay out what it already holds. That produces a failure mode netting systems do not have: a queue in which ALPHA cannot pay BETA until BETA pays ALPHA, and neither can move first. The payments are collectively affordable and individually impossible. Central banks call this gridlock, and the standard answer is a periodic sweep that looks for a set of queued payments which can settle together, funding each other.

                    owes 100.00
        ALPHA  ========================>  BETA
          ^                                 |
          |          owes 100.00            |
          +=================================+

        ALPHA holds 0.00            BETA holds 0.00

One at a time, neither payment can move: ALPHA must fund its own payment before BETA's arrives, and BETA is in the same position. The queue is stuck forever, and no amount of waiting helps, because nothing is going to arrive from outside.

Both at once, each payment funds the other. Both settle, both banks end at 0.00, and no money was invented along the way. That is the whole trick, and finding which payments can do it is the whole problem.

$ unjam instances/morning-window.unjam

instance: 6 accounts, 12 payments, scale 2
settled:  5 of 12 payments, 650.00 of 2505.00
work:     7 removals over 4 worklist steps

payments
  #0   ALPHA   -> BETA            200.00  settled
  #1   ALPHA   -> GAMMA           400.00  queued
  ...

bilateral limits
  EPSILON -> ZETA                   0.00 of 400.00

closing positions
  ALPHA           110.00  (opened 250.00)
  ...

7 payment(s) worth 1855.00 remain queued. The first of each queue is held
by the constraint named beside it; the rest are behind it in FIFO order.
  #1   ALPHA   would overdraw ALPHA to -290.00
  #4   GAMMA   would overdraw GAMMA to -75.00
  #8   EPSILON would take EPSILON -> ZETA to 450.00, over the cap of 400.00
  #10  ZETA    would overdraw ZETA to -290.00

Every payment left queued names the constraint that held it, which is the operational form of the guarantee: there is no payment sitting in that list because the sweep happened to reach it first.

The claim

A queue is FIFO, so the only thing to decide per account is how far down its queue to go. A settlement plan is therefore a vector k, where k[i] is how many payments are taken from the front of account i's queue. In the two-bank example above the answer is k = (1, 1): one payment from each.

resolve does not return a maximal plan. It returns the greatest one: the plan that goes at least as far down every queue as any other feasible plan does.

The difference is not pedantry. Maximal means "nothing can be added to it". Greatest means "it beats every alternative". Those come apart the moment two plans block each other:

ALPHA holds 10 and has queued two payments of 10, one to BETA and one to GAMMA.

Ignore the queue for a second and treat these as a set. ALPHA can fund either payment but not both, so {to BETA} and {to GAMMA} are each maximal, neither contains the other, and "the maximal settleable set" does not name anything. FIFO is what collapses that: only {to BETA} is reachable as a prefix, and it is the unique greatest plan. Run it:

$ unjam instances/no-unique-maximum.unjam --subsets   # 2 maximal sets
$ unjam instances/no-unique-maximum.unjam --maximal   # 1 greatest plan

Why an operator should want the greatest one

Any maximal plan clears a legal batch, so a solver returning one is not dangerous. What it costs is determinism, and determinism is load-bearing in three places.

Replay and reconciliation. A settlement system runs a primary and a disaster recovery site over the same queue, and they must agree on which payments cleared in a window, byte for byte. A version upgrade must not silently change that answer either. "Any maximal plan" makes both of those impossible to check, because two correct implementations may legitimately disagree.

Answerability. The bank whose payment did not settle asks why. With a merely maximal plan the honest answer is "the sweep happened to remove yours first", which is not an answer anyone can act on. With the greatest plan, every payment left queued is left queued because settling it would have overdrawn someone or breached a limit, and the CLI names which.

Testability. A solver whose output is not a function of its input cannot be differentially tested against anything, including a later version of itself. Half the verification in this repository would be impossible to state.

And it settles at least as much value. Going further down a queue only ever adds payments to what settles, so a plan that dominates another in payment counts also dominates it in value. The guarantee is stated in counts because that is the ordering the lattice argument needs; the thing an operator actually cares about follows from it rather than being assumed.

Is "greatest" an achievement, or an artifact of the model?

A fair question, and the answer is that it is two claims which are easy to run together.

That a greatest plan exists is a theorem about the problem, and it is not free. It holds because of a specific asymmetry, it needs the queue discipline, and it is false for a constraint an operator might plausibly ask for: add an upper bound on a net position and instances appear with several incomparable maximal plans and no greatest one. So the existence is a real result with a real boundary, and both sides of that boundary ship as runnable instances.

That this solver finds it is a separate claim about the algorithm, and it is also not free. Nothing about FIFO forces a correct-looking solver to return the greatest plan: one that removes a payment more than the violation required returns a feasible, maximal, wrong answer, and one that clears a queue instead of clearing a violation returns a feasible answer that settles almost nothing. Both are plausible implementations, both pass a smoke test, and both are in mutate.py as E4 and E10 precisely because they are the mistakes worth being afraid of.

The suite exists because the second claim can fail quietly while everything still looks right.

That is a strong claim, it is the only interesting thing this repository has to say, and a plausible-looking implementation can get it wrong in ways no smoke test would notice. So the claim is not asserted. It is attacked.

How the claim is checked

Run cargo test. 61 tests, about a second.

An independent oracle. src/oracle.rs walks every settlement plan an instance admits and keeps the feasible ones. It shares no part of the search with the solver: no worklist, no incremental bookkeeping, no removal rule. 3000 generated instances go through both and the answers must match exactly. Enumeration is exhaustive within a budget (default 4,000,000 plans), and the generated instances average about 30 plans each, so "exhaustive" here means genuinely exhaustive rather than sampled.

The two do share one thing, and it is worth naming: both ask engine::is_feasible whether a plan is legal. That is the definition of the problem rather than a way of solving it, and keeping one definition is what makes the comparison meaningful at all. But it does mean a bug in the predicate itself would fool solver and oracle together. Two things push back on that. The predicate is declarative, recomputing positions from scratch, and running_positions_match_a_fresh_recomputation checks the solver's incremental arithmetic against it on every generated instance. And mutate.py mutates the oracle as well as the solver, so a suite that could not tell a broken oracle from a working one would be caught saying so.

The lattice property, per instance. The proof below rests on one fact: the componentwise maximum of any two feasible plans is feasible. That exact statement is checked, over every pair of feasible plans of every generated instance, by any_two_feasible_plans_have_a_feasible_join. It is worth being pedantic about, because the easier thing to check is that the maximum over the whole feasible set is feasible, and that is a strictly weaker claim than the one the proof uses.

Order invariance. The solver's fixed point should not depend on which violation it clears first, or how far it lowers a coordinate at a time. Sixteen different removal policies are run over every instance and must all land on the identical plan. This is the property most likely to be quietly false in an implementation that looks correct.

Add-back maximality. For every queue that still has payments waiting, settling one more must break feasibility. Stated over the next queued payment specifically, because FIFO means that is the only payment which could be added at all.

Two negative results. The suite also pins down where the guarantee stops being true: fifo_is_what_makes_the_maximum_unique and exposure_caps_break_the_lattice. Both are described below.

Mutation testing. A green suite proves things about the code and nothing about the suite, so twenty-one deliberate bugs were injected to see whether the tests would notice. Five of them go into the oracle, not the solver, because a differential test is theatre if a broken oracle would agree with a broken solver just as happily as a working one would.

All twenty-one are caught. Two were not, at first, and both were worth the run. One neutered the worklist shuffle so that every removal policy secretly became the same policy, leaving the order-invariance property above passing while demonstrating nothing; that is why Settlement exposes removal_order and why different_seeds_really_do_reorder_the_work exists. The other removed a constraint check from the oracle that had been added to fix a bug and never given a test, which made the fix a claim rather than a change.

Run it yourself with python mutate.py. The write-up is in docs/mutation-testing.md, including the mutant caught only by hanging, the four places where coverage rests on a single assertion, and why a mutant that fails to compile is counted as proving nothing rather than as a kill.

The algorithm

This is Bech and Soramäki's gridlock resolution algorithm, from a 2001 Bank of Finland discussion paper.

To calibrate how real this is, since the hedging below could otherwise read as "probably academic": queue management with periodic offsetting is a standard documented design feature of large-value payment systems, not a proposal. It has its own established vocabulary (gridlock resolution, liquidity-saving mechanisms, queue optimisation), central banks publish on it, and the Bank of Finland maintains a simulator built for studying exactly these algorithms. A payments-infrastructure engineer will recognise the problem immediately.

What this README does not claim is that any named operator runs this exact variant today. I have not verified that, the details are not generally public, and several systems the 2001 literature discusses have since been replaced, TARGET2 by T2 in 2023 among them. So: real problem class, honestly attributed algorithm, unverified deployment.

A settlement plan is a prefix vector k, where k[i] is how many payments are taken from the front of account i's queue. Queues are FIFO, so a plan cannot skip a payment and settle the one behind it. Start from the plan that settles everything, then repeatedly find a violated constraint and lower a coordinate that is responsible for it. Stop when nothing is in violation.

k <- (|Q_1|, ..., |Q_n|)
while some constraint is violated:
    if net_i(k) < 0 for some account i:              lower k_i
    if value_L(k) > cap_L for some limit L = p -> q: lower k_p
return k

The second rule has a wrinkle worth stating here rather than leaving in the source: lowering k_p drops whatever payment is at the end of p's settled prefix, and that payment need not be one of the payments the limit constrains. That is correct and it is deliberate. The lemma in src/engine.rs justifies lowering the sender's coordinate, not removing a particular payment, and FIFO means the only coordinate move available is to drop the last one. It also means a single limit violation can cost work on payments unrelated to that pair, which is where the O(payments * L) bound below comes from.

Both descent rules matter, and stating only the first would be wrong rather than merely incomplete. Take an account holding 1000 with two queued payments of 60 to the same counterparty and a limit of 100 on that pair. At the top plan nobody is overdrawn, so an overdraft-only loop halts at once and returns a plan breaching the limit by 20. The unit test a_bilateral_limit_trims_the_plan is exactly that instance. instances/limits.unjam is its more interesting sibling: the same two payments and the same cap, plus a 50.00 return leg that nets the exposure down to 70 so all three settle after all.

Implementation is a worklist: payments live in a flat arena, each queue is a list of indices into it, net positions are a Vec<Amount> updated incrementally as payments are pulled out, and accounts that go negative are pushed onto a VecDeque. A plan only ever moves downwards, so a payment is removed at most once and the removal count is bounded by the number of queued payments; the_removal_log_reconciles_with_the_plan asserts that the log of dropped payments and the returned plan describe exactly the same thing. That makes the sweep linear in the size of the queue when there are no bilateral limits. With L limits a single removal can put up to L of them back on the worklist, so the bound is O(payments * L) rather than linear, and building the payment-to-limit index costs the same again up front.

All money is i128 minor units with no floating point anywhere, including in parsing and formatting. overflow-checks is left on in release builds, and the instance builder rejects inputs whose total value could overflow an intermediate sum, which is what lets the hot loop use plain arithmetic.

Why a greatest plan exists

Write out_i(k_i) for what account i pays out and in_i(k) for what it receives. The asymmetry that makes this work: out_i depends only on i's own coordinate, while in_i is nondecreasing in every coordinate.

Take feasible plans k and k' and their componentwise maximum m. Fix an account i, and assume without loss of generality that m_i = k_i. Then out_i(m_i) = out_i(k_i), while m >= k gives in_i(m) >= in_i(k). So

net_i(m) = b_i + in_i(m) - out_i(m_i)  >=  b_i + in_i(k) - out_i(k_i) = net_i(k)  >=  0

The feasible set is closed under componentwise maximum. It is finite and contains the all-zero plan, since balances are non-negative. A finite non-empty join-closed set has a unique greatest element.

Why the loop finds it. If net_i(k) < 0, then every feasible k' <= k has k'_i < k_i: if k'_i equalled k_i we would have out_i(k'_i) = out_i(k_i) and in_i(k') <= in_i(k), so net_i(k') <= net_i(k) < 0. Lowering a violated coordinate therefore never steps below the greatest plan. The plan strictly decreases each step and is bounded below, so the loop terminates; it terminates feasible and still at or above the greatest plan, hence exactly at it.

Nothing in that argument fixes which violated account to pick or how far to lower it. That is where the order-invariance property comes from, and it is why Policy exists as a public type: so the invariance can be tested instead of believed.

Why FIFO is load-bearing

The counterexample is in "The claim" above: without the queue discipline, ALPHA's two payments give two incomparable maximal sets and no greatest one. Two consequences follow that are easy to miss.

FIFO has a price, and it is real. In instances/fifo-blocks.unjam ALPHA holds 10.00 and has queued 100.00 followed by 5.00. It could easily afford the 5.00 and cannot settle it, because an unaffordable payment sits in front of it. Nothing settles at all. A system that allowed reordering would clear that queue; this one will not, and the guarantee is bought with exactly that.

It is also why the oracle enumerates plans rather than subsets. Walking the 2^n subsets of payments would answer a different question, one whose answer is not unique, and a differential test built on it would fail correctly against a solver that is right. oracle::maximal_subsets still exists, but only to demonstrate the negative result: it is what --subsets runs, and it judges feasibility by every constraint, not just balances, so that any difference it reports is attributable to the queue discipline and to nothing else.

Which constraints keep the guarantee, and which kill it

Bilateral limits keep it. A cap on out(i->j) - out(j->i) rises in i's coordinate and falls in j's. Under a componentwise maximum, whichever plan supplied i's coordinate already capped the rising term, and the falling term only grows. So the join property survives, the solver handles limits natively, and bilateral_limits_keep_the_lattice checks it on every generated instance that carries one.

I expected this constraint to break the lattice and it does not. The proof above is the corrected version.

Credit lines keep it, for free. A credit line moves the threshold an account is measured against from 0 to -credit. Neither the join-closure argument nor the descent lemma uses anything about that threshold except that it is fixed per account, so both go through verbatim; the all-zero plan stays feasible because an opening balance is non-negative and so is above any negative floor. This is not an assertion: every property in the suite runs against generated instances carrying credit lines, and credit_lines_change_outcomes_and_only_ever_help checks separately that the lines actually bind (925 of 3000 instances) and that granting one can only ever let more settle, never less.

The general shape is worth stating once, because it is the punchline of the whole repository: a lower bound on a net position preserves the join; an upper bound destroys it. Overdraft protection is a lower bound at zero and credit is the same bound moved down, so both survive. Bilateral limits bound a difference that moves the right way in both coordinates, so they survive too. Exposure caps are an upper bound, and they do not.

Exposure caps kill it. An upper bound on a net position is not preserved under join, because raising other accounts' coordinates raises your inflows. The counterexample is three lines:

ALPHA and BETA each hold 10 and each owe GAMMA 10. GAMMA may absorb at most 10.

Either payment settles alone; neither plan dominates the other; their join is infeasible. There is no greatest plan. resolve therefore refuses an instance carrying exposure caps rather than returning one of the two maximal plans and letting the caller assume it is the maximum:

$ unjam instances/no-greatest.unjam --maximal

Honest limits

• Single currency. One instance is one currency. Multi-currency settlement and payment-versus-payment are not modelled.
• Credit lines are modelled, collateral is not. An account may be granted an intraday line and close as low as -credit, which is what real large-value systems actually run on. What is not modelled is where that line comes from: no collateral, no haircuts, no limit on aggregate central bank exposure.
• No partial settlement. A payment settles whole or not at all. Real systems sometimes split one.
• Priorities: it depends which kind, and the answer is sharp. The solver never asks why a queue is in the order it is in, only that the order is fixed. So a priority scheme that yields a fixed total order per account, such as urgent-before-normal with arrival order inside each class, is already supported: sort the queue that way before writing the file and every guarantee holds verbatim. What is not supported, and cannot be, is a scheme where a payment may jump a stuck one ahead of it. That turns the plan space from prefixes back into arbitrary subsets, and the counterexample in "The claim" above is then exactly the situation: two incomparable maximal answers and no greatest one. Uniqueness is not lost to difficulty there, it is lost because it stops being true.
• The differential claims are about very small instances. The enumeration budget allows a few million plans, but the generated instances are nowhere near it: measured over all 3000 seeds, the mean plan space is 28, the largest is 144, and no instance exceeds 12 payments. So "the solver agrees with exhaustive enumeration on 3000 instances" is a claim about instances of that size. Above it there is no oracle, and what stands in its place is weaker: scales_past_the_reach_of_enumeration runs 400 accounts and 2000 payments and checks feasibility, position consistency, policy agreement, and add-back maximality on every account with a queue remaining. That last one is the only assertion there with anything to say about greatest, and it is a local check, not a global one.
• No wall-clock benchmarks. The complexity argument is in the README and the removal count is asserted in a test; there is no performance claim here because none has been measured properly.
• This is not a settlement system. It is the resolution algorithm on its own, with a file format and a CLI.

Input format

One directive per line, # starts a comment. Payments join the sending account's queue in file order, which is what makes the discipline FIFO.

scale 2                      # decimal places for every amount below
account ALPHA 1_000.00       # name and opening balance
account BETA  0
credit BETA 250.00           # BETA may close as low as -250.00
payment ALPHA BETA 600.00    # appended to ALPHA's outgoing queue
payment BETA ALPHA 600.00
limit ALPHA BETA 500.00      # cap on the net flow ALPHA -> BETA
exposure BETA 900.00         # cap on BETA's closing position

Amounts are parsed into integer minor units and never touch a float. 10.005 at scale 2 is an error, not a silent rounding.

Usage

unjam <file> [--verify] [--maximal] [--subsets] [--policy one|tofeasible]
             [--seed N] [--budget N]

--verify runs the exhaustive oracle alongside the solver and reports whether they agree, which puts the differential check in reach outside the test suite. It only checks where exhaustive enumeration is affordable: past the budget it reports that it skipped, rather than reporting success it has not earned.

Exit status: 0 when everything settled, 1 when the plan is partial, 2 on a bad instance, 3 when --verify found a disagreement.

Library

use unjam::{engine, parse};

let instance = parse::parse(source)?;
let settlement = engine::resolve(&instance)?;

for id in &settlement.settled {
    println!("{:?}", instance.payment(*id));
}

engine::resolve is the whole API. Everything else is diagnostics.

Build

cargo test
cargo run --release -- instances/morning-window.unjam --verify

No dependencies, including in the test suite. The generators that shape the instances live in tests/properties.rs; they draw from a 30-line splitmix64 in src/rng.rs, so a failing property test names the seed that produced it and reproduces exactly.

Reference

Morten L. Bech and Kimmo Soramäki, "Gridlock Resolution in Interbank Payment Systems", Bank of Finland Discussion Papers 9/2001.

The algorithm is theirs. What is here is an implementation whose central property is machine-checked, a statement of that property precise enough to be wrong, and two counterexamples marking where it stops holding.

License

MIT. See LICENSE-MIT.