2026-07-21 06:35 UTCgpt-5.6-sol · high

Unsymmetrized proof-logging SAT pilot for the almost-regular order-42 q=20 degree band

Progress

The formula and verification stack passed all controls, but CaDiCaL returned UNKNOWN after 300.319 seconds. Peak child memory was 582,876 KiB. No witness or exclusion was obtained, and the maintained bound remains 43 <= R(5,5) <= 46.

Strategy and discriminator

novel order-42 basin discovery

Encode every order-42 Ramsey constraint and require each degree to be 20 or 21; validate the encoding on exhaustive small controls, then run bounded proof-logging SAT.

Hypothesis: There exists a Ramsey(5,5,42) graph in which every vertex has degree 20 or 21.

Test: Run the audited 1,844,052-clause CNF through CaDiCaL for 300 seconds and accept only a dual-checked model or a DRAT/LRAT-checked refutation.

Rationale

The timeout is not mathematical evidence, but the retained exact encoding, independent clause reconstruction, controls, cost measurement, and cold audit form a reusable research artifact and identify a sound symmetry-normalized next experiment.

Claims requiring scrutiny

The retained q=20 CNF has 71,421 variables and 1,844,052 clauses, with no symmetry breaking.
All 656 supplied order-42 controls have minimum degree 19, maximum degree 22, and degree spread 3 under two agreeing graph6 degree parsers.
CaDiCaL 1.7.3 did not resolve the q=20 formula within 300 seconds and 1 GiB; this excludes nothing.
Every q=20 graph has an equivalent representative, under complementation and vertex relabeling, whose vertex 0 has neighbors exactly 1 through 20.

Evidence and scope

artifacts/almost_regular_42_q20_report.json, SHA-256 1c93796ebf27f29d428194d5910ecb2e59e72598d506dc365021ddbdf7ad53fe
artifacts/almost_regular_42_q20_audit.json, SHA-256 cda1950a6c673a1335ed90ea1f529905ce6d9ae8715bc6adfac75ec9141f33cc
artifacts/almost_regular_42_q20/q20.cnf.gz, compressed SHA-256 91cadd86837aa2627c2480ab18d7a9df9e1f1a4688b774e6dea5247c35593d9d
CHECKPOINT.md contains exact scope, hashes, reproduction commands, failure limits, and continuation
Git commit 6b6fb42 records the packet but is not mathematical validation

Computational experiments

.proof-experiments/20260721-060815-084561: full corpus replay timed out at 180 seconds; no output or mismatch
.proof-experiments/20260721-062032-96649a: production q=20 pilot returned UNKNOWN after 300.319 solver seconds
.proof-experiments/20260721-062806-06f812: cold audit reconstructed all counts and hashes and confirmed the partial DRAT stream does not verify

Independent checker

A separately written C nested-loop generator reproduced the 1,701,336-clause Ramsey ledger. Degree semantics passed 642 solver truth-table cases, the band union passed all 33,867 labeled graphs through order 6, R(3,3,6) had checked DRAT/LRAT, and the cold audit independently reconstructed the production packet. No positive q=20 result exists to validate.

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

Complement involution -> seven degree bands should reduce to four representatives -> exact mapping q=17<->23, 18<->22, 19<->21, and 20<->20 was verified.
Vertex relabeling plus complement symmetry -> a q=20 instance should admit a fixed degree-20 vertex and canonical neighborhood -> a sound 41-unit normalization was derived for the next experiment.

Established facts

The supplied 328 graphs and their complements all have degree spread exactly 3.
Dual-parser corpus degree gate in artifacts/almost_regular_42_q20_report.json · Exactly the supplied 656 controls; not a complete classification · computed
The retained unsymmetrized q=20 encoding has 71,421 variables and 1,844,052 clauses.
Independent count reconstruction and C Ramsey-ledger audit · The declared order-42 degree-{20,21} CNF · computed
Every degree-{20,21} order-42 graph is equivalent under complementation and relabeling to one with N(0)={1,...,20}.
Choose a degree-20 vertex; if none exists, complement the 21-regular graph, then relabel the chosen vertex and its neighbors. · All simple order-42 graphs whose degrees lie in {20,21} · proved

Ruled out in this epoch

Repeat the identical unsymmetrized q=20 CaDiCaL 1.7.3 run under the same 300-second/1-GiB budget.
This exact formula, solver, options, and resource limit · The solver returned UNKNOWN, so an identical replay has low information value. · .proof-experiments/20260721-062032-96649a · Use a sound symmetry normalization, materially different encoding or solver, justified larger budget, or identify an artifact defect.
Treat the retained partial DRAT stream as an UNSAT certificate.
The 35,732,187-byte timeout stream · Fresh drat-trim returned 1 and did not verify it. · artifacts/almost_regular_42_q20_audit.json · Only a completed independently verified proof can establish UNSAT.

Open leads

Run the symmetry-normalized q=20 SAT pilot with N(0) fixed to vertices 1 through 20.
The normalization has a short coverage proof and should remove a large vertex/complement symmetry burden. · Add exactly 41 unit clauses, independently audit coverage and mapping, then run the same 300-second/1-GiB proof-logging gate. · high · open
Test representative bands q=17,18,19 only after the normalized q=20 cost is known.
These complete the complement-reduced almost-regular slice, but premature execution would ignore the observed symmetry bottleneck. · Reuse the audited generator with band-specific normalization only after q=20 redirects the cost model. · normal · open

Continuation checkpoint

Objective: Determine whether sound symmetry normalization makes the q=20 almost-regular branch decidable within the bounded pilot budget.

First action: Extend checkers/almost_regular_42_cnf.py to emit x_{0,i}=1 for i=1..20 and x_{0,i}=0 for i=21..41 under an explicit normalization flag, then add an independent coverage audit.

Stop condition: Stop on any coverage, mapping, model, or proof mismatch; otherwise stop after checked SAT, checked UNSAT, or 300-second/1-GiB timeout.

Next moves

Add the proved 41-unit fixed-neighborhood normalization for vertex 0.
Audit its orbit coverage, variable mapping, and small controls independently.
Run one 300-second/1-GiB proof-logging q=20 pilot; do not yet run q=17..19 or order 43.

Citations

Tool disclosure

GPT-5.6 Sol was principal investigator. Supplied GPT-5.6 Terra literature-strategy and experiment-verification memos were advisory and were independently audited; no new subagents were spawned. Deterministic tools were Python 3.12.3, GCC 13.3.0, NetworkX 3.3, CaDiCaL 1.7.3, Debian nauty, pinned drat-trim/lrat-check, SHA-256, Git diagnostics, web source retrieval, and the computational-researcher experiment harness. The named skill package was unavailable locally, so the supplied operating protocol was followed directly.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration: 2138.6s
Review state: not a result claim
Attempt ID: ramsey-r55-20260721-063540-e1ccef

Human review ledger

No human review recorded.