💻 computer science

Witness-split + window-cardinality refinement for $r_3(N)$ : Architecture, empirical results, and a structural hard pocket

This paper presents a reproducible computational framework combining witness-splitting, window-cardinality pruning, and hybrid SAT/MIP solvers to rigorously investigate the upper bound of $r_3(212)$ , successfully eliminating most candidate 44-sets while isolating two resistant structural cases that remain unproven despite extensive verification efforts.

Original authors: Mehmet Ergezer

Published 2026-06-04

📖 5 min read🧠 Deep dive

CC BY 4.0

Original authors: Mehmet Ergezer

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you are trying to pack a suitcase (the numbers from 1 to 212) with as many items as possible, but with one strict rule: You cannot pick three items that form a perfect arithmetic pattern.

For example, if you pick the number 2, you cannot also pick 4 and 6, because $2, 4, 6$ is a pattern where each number is 2 more than the last. This is called a "3-term arithmetic progression."

Mathematicians have been trying to figure out the absolute maximum number of items you can fit in this suitcase without breaking the rule. For a suitcase size of 211, the answer is known to be 43. The big question for this paper is: Can you fit 44 items into a suitcase of size 212?

The author, Mehmet Ergezer, didn't just guess; he built a massive digital factory to try and prove that 44 is impossible. Here is how the paper breaks down, using simple analogies:

1. The Strategy: The "Witness Split" Factory

Trying to check every possible combination of 44 numbers out of 212 is like trying to find a specific grain of sand on every beach on Earth. It's too big for one computer to handle.

So, the author used a clever trick:

The Witness: He started with a known "safe" list of 43 numbers that already works.
The Split: He took the 24 most "important" numbers from that safe list and asked the computer to check every possible "Yes/No" scenario for them.
The Result: This broke the impossible mountain of data into 12.5 million smaller, manageable piles (called "chunks"). The computer then tried to solve each pile one by one.

2. The Tools: The "Window" and the "Refinement"

To make the computer faster, the author added two special tools:

The Window Card (The Pruner): Imagine looking through a window at a small section of the suitcase. We already know from previous math that a small window of size 50 can only hold, say, 10 items. The computer uses this rule to instantly throw out any pile that tries to put 11 items in that window. This was the most powerful tool, cutting the number of difficult piles by nearly 30%.
The Refinement (The Deep Dive): If a pile was too hard to solve in 60 seconds, the computer didn't give up. It took that specific hard pile, added more rules to it, and tried again with a longer time limit. This is like taking a locked box, picking a specific lock, and trying again with a bigger key.

3. The Results: The "Hard Pocket"

After running millions of these checks on a supercomputer cluster, here is what happened:

Zero Success: The computer never found a single valid way to pack 44 items. Every time it tried, it hit a wall and said, "Impossible."
The Evidence: This is strong evidence that 44 is impossible, but it's not a formal proof yet. Why? Because there are still a few stubborn piles the computer couldn't finish in time.

The "Hard Pocket" (The Resistant Chunks):
Out of the millions of piles, the author found a tiny, stubborn group of 45 piles that refused to solve even after being given extra time and different tools.

The LP Attack: They tried a different type of math solver (called HiGHS) that looks at the problem like a smooth curve. It failed to solve any of the 45 piles.
The CDCL Attack: They tried a third type of solver (called CDCL) that works like a detective, learning from its mistakes. This one was successful! It solved 18 of the 45 piles.
The Final 2: However, 2 piles (labeled T1c) remained completely unsolved. They resisted the first solver, the second solver, and the third solver. They are the "final boss" of this problem.

4. The Conclusion: The "Unit Gap"

The paper concludes that:

We have a verified list of 43 numbers that works.
We have strong evidence that 44 is impossible, because the computer tried millions of times and failed.
However, because of those 2 final stubborn piles, we don't have a 100% mathematical proof yet. The answer is almost certainly 43, but the "gap" between 43 and 44 is still technically open.

5. The Gift to the Community

Instead of just saying "I give up," the author is releasing all the data. He is handing the 2 stubborn piles to the world as a challenge.

He provides the exact code and data so other mathematicians can try to solve just those two piles.
He even translated the problem into a language for formal proof systems (Lean), inviting computer scientists to try to prove it using logic engines.

In short: The author built a massive digital machine that tried to break the record for packing numbers without patterns. The machine failed to find a way to break the record, but it got stuck on two tiny, incredibly difficult puzzles. The paper says, "We are 99.9% sure the answer is 43, but here are the two final puzzles you need to solve to prove it."

Technical Summary: Witness-Split + Window-Cardinality Refinement for $r_3(212)$

Problem Statement
The paper addresses the exact computation of $r_3(N)$ , defined as the maximum size of a subset of $[1, N]$ containing no nontrivial three-term arithmetic progression (3-AP). While asymptotic behavior is well-studied (e.g., Roth's theorem, Kelley–Meka), the focus here is the finite frontier at $N=212$ . Based on OEIS A003002, $r_3(211) = 43$ . The authors investigate the decision problem: Does there exist a 44-element 3-AP-free subset of $[1, 212]$ ?
The authors have independently verified a 43-element witness, establishing $r_3(212) \ge 43$ . The upper-bound question is whether $r_3(212) \le 43$ . A necessary condition for any hypothetical 44-set is that it must contain both endpoints, 1 and 212; otherwise, it would translate to a 44-set in $[1, 211]$ , contradicting the known value. Thus, the problem reduces to proving the infeasibility of a 44-set containing $\{1, 212\}$ .

Methodology and Architecture
The authors propose a reproducible computational framework combining five components to search for a feasible 44-set:

Decision-Form CP-SAT Model: The problem is encoded using Boolean variables $x_i$ for $i \in [1, 212]$ . Constraints include:
- 3-AP inequalities: $x_a + x_b + x_c \le 2$ for all triples $(a, b, c)$ forming an AP.
- Cardinality equality: $\sum x_i = 44$ (tighter for propagation than inequality).
- Endpoint forcing: $x_1 = x_{212} = 1$ .
- Symmetry breaking: Lexicographical ordering to eliminate reflection symmetry.
Witness-Splitting: To manage the search space, the authors use a verified 43-element witness $A_{43}$ . They rank elements of $A_{43}$ by their AP-incidence degree and select the top 24. The search space is split into $2^{24}$ "chunks" by fixing the values of these 24 variables. Many chunks are pruned immediately if the fixed prefix forces a 3-AP.
Window-Cardinality Pruning: A critical intervention involves adding valid inequalities derived from OEIS A003002. For any window $[a, a+L-1]$ , the sum of variables is bounded by $r_3(L)$ . With $N=212$ , this adds 22,154 inequalities, significantly strengthening the model beyond the raw 3-AP constraints.
Recursive Refinement: Chunks returning UNKNOWN at the broad layer (depth 24) are refined by extending the fixed prefix with the next highest-degree witness variables (depths 40, 48, 56, 64) and re-solving with longer time caps.
Solver Diversity and Engineering: The campaign utilizes a SLURM-based pipeline running on the UMass Unity cluster. It employs:
- CP-SAT (OR-Tools): For the broad pass and recursive refinement.
- HiGHS (MIP): An LP-relaxation-based solver used to attack the hardest "UNKNOWN" chunks.
- CDCL/SAT (CaDiCaL): Used to re-attack chunks resistant to LP methods, generating DRAT proofs for unsatisfiability.

Empirical Results
The campaign processed millions of subproblems across the depth-24 sweep and various refinement levels.

Zero Feasible Solutions: Across all tested subproblems (broad pass, refinements, HiGHS, and CDCL), zero feasible 44-sets were found. This provides strong empirical support for $r_3(212) = 43$ , though it is not a formal proof.
Impact of Window-Cardinality: Enabling window-cardinality inequalities reduced the UNKNOWN rate in broad passes by approximately 28 percentage points (e.g., from ~30% to ~1.65% in controlled batches), making it the most effective pruning layer.
The Structural Hard Pocket:
- From a 100,000-chunk expansion batch, 6,071 chunks returned UNKNOWN.
- A 300-second recap of a random sample of these left 45 resistant chunks (Tier T1).
- HiGHS Attack: A one-hour HiGHS run closed 0/45. An 8-hour audit closed 25/45, leaving 20 chunks (Tier T1b) with dual bounds pinned at 0.0, indicating the LP relaxation provided no certificate of infeasibility.
- CDCL Attack: A pure CDCL/SAT attack on the 20 T1b chunks closed 18/20, generating independently verified DRAT proofs.
- The Residual (T1c): Two chunks (IDs 40959 and 48895) remained UNKNOWN even after 12-hour pure CDCL runs and 4-hour windowed CDCL diagnostics. These two chunks resist CP-SAT, HiGHS (LP-MIP), and CDCL paradigms.

Key Contributions
The paper explicitly frames its contribution as methodological rather than a new exact value for $r_3(212)$ . The specific contributions are:

Architecture: A reproducible framework combining witness-splitting, window-cardinality pruning, and recursive refinement for exact upper-bound searches.
Empirical Account: A detailed analysis of the $N=212, K=44$ campaign, including solver trade-offs and the non-uniformity of the search space (e.g., "middle-out" chunks with specific pin assignments are significantly harder).
Characterization of the Hard Pocket: Identification of a structural obstruction (T1c) that is invariant across CP-SAT, HiGHS, and CDCL paradigms under generous time limits.
Benchmark Release: A tiered release of instances:
- T1a: 25 chunks closed by HiGHS.
- T1b \ T1c: 18 chunks closed by CDCL with DRAT proofs.
- T1c: The final 2 resistant chunks, framed as the sharpest open problem.
- T2/T3: The 6,071 broad UNKNOWNs and the full 12.5M chunk generator for future attempts.
Formalization: A Lean 4 encoding of the T1c targets for formal proof-search systems.

Significance and Claims
The authors modestly claim that while the campaign strongly supports the conjecture $r_3(212) = 43$ , it does not constitute a formal proof due to the unresolved T1c residual. The significance lies in isolating the specific computational barrier:

The gap between certified bounds is exactly one ( $43 \le r_3(212) \le 44$ ).
The failure of LP-based methods (HiGHS) and the partial success of CDCL suggest the hardness is not merely a propagation artifact but a structural property where the LP relaxation gap is tight and the integer infeasibility certificate is combinatorially diffuse.
The paper posits that closing the gap requires either stronger additive-combinatorial bounds (e.g., Fourier-analytic or multi-window partition bounds) or custom branch-and-bound systems that exploit problem-specific symmetries not captured by general-purpose solvers.

The work serves as a benchmark for the community, offering specific, verified instances (T1c) that represent the current limit of general-purpose combinatorial optimization solvers for this class of problems.