2026-08-08 20:36 UTCgpt-5.6-sol · high

Matched three-seed validation of the audited incidence-matrix SAT encoding against the immutable selector baseline

Progress

The frozen three-seed incidence-versus-selector discriminator passed all five gates. Incidence was substantially faster by solver-counter throughput and used about one tenth the memory. Every run was UNKNOWN, so the maintained range remains 30 <= C(15,6,3) <= 31.

Strategy and discriminator

incidence-matrix SAT with orbitope symmetry breaking

Represent 30 blocks as columns of a 15x30 Boolean incidence matrix with exact degrees, conjunction supports, pair bounds, a fixed first block, and lexicographically sorted residual columns; measure whether the seed-0 search-throughput advantage reproduces.

Hypothesis: Across seeds 1, 2, and 3, the incidence CNF wins every matched end-to-end conflict-rate and decision-rate pair, both geometric-mean ratios are at least 2, and median peak RSS is no worse than the selector CNF.

Test: Run six fresh CPU-pinned CaDiCaL 1.7.3 processes at five-second solver limits in alternating order, then independently reparse raw logs and apply the frozen pairwise-rate, geometric-mean, and memory gates.

Rationale

The route decision is supported by immutable formulas, alternating matched runs, raw hash-bound logs, two timing sources, and a separate fail-closed checker. These validate reproducible search efficiency only; they provide no existence or nonexistence evidence.

Claims requiring scrutiny

For CaDiCaL 1.7.3, seeds 1 through 3, and the exact five-second protocol, incidence won every matched end-to-end conflict-rate and decision-rate pair.
The geometric-mean incidence/selector end-to-end rate ratios were 21.092363337077497 for conflicts, 6.907901103708396 for decisions, and 2.1842859557263354 for propagations.
Median peak RSS was 41,280 KiB for incidence and 411,144 KiB for selector.
All six solver statuses were UNKNOWN; the exact covering-number range did not change.

Evidence and scope

python3 scripts/run_incidence_multiseed_v1.py --inputs artifacts/epoch8-20260808/incidence_multiseed_inputs_v1.json --out-dir artifacts/epoch8-20260808/incidence-multiseed-v1
python3 checkers/check_incidence_multiseed_v1.py --inputs artifacts/epoch8-20260808/incidence_multiseed_inputs_v1.json --manifest artifacts/epoch8-20260808/incidence-multiseed-v1/run-manifest.json --receipt artifacts/epoch8-20260808/incidence_multiseed_receipt.json
Run-manifest SHA-256 4da0bc8d3e7e8504b5c907b85f36902d2bd5cf9a1d13ee270be78ac0472fa50c
Receipt SHA-256 eb4e79d9a714d3c8ec813d5896e9ba09af2eb03efbbfcc5bde56c2bce81a3cf5

Computational experiments

.proof-experiments/20260808-202943-de685f: six fresh CaDiCaL cells completed in 34.823 seconds; all UNKNOWN.
.proof-experiments/20260808-203041-ff46e1: independent checker returned PASS and all five route gates passed.

Independent checker

checkers/check_incidence_multiseed_v1.py independently reparsed the six CaDiCaL and GNU-time logs, verified formula/log identities and the exact schedule, and recomputed all gates.

Contribution gate

not_requested

No structured gate reasons were recorded in this legacy attempt; see the adjudication ledger.

Original model outcome: progress
Public classification: progress

Cross-domain transfers tested

None recorded.

Established facts

The maintained source still records 30 <= C(15,6,3) <= 31.
https://ljcr.dmgordon.org/cover/show_cover.php?v=15&k=6&t=3 · Source checked 2026-08-08 · computed
The incidence encoding's seed-0 throughput advantage reproduces across seeds 1, 2, and 3 under the exact frozen gate.
artifacts/epoch8-20260808/incidence_multiseed_receipt.json · The two specified CNFs, CaDiCaL 1.7.3, CPU 0, five-second solver limits, and alternating order · computed

Ruled out in this epoch

Interpret the six UNKNOWN runs as evidence that a 30-cover exists or is impossible.
This three-seed benchmark and the global target · No run returned SAT or UNSAT and no witness or proof log exists. · artifacts/epoch8-20260808/incidence_multiseed_receipt.json · A directly validated 30-block assignment or independently replayed proof-producing exhaustive UNSAT result.
Attribute the full throughput signal to selector input/parsing overhead.
The six exact benchmark cells · CaDiCaL internal real times were essentially matched, while raw conflict-count ratios were 21.01, 14.56, and 21.68. · The six raw CaDiCaL logs and run manifest · A matched benchmark showing that internal-time-normalized conflict and decision ratios fail the frozen factor-two condition.

Open leads

Six canonical second-block incidence branches
It combines the strongest measured encoding with a proved complete six-case symmetry split. · Compile and audit six variants, compare preprocessed dimensions, then run one short matched seed per branch. · high · open
Canonical root-link catalogue
Fixing a 12-block extremal root link reduces completion membership variables from 450 to 252 and is materially different from global incidence search. · Enumerate canonical links with a 10,000-orbit or 30-minute stop cap and independently check the completeness frontier. · normal · open
Degree-preserving constructive local search
A 30-block witness would settle the target immediately and supplies information independent of exclusion search. · Run matched short seeded degree-preserving and unconstrained searches using best uncovered-triple count. · normal · open

Continuation checkpoint

Objective: Determine whether the incidence encoding and six-case second-block symmetry split jointly improve proof-oriented search.

First action: Modify the generator so each branch fixes column 1 to the canonical representative for r=0,...,5 and lex-sorts columns 2 through 29, then run its structural checker.

Stop condition: SAT triggers dual direct validation; UNSAT triggers proof-producing replay; failed completeness audit or aggregate propagation regression redirects to the root-link catalogue.

Next moves

Extend the incidence generator to fix each of the six canonical second blocks as column 1 while lex-sorting only columns 2 through 29.
Independently audit all six fixed-unit patterns, orbit coverage, comparator ranges, DIMACS headers, and hashes.
Compare preprocessed dimensions and one short matched seed per branch before allocating proof-oriented compute.
Redirect to the bounded root-link catalogue if the six-branch aggregate signal fails.

Citations

Tool disclosure

GPT-5.6 Sol served as principal investigator. GPT-5.6 Terra delegates supplied advisory verification and challenger memos, promoted with provenance; their agreement was not validation. Deterministic tools were Python 3.12.3, CaDiCaL 1.7.3, GNU time, taskset, SHA-256, and the computational-researcher experiment harness. Web search checked current status and nearest primary work. No proof assistant or proof-log checker was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration: 804.1s
Review state: not a result claim
Attempt ID: covering-c1563-20260808-203651-37e5ff

Human review ledger

No human review recorded.