Audited fixed-block SAT propagation pilot comparing degree-only formulas with degree-plus-pair-bound formulas under two independently implemented cardinality encodings.

pair-excess structural reduction with fixed-block SAT discrimination

Fix a distinguished block WLOG, encode forced point degrees, and measure whether all sound residual pair bounds improve bounded CaDiCaL search under iterative-counter and balanced-totalizer encodings.

Hypothesis: At the same seed-0 60-second cap, adding all sound residual pair bounds reduces conflicts or decisions by at least 2x in both independently validated cardinality encodings.

Test: Generate four hash-bound formulas—two encodings times degree-only versus degree-plus-pair—and compare CaDiCaL conflicts, decisions, propagations, status, and wall time.

The propagation claim is supported by exact raw logs and independent receipt replay. No SAT witness or replayable UNSAT certificate exists, so only a scoped computational-method result is justified.

• The promoted archival list consists of 31 distinct 6-subsets covering all 455 triples and has point-degree profile 12^9 13^6.
• Both cardinality encoders agree with every exact and interval cardinality predicate on all 112636 tested assignments for n<=9.
• At seed 0 and a 60-second cap, adding pair bounds reduced conflicts by 5.897187426140392x in the sequential encoding and 7.566710315728212x in the totalizer encoding.
• No result in this epoch determines whether C(15,6,3) equals 30 or 31.

• python3 checkers/check_pair_pilot_receipt_v1.py artifacts/epoch2-20260808/pair_pilot_receipt.json
• python3 checkers/audit_fixed_block_model_v1.py
• scripts/run_cover_controls_v1.sh
• python3 scripts/fixed_block_sat_pilot_v1.py --self-test
• CaDiCaL 1.7.3 seed 0, 60 seconds on each of four exact CNFs

• .proof-experiments/20260808-162419-dd15d1: 112636 exhaustive cardinality semantic cases passed
• .proof-experiments/20260808-162858-34faa6: four-formula seed-0 pilot completed; all statuses UNKNOWN
• .proof-experiments/20260808-163420-9a3be0: two cover validators accepted the archival cover and rejected both controls
• .proof-experiments/20260808-163428-3a1a23: independent bitmask incidence audit passed
• .proof-experiments/20260808-163702-b4b86d: initial receipt replay caught incorrect formula-growth transcription
• .proof-experiments/20260808-163854-33424f: final hash-bound receipt replay passed

checkers/check_pair_pilot_receipt_v1.py independently recomputes raw hashes, DIMACS headers, CaDiCaL statistics, UNKNOWN statuses, and ratios; checkers/audit_fixed_block_model_v1.py uses a separate bitmask construction for incidence geometry.

not_requested

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

Original model outcome

progress

Public classification

progress

• Certified covering-SAT work on C(12,6,4) -> redundant structural cardinality constraints may materially alter propagation -> pair bounds reduced seed-0 conflicts by 5.90x and 7.57x, but completion benefit remains unconfirmed.

• The archival 31-block list covers every triple.
  .proof-experiments/20260808-163420-9a3be0 with Python-set and C direct-incidence validators · The exact promoted 31-block file with SHA-256 289eed03daa87839214706723ff94bbf615f248044ef5591553daf89e120050a · computed
• The fixed-block residual incidence counts and pair offsets used in the formulas are correct.
  .proof-experiments/20260808-163428-3a1a23 · The normalized block 012345 model · computed
• Both encoders passed exhaustive cardinality semantics for n<=9.
  .proof-experiments/20260808-162419-dd15d1 · 112636 assignment/bound cases · computed
• Both seed-0 matched conflict ratios exceed the predeclared factor-two gate.
  artifacts/epoch2-20260808/pair_pilot_receipt.json and .proof-experiments/20260808-163854-33424f · CaDiCaL 1.7.3, seed 0, 60-second cap, four recorded CNFs · computed

• Pair bounds fail to achieve a 2x conflict reduction in either tested encoding.
  Seed 0, CaDiCaL 1.7.3, 60-second cap, the four recorded formulas · Observed reductions were 5.8972x and 7.5667x. · artifacts/epoch2-20260808/pair_pilot_receipt.json · A formula-generation defect, log-parsing defect, or materially different matched protocol.
• Treat a single-seed UNKNOWN benchmark as evidence for C(15,6,3)>=31.
  This pilot · Timeout/UNKNOWN is neutral and no exhaustive certificate or proof replay exists. · All four raw logs lack SATISFIABLE and UNSATISFIABLE status lines. · A complete, independently regenerated exhaustive split with replayable proofs.

• Five-seed matched propagation confirmation
  Cheapest test distinguishing genuine search-tree improvement from seed-specific propagation overhead. · Run seeds 1..5 on the four existing CNFs, 60 seconds each. · high · open
• 31-to-30 degree-aware repair search
  A constructive hit settles the exact value and supplies information independent of the exclusion route. · Delete each archival block and run fixed-budget incremental one- and two-block repair neighborhoods. · normal · open
• Canonical excess-multigraph splitting
  Every hypothetical cover induces a loopless 4-regular excess multigraph. · Enumerate a small rooted canonical sample only after the five-seed pair-bound gate passes. · normal · open

Objective: Determine whether pair-bound propagation provides robust solver progress across seeds.

First action: Run CaDiCaL seeds 1 through 5 for 60 seconds on each of the four existing CNFs and record a matched ratio table.

Stop condition: SAT stops for dual validation; provisional UNSAT stops for proof replay; collapse of the two-encoding signal redirects to constructive repair; robust signal advances only a small excess-graph sample.

• Run seeds 1 through 5 on all four immutable CNFs at the same 60-second cap.
• Advance canonical excess-multigraph splitting only if both encodings retain an information-rich advantage.
• Redirect to the bounded 31-to-30 repair search if the totalizer signal collapses.
• Pin proof-generation and DRAT/LRAT replay tools before treating any future UNSAT status as evidence.

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

GPT-5.6 Sol served as principal investigator. GPT-5.6 Terra delegates supplied bounded prior-art and verification reconnaissance; their agreement was not treated as validation. Deterministic work used Python 3.12.3, Z3 for small-CNF existential semantic checks, GCC for an independent C cover checker, and CaDiCaL 1.7.3 (SHA-256 7b73df0a6d9cf3c751a1948300e5baff8e82c4d39bcd88f0c063b5f5cfb8b33e). No proof assistant, DRAT replay, or LRAT replay was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1568.3s

Review state

not a result claim

Attempt ID

covering-c1563-20260808-164111-4220bb

No human review recorded.