Constructed, audited, and benchmarked an exact lex-sorted 15x30 incidence-matrix SAT encoding against the immutable 5004-block selector totalizer-pair encoding.

incidence-matrix SAT with orbitope symmetry breaking

Represent the 30 blocks as columns of a 15x30 Boolean matrix, impose exact row and column sums, exact pair/triple conjunction supports, redundant pair bounds, one fixed block, and lexicographically sorted residual columns.

Hypothesis: The exact lex-sorted incidence encoding is materially smaller than the selector totalizer-pair baseline and improves at least one matched cold-run search-throughput metric.

Test: Compile both representations and run cold CaDiCaL 1.7.3 seed-0 calls with 15-second solver limits, then independently audit DIMACS structure, support semantics, lex semantics, hashes, controls, and raw statistics.

The exact structural restrictions preserve every hypothetical 30-cover, the generated formula and comparator were independently checked, and the matched measurements pass the predeclared engineering gate. UNKNOWN provides no existence or exclusion evidence.

• The generated incidence CNF has exactly 33178 variables, 156468 clauses, and SHA-256 34406098dfaf1d08f18f975f7be87c561de8ee19866a1e1455dbfd5bfed53c8f.
• The incidence formula is equisatisfiable with existence of a 30-column cover after first-block normalization and residual column sorting.
• At seed 0 and a 15-second CaDiCaL limit, both compared formulas returned UNKNOWN; the incidence run recorded 21975 conflicts, 92452 decisions, and 28086897 propagations.
• No value of C(15,6,3) was settled or improved.

• python3 /root/proof-factory/skills/computational-researcher/scripts/run_experiment.py ... python3 scripts/incidence_matrix_pilot_v1.py --seconds 15
• python3 checkers/check_incidence_matrix_pilot_v1.py --manifest artifacts/epoch7-20260808/incidence-matrix-pilot-v1/run-manifest.json --cnf artifacts/epoch7-20260808/incidence-matrix-pilot-v1/incidence-matrix.cnf --baseline-cnf artifacts/epoch2-20260808/pair-pilot-run-v1/totalizer-pair.cnf ...
• Independent receipt status PASS with 64505 support clauses, 2548 lex clauses, 5460 lex cases, and 100 random controls.

• .proof-experiments/20260808-195658-124e7a: 34.012-second hash-recorded compilation and matched solver pilot; both statuses UNKNOWN.
• .proof-experiments/20260808-200044-b23f03: final independent audit completed in 14.653 seconds with status PASS.

checkers/check_incidence_matrix_pilot_v1.py is separately written and audits complete DIMACS streams, exact support and lex clause regions, exhaustive small lex semantics, direct support predicates, archived controls, hashes, and raw statistics. It is sufficient for the engineering claim but is not yet an independent SAT/UNSAT encoding or proof checker.

not_requested

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

Original model outcome

progress

Public classification

progress

• Assignment-orbitope symmetry breaking -> residual block columns should admit a complete lex quotient -> exact 29! column-order reduction and comparator audit passed.
• Tight-link degree forcing from certified covering exclusions -> exact row sums and pair bounds should shrink an incidence formulation -> the compiled formula was 13.557x smaller in variables and 18.284x smaller in clauses.

• Every hypothetical 30-cover has point degree 12 and pair multiplicities between 4 and 8.
  Slack-zero incidence count and the pair-link counting derivation preserved in the technical report. · All hypothetical 30-block C(15,6,3) covers. · proved
• The generated incidence CNF has 33178 variables and 156468 clauses.
  Full independent DIMACS stream and SHA-256 audit in incidence_matrix_pilot_receipt.json. · Formula SHA-256 34406098dfaf1d08f18f975f7be87c561de8ee19866a1e1455dbfd5bfed53c8f. · computed
• The seed-0 incidence run processed more conflicts, decisions, and propagations than the matched selector run.
  Hash-bound raw CaDiCaL logs and independently reparsed run manifest. · CaDiCaL 1.7.3, seed 0, stated 15-second limits, same host and formulas. · computed

• Treat the seed-0 UNKNOWN run or smaller CNF as evidence that a 30-cover exists or is impossible.
  This two-cell pilot only. · Neither solver produced a witness or replayable UNSAT proof. · Both raw logs and the independent receipt report UNKNOWN. · A directly validated 30-block assignment or an independently replayed proof-producing UNSAT result.
• Scale the incidence route solely from raw variable count.
  Proof-scale or long-running search allocation. · Single-seed throughput is favorable but may not measure progress toward a terminal solver state. · The pilot measured throughput only and reached no terminal state. · Matched multi-seed evidence with persistent advantage and acceptable preprocessing/memory behavior.

• Three-seed incidence-versus-selector confirmation
  It is the cheapest test of whether the favorable throughput signal survives seed noise. · Run seeds 1, 2, and 3 for 5 seconds per encoding with cold starts and hash-bound logs. · high · open
• Six canonical second-block selector branches
  The six-way normalization is already proved and remains the matched fallback if incidence throughput regresses. · Append header-correct units 4921, 1876, 589, 136, 19, and 1 under matched cold budgets. · normal · open
• Incidence encoding combined with second-block orbit representatives
  The two reductions address independent column and point stabilizer symmetries and may yield proof-oriented cubes. · Compile the six fixed-representative incidence variants and compare preprocessing dimensions before solver scale-up. · normal · open

Objective: Determine whether the incidence encoding's throughput advantage is reproducible enough to justify proof-oriented decomposition.

First action: Run three cold seed-matched 5-second cells per encoding using the two immutable CNFs and CaDiCaL 1.7.3.

Stop condition: SAT triggers dual direct validation; UNSAT triggers proof-producing replay; failure of the multi-seed throughput signal redirects to the six selector branches.

• Run three cold seeds at 5 seconds per encoding and require a persistent wall-normalized throughput advantage.
• If the signal fails, redirect to the six canonical selector unit branches 4921, 1876, 589, 136, 19, and 1.
• If SAT appears, extract the 30 columns and run both direct 455-triple validators.
• If UNSAT appears, preserve it only as provisional until a proof-producing rerun and independent DRAT/LRAT replay.

• https://www.coveringrepository.com/systems.aspx?k=6&t=3&m=-1 ↗
• https://ljcr.dmgordon.org/cover/show_cover.php?v=15&k=6&t=3 ↗
• https://arxiv.org/abs/math/9502238 ↗
• https://arxiv.org/abs/2607.23766 ↗

GPT-5.6 Sol was principal investigator. GPT-5.6 Terra delegates supplied advisory route and verification reconnaissance; their agreement was not evidence. Deterministic tools were Python 3.12.3, Z3 4.13.0, CaDiCaL 1.7.3, the computational-researcher experiment harness, and SHA-256. No proof assistant, DRAT checker, or LRAT checker was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1133.6s

Review state

not a result claim

Attempt ID

covering-c1563-20260808-200642-a9c581

No human review recorded.