FixtureA league scheduler that explains its conflicts
Can a whole season be scheduled around everyone’s constraints — and if not, which ones are to blame?
Summary
A SAT solver written from scratch schedules a full season, proves the minimum number of home/away breaks, and explains impossible constraint sets.
What you can do
- Schedule single or double round-robins for 2–20 clubs with nine kinds of rules.
- Minimise home/away breaks and get “Optimal (proven)” when the solver shows nothing better exists.
- When rules clash, see the smallest set that cannot hold together and relax one with a click.
- Every schedule is re-checked by an independent validator, and every proof by a separate checker.
- Export CSV and a calendar (ICS) per club, or share the whole setup as a link.
How it works
The league becomes a CNF formula: match, round and venue variables, cardinality encodings, and a selector literal per rule. A CDCL SAT solver written from scratch — watched literals, clause learning, VSIDS, restarts — solves it in a Web Worker. Tightening a totalizer bound until it is UNSAT proves the minimum; assumption cores shrunk to a minimal set explain infeasibility.
The hard part
Writing a capable SAT solver in TypeScript and turning its raw output — cores and proofs — into explanations a league organiser can act on.
Validation
- Single round robin, minimum breaks (de Werra: n − 2)
- n − 3 proven impossible, n = 4…16
- Mirrored double round robin (3n − 6)
- proven for n = 4…12
- Random 3-SAT, n = 20, ratio 4.26, vs brute force
- 1 000 / 1 000 agree
- Pigeonhole PHP(n+1, n)
- UNSAT up to PHP(9, 8), proofs checked
- Example league
- optimal 18 breaks proven in ≈ 0.1 s