The optimal sorting network on 6 channels has exactly 12 comparators

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

Recorded description

S(6) = 12: some comparator network of 12 comparators sorts every input of length 6, and no network of 11 comparators does.

Formal statement

(and (exists ((n (Network 6 12))) (sorts n)) (not (exists ((n (Network 6 11))) (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-n6

Kind: unsat-certificate
Status: checked

Supports: no network of 11 comparators sorts all 6-input sequences

Checker command

test "$(cargo run --release -q -p axeyum-cnf --example sorting_network -- --n 6 --size 11 --cubes "${TMPDIR:-/tmp}/sortnet-n6-$$" --depth 3 --jobs 4 --cube-sym full 2>/dev/null | grep -oE 'all 51 cubes refuted')" = 'all 51 cubes refuted'

Evidence notes

Four routes, and they do not share a search. Monolithic --sym full: Unsat in 1195s single-core. Cube split depth 3 (51 branches) 151s and depth 4 (322 branches) 138s on 16 cores -- different partitions of the same space, so their agreement is not a re-run. The control that matters is the fourth: --cube-sym none, where every prefix position ranges over EVERY comparator and the suffix gets no symmetry break, leaving output-set equality as the only reduction -- 1441 branches, same UNSAT, 1446.61s. An unsound symmetry break manufactures a wrong UNSAT, so a verdict that survives having every relabelling argument removed is the one worth believing. Every branch streams its own DRAT proof to disk and is read back and re-checked by this repository's backward checker before it counts as refuted. RESOURCE NOTE: this checker needs writable scratch under $TMPDIR -- each of the 4 concurrent branches streams a 30-75 MB certificate, which is deleted as soon as the backward checker accepts it. One observed run exited 1 on a shared box whose /tmp tmpfs was at 80% and climbing under other work; the same command passed immediately before and after. A failure here is far more likely to be a full scratch filesystem than a mathematical one, and stderr (suppressed above) names the failing branch.

upper-sorts-n6

Kind: exhaustive-enumeration
Status: checked

Supports: an explicit 12-comparator network sorts every input

Checker command

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

Evidence notes

The witness network is replayed over all 2^6 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. The size-12 network was also rediscovered independently by the SAT search under all three cube modes, each time passing the same 0-1 replay.

Provenance

{
  "date": "2026-08-14",
  "established_by": "axeyum SAT core via the prefix/suffix cube split; symmetry-breaking soundness controlled by re-refuting under --cube-sym none",
  "source": "lane `sorting-networks-2`",
  "prior_art": [
    {
      "who": "Floyd and Knuth (1966); 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"
    }
  ]
}