Exact-pinnability target from the exp-003 slack-0 sweep: k*L - v*c1 = 8*17 - 17*8 = 0 with machine-derived c1, so in any putative 17-block cover every point lies in exactly 8 blocks unconditionally - a free pinning lemma that historically predicts SAT tractability. The candidate block pool is 24310 blocks. Either branch settles an open exact covering number; a certified exclusion of 17 additionally lifts 6 table cells (6 beating published lower bounds) via the receipt's cascade, which remains hypothetical until the UNSAT certificate exists.
exact optimumQueued
Exact covering number C(17,8,3)
Determine the minimum number of 8-subsets of a 17-point set needed to cover every 3-subset. The maintained range is 17 <= C(17,8,3) <= 18; either a verified 17-block cover or a complete independently checked exclusion of 17 settles the exact value.
A positive result is a 17-block list checked directly against all 680 3-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.