Schur numbers, lower bounds by sum-free partitions

# Schur numbers: lower bounds by sum-free partitions ## Goal A set of integers is *sum-free* if it contains no `x, y, z` with `x + y = z`; `x = y` is allowed, so `{1, 2}` is not sum-free (`1 + 1 = 2`). The Schur number `S(r)` is the largest `N` such that `{1, ..., N}` can be partitioned into `r` sum-free sets. (Some authors define it as `N + 1`, the least `n` forcing a monochromatic solution; Wikipedia's `S(5) = 161` is the same fact as the `S(5) = 160` used here.) `S(1..5) = 1, 4, 13, 44, 160`; the last was settled by Heule's 2-petabyte SAT proof in 2017. Nothing beyond `r = 5` is known exactly, and every known lower bound is an explicit partition. `colouring.py` exposes colouring(r: int, time_budget: float, seed: int) -> list[int] returning a list of Python ints in `range(r)`; entry `i` is the colour of the integer `i + 1`. Its length `N` is what you are maximising. Instances are labelled by `r`: | label | r | record N | |---|---|---| | `6` | 6 | 536 | | `7` | 7 | 1696 | | `8` | 8 | 5362 | ## Metric metric = mean over instances of N(instance) / record(instance) The eval checks every `x + y = z` exactly (colour classes as bitmasks: `x` has a partner in its class `B` iff `B & (B >> x)` is non-zero). A single monochromatic triple fails the run (`wrong_answer`, naming `x + y = z`). Entries that are not ints in `range(r)` fail the run. A list longer than `2 × record` is refused rather than checked. Anything above 1.0 on an instance is a new lower bound for that `S(r)` and is flagged in `records_beaten`. `ZT_EVAL_SEED` only changes the `seed` handed to your solver; the instance set is fixed. ## Records None of the three is known to be optimal; the best upper bounds (via `S(r) ≤ R_r(3) − 2`) are far above them. Each record partition was re-verified by this pack's checker before being pinned. | label | record | source | status | |---|---|---|---| | `6` | 536 | H. Fredricksen, M. M. Sweet, "Symmetric sum-free partitions and lower bounds for Schur numbers", EJC 7 (2000) R32 — the symmetric partition is printed in the paper | open | | `7` | 1696 | F. Rowley, "An improved lower bound for S(7) and some interesting templates", arXiv:2107.03560 (2021), ancillary file; supersedes 1680 (Fredricksen–Sweet 2000) | open | | `8` | 5362 | N. Bengone, A. Brouk, M. Grinsztajn, T. Helbert, B. Lugherini, A. Rimmel, J. Tomasik, "Shifted S-templates and improved lower bounds for Schur numbers", arXiv:2607.15034 (2026): a width-10 template applied to the Fredricksen–Sweet 536-partition, `S(r+2) ≥ 10 S(r) + 2`; supersedes 5286 | open | For orientation only (not instances): `S(9) ≥ 17 803` and `S(10) ≥ 60 948` (Ageron, Casteras, Pellerin, Portella, Rimmel, Tomasik, arXiv:2112.03175, 2022). ## Constraints - Standard library only. No numpy, no scipy. The eval rejects other imports. - Respect `time_budget` (seconds, per call). The eval fails a call that runs more than 25 % over. - Deterministic given `seed`: use `random.Random(seed)`. ## Iterating - `ZT_EVAL_INSTANCES=6,7` restricts the eval to a subset of labels (default `6,7,8`). - `ZT_EVAL_PER_INSTANCE_SECONDS=5` shrinks the per-instance budget (default 30; the full eval takes about 90 s). - `ZT_EVAL_SEED` only changes the `seed` handed to your solver. ## Ideas that are known to matter (check the journal before repeating one) - Recurrences from small partitions (the baseline uses Schur's `S(r+1) ≥ 3 S(r) + 1`): Abbott–Hanson `S(r+2) ≥ 9 S(r) + 4`, Rowley's templates `S(r+3) ≥ 33 S(r) + 6`, `S(r+4) ≥ 109 S(r) + 39`, `S(r+5) ≥ 376 S(r) + 160`, and the 2026 shifted template `S(r+2) ≥ 10 S(r) + 2`. From `S(5) = 160` and `S(6) ≥ 536` these already give 1444 (`r = 7`) and 5362 (`r = 8`); the `r = 6` record is pure search. - Symmetry: every record partition is (almost) symmetric, `colour(x) = colour(N + 1 − x)`. Halve the search space by imposing it; Fredricksen–Sweet also track the "e-depth" (how far a partition of `[1, n]` extends) to pick which partial partitions to grow. - Rowley's `S(7) ≥ 1696` came from taking a six-colour partition of `[1, 536]`, giving 537 the new colour, forcing symmetry about 1697, and running a plain tree search upward from 538: the integers just above 537 are already heavily blocked, so the search is narrow. - Local search: state = a colouring, cost = number of monochromatic `x + y = z`; the classic SAT encoding (one clause per triple) responds well to WalkSAT-style flips. Use the bitmask trick from the checker so that evaluating a flip costs a few big-int operations. - Start from a good partition of a shorter interval and extend greedily, backtracking only over the last few dozen integers. Write one honest line in `NOTES.md`: the idea, and which instance it helped. Simpler is better: all else equal prefer the shorter solver, and treat removing code for an equal score as a win. Log every experiment, including discards, in your results.tsv.