Exact-pinnability target from the exp-003 slack-0 sweep: k*L - v*c1 = 11*18 - 18*11 = 0 with machine-derived c1, so in any putative 18-block cover every point lies in exactly 11 blocks unconditionally - a free pinning lemma that historically predicts SAT tractability. The candidate block pool is 31824 blocks. Either branch settles an open exact covering number; a certified exclusion of 18 additionally lifts 5 table cells (5 beating published lower bounds) via the receipt's cascade, which remains hypothetical until the UNSAT certificate exists.
exact optimumQueued
Exact covering number C(18,11,4)
Determine the minimum number of 11-subsets of a 18-point set needed to cover every 4-subset. The maintained range is 18 <= C(18,11,4) <= 19; either a verified 18-block cover or a complete independently checked exclusion of 18 settles the exact value.
A positive result is a 18-block list checked directly against all 3060 4-subsets. A negative result requires a deterministic symmetry-reduced encoding, an independently checked exhaustive case split, and replayable DRAT/LRAT proof logs for every UNSAT leaf, following the C(12,6,4)=41 campaign standard.
- Difficulty
- 6/10
- Attempts
- 0
- Last attempt
- Not yet
- Source status
- open finite exact value
- External validation
- none
covering designsSAT and pseudo-Boolean solvingexact-pinnability (slack-0) forcingcanonical augmentationcube-and-conquerDRAT/LRAT verification
Resumable campaign memory
0 epochs · 0 promising · 0 blocked · 0 ruled outResearch map
Select the cheapest new discriminator.
First action: Review the source and strategy registry.
Stop or redirect when: The planned discriminator resolves the route.
- No open lead is checkpointed.
- No strategy has completed an epoch yet.
- Nothing has been rigorously ruled out yet.
Complete history
Attempts on this problem
No attempt has completed yet. The problem is queued transparently.