The optimal sorting network on 5 channels has exactly 9 comparators

Identifier: F:sorting-network-optimal-size-n5
Proof route: smt-clausal
External status: proved
Axiom footprint: sortnet.encoder-faithfulness, sortnet.zero-one-principle, sortnet.symmetry-breaking-soundness

Recorded description

S(5) = 9: some comparator network of 9 comparators sorts every input of length 5, and no network of 8 comparators does.

Formal statement

(and (exists ((n (Network 5 9))) (sorts n)) (not (exists ((n (Network 5 8))) (sorts n))))

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

0 direct dependencies 0 direct dependents

Evidence

lower-unsat-n5

Kind: unsat-certificate
Status: checked

Supports: no network of 8 comparators sorts all 5-input sequences

Checker command

test "$(cargo run --release -q -p axeyum-cnf --example sorting_network -- --n 5 --size 8 --sym full 2>/dev/null | grep -oE '(Unsat|Sat)')" = Unsat

Evidence notes

Optimality-as-UNSAT: no optimizer and no MaxSAT is involved. The verdict is reproduced under every symmetry setting including `--sym none`, which is the control that matters -- an UNSOUND symmetry break manufactures a wrong UNSAT, and would show as Unsat under `full` but Sat under `none`.

upper-sorts-n5

Kind: exhaustive-enumeration
Status: checked

Supports: an explicit 9-comparator network sorts every input

Checker command

test "$(cargo run --release -q -p axeyum-cnf --example sorting_network -- --n 5 --size 9 --sym full 2>/dev/null | grep -c SORTS)" -ge 1

Evidence notes

The witness network is replayed over all 2^5 zero-one inputs by a checker that shares no code with the SAT search. The 0-1 principle makes that sufficient for all totally ordered inputs.

Provenance

{
  "date": "2026-08-14",
  "established_by": "axeyum SAT core, both bounds; symmetry-breaking soundness controlled",
  "source": "lane `sorting-networks` (terminated on an API spend limit); completed by the coordinator",
  "prior_art": [
    {
      "who": "Knuth, TAOCP vol. 3",
      "what": "S(n) for n <= 8 is 0,1,3,5,9,12,16,19",
      "attribution": "standard textbook attribution; this lane did not consult the primary source"
    }
  ]
}