Strongly Solving $7 \times 6$ Connect-Four on Consumer Grade Hardware

Markus B\"ock

REVIEW 3 major objections 5 minor 1 cited by

Strongly Solving $7 \times 6$ Connect-Four on Consumer Grade Hardware

T0 review · 3 major / 5 minor · reviewed 2026-08-06 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read A complete win/draw/loss lookup table for every 7×6 Connect-Four position has been built on a single CPU core in 47 hours.

desk verdict A real engineering feat and likely the first full 42-ply Connect-Four lookup table, but the correctness claim currently leans on an unverified BDD implementation and no independent label check. read the letter →

arxiv 2507.05267 v1 pith:4XODYRZC submitted 2025-07-01 cs.AI

Markus Böck This is my paper · ORCID

classification cs.AI

keywords Connect-Fourstrongsolutionlookuptablebinarydecisiondiagramssymbolicsearchretrogradeanalysisgamesolvingcombinatorialgames

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper claims that a complete strong solution of the standard $7 \times 6$ Connect-Four game—a lookup table giving the win/draw/loss outcome for every reachable position—is feasible on ordinary hardware. The author reports building an 89.6 GB table in 47 hours on one CPU core with 128 GB main memory, using binary decision diagrams (BDDs) and a compressed column-wise position encoding. If correct, this is the first look-up-table-style strong solution of the game, meaning any position can be evaluated instantly rather than by search. The paper also reproduces known unique-position counts, solves the $6 \times 6$ board, and provides an $\alpha$-$\beta$ search that uses the table to find fastest-win or slowest-loss moves.

What carries the argument

The load-bearing object is the compressed column-wise BDD encoding, which uses $\mathrm{width}\cdot(\mathrm{height}+1)+1$ Boolean variables per board rather than the classical two-variables-per-cell scheme: each cell gets one variable, the lowest empty cell in each column is forced to true, and all filled cells below it are encoded by the owner's color, with an extra row added to support the logic. This encoding shrinks the BDD for all $7 \times 6$ positions from about 95 million to 59.9 million nodes, making the symbolic forward pass and retrograde analysis tractable with 128 GB memory. The computation is carried out by a minimal hand-written C BDD library that pre-allocates all nodes and uses manual reference counting, and by a retrograde analysis that propagates win/draw/loss from the fully filled ply-42 positions back to the empty root, storing only the win and loss BDDs since $\mathrm{draw} = \neg \mathrm{win} \land \neg \mathrm{loss}$.

What would settle it

Take a random sample of stored positions (for example, all 184,275 eight-ply positions or a million uniformly chosen positions), decode each into a board, and run an independent search-based Connect-Four solver on them; any disagreement with the table's win/draw/loss classification would refute the table. Additionally, decode a random sample of variable assignments from the BDDs and verify that each decodes to a legal position in bijective correspondence with the encoding rules.

Watch

Extended reading notes

Core claim

The central claim is that the previously believed-infeasible full retrograde solution of $7 \times 6$ Connect-Four can be brought within reach of consumer hardware. Using a BDD-based symbolic search with a compressed column-wise variable encoding—where each column's lowest empty cell is marked true and filled cells below it carry the owner's color—the author computed the win/draw/loss classification of all unique positions (about $4.53 \times 10^{12}$) and stored the result as per-ply BDDs occupying 89.6 GB. The computation took 47 hours on a single AMD Ryzen 5950X core with 128 GB RAM, and the resulting table agrees at every ply with the partial solution previously reported for the same board. The paper further reports novel position counts (including all $7 \times 7$ positions), a reproduction of the $6 \times 6$ solution in 2:13 hours, and a confirmation that the first player wins in 41 plies by opening in the center column.

Load-bearing premise

The whole table rests on the assumption that the compressed column-wise encoding maps every legal position to exactly one Boolean assignment and that the custom BDD library's operations on those assignments are error-free; the paper gives no formal proof of either.

Editorial extensions

If this is right

The full 42-ply game is stored: any $7 \times 6$ Connect-Four position can be classified as a first-player win, draw, or loss by consulting the table, with no search required.
Consumer-grade hardware (128 GB RAM, one CPU core) is enough to reproduce the solution in under two days, which makes the method practical for other combinatorial games of similar state-space size.
The compressed column-wise encoding could become a standard ingredient in symbolic game solving for boards wider than they are tall, where it outperforms the classical cell-wise encoding.
The position counts for boards such as $7 \times 7$ (161,965,120,344,045 unique positions) are now known and can serve as a benchmark for other exact enumeration methods.
With the table, alpha-beta search can be pruned heavily: verifying the first-player win takes 9.2 seconds instead of 128 seconds, a reduction in explored positions by a factor of six.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

If the table is correct, it effectively settles the 'who wins from any position' question for the standard board, leaving distance-to-win and move-quality as the more interesting remaining questions, which the table plus search can now map.
The same compression idea may transfer to other gravity-based column-drop games (for example, larger Connect-N variants or scoring versions), though the paper notes performance degrades as the number of rows grows; testing those variants would be a natural next step.
Because the paper gives no formal correctness proof for the encoding or the BDD library, an independent verification by a second, search-based solver on a sample of positions is prudent before treating the table as ground truth in other systems.
The 89.6 GB table size means 'look-up-table solution' is accurate but not cheap to distribute or query on small devices; future work could investigate lossy or hierarchical compressions of the same BDDs, a direction the paper does not explore.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

The actual news here is concrete: a 42-ply win/draw/loss table for standard 7x6 Connect-Four, stored as BDDs in 89.6 GB, produced in 47 hours on one CPU core with 128 GB RAM. That is a genuine first, and the open-source artifact plus the new 7x7 position counts are useful. The paper also reproduces known Tromp totals and the 6x6 solution, which is the right kind of sanity check.

What the paper does well is mostly engineering: a compressed column-wise encoding that avoids the exponential blowup of the old cell-wise encoding, a minimal hand-written BDD library, and careful handling of terminal states. The appendix is internally consistent, and the per-ply counts sum to the known totals. As a demonstration that symbolic search can scale to 7x6 on consumer hardware, it is credible.

The soft spot is not the encoding, exactly. The stress-test note is right: the forward-pass counts largely constrain the state enumeration, so ghost states would show up as inflated totals. What the counts do not constrain are the retrograde labels. A bug in the pre-image logic, the mirrored transition relation, the complement/negation steps, or the manual reference-counting garbage collector could systematically misclassify positions while preserving the counts. Nothing in the paper independently cross-checks any stored outcome against a different solver, and there is no verification script or checksum for the 89.6 GB table. For a claim of this size, that is a real gap, not a nitpick. The timing inconsistencies between Section 4.1 and the appendix are minor and fixable.

I also would have liked a formal statement that the compressed encoding is injective and complete. The count agreement with Tromp makes a massive injectivity failure unlikely, but a short proof would remove the last doubt.

Who is this for? Researchers in game solving, BDD-based symbolic search, and anyone who cares about reproducible large-scale artifacts. It deserves serious peer review, but the referee should insist on a verification artifact: a commit hash, a script that checks a sampled set of positions with an independent solver, and ideally a checksum for the table. Without that, the strong-solution claim is an impressive but unverified engineering report.

Referee Report

3 major / 5 minor

Summary. The paper presents a symbolic-search approach based on reduced ordered binary decision diagrams (BDDs) to strongly solve 7x6 Connect-Four. It claims to have produced an 89.6 GB lookup table containing win/draw/loss values for all 4,531,985,219,092 positions in 47 hours on a single CPU core with 128 GB RAM, using a compressed column-wise state encoding and a custom C BDD library. The authors also report reproducing known position counts and the 6x6 solution, and provide an alpha-beta solver and an opening book that query the table. The main contribution is the artifact and the claim that this is the first lookup-table-like strong solution of the standard board size.

Significance. If the table is correct, the paper demonstrates that a full strong solution of standard Connect-Four can be stored and queried on consumer-grade hardware, which would be a notable engineering result. The work is reproducible in principle: the code is open source, the artifact is deposited on Zenodo, and the forward-pass counts match the known Tromp totals. The approach is non-circular in that no free parameters are fitted and the validation uses external counts. However, the significance depends entirely on the correctness of the custom BDD pipeline, including the compressed encoding and the hand-written BDD library; the current paper provides insufficient evidence for that correctness, and the load-bearing validation therefore needs to be strengthened.

major comments (3)

[§4.2, Appendix Table 2] The validation described in this section—per-ply totals matching Tromp, reproduction of the 6x6 solution, and agreement with Edelkamp et al.—does not verify the 4.5 trillion individual win/draw/loss labels in the 89.6 GB table. A bug in the retrograde equations, in the complement or draw computation, in the mirrored transition relation, or in the manual reference-counting garbage collector could preserve all per-ply aggregate counts while systematically misclassifying positions. I request an independent label check: sample positions, for example all 184,275 8-ply positions already used for the opening book, and compare the table's outcome with an independent negamax/alpha-beta solver; in addition, check the local retrograde equation for a sample of stored non-terminal positions, namely value(p) = max over moves of the negated value of the successor, with draws handled by the standard rule. Finally, publish a checksum or hash of the table files so that readers can verify the artifact's integrity.
[§3.1] The compressed column-wise encoding is described only informally. No theorem or proof establishes that the mapping between legal Connect-Four positions and Boolean assignments satisfying the stated invariant (lowest empty cell true, all cells above false, occupied cells below marked by player color) is a bijection, nor that the transition relation preserves this invariant after every move. The fact that the forward-pass count matches Tromp's known total is good empirical evidence, but it is not a substitute for a correctness argument, especially because a collision or missing state in the encoding would silently corrupt the table. Please add a precise invariant and an inductive proof (or at least a proof for all reachable states) that every legal position has exactly one representation and every represented reachable assignment corresponds to exactly one legal position.
[§3.2] The custom C BDD library is a black box at the heart of the result, yet the paper gives no correctness evidence for it. The text states that no special improvements were made and that garbage collection is manual, but it does not describe the implementation of the core operations (apply, complement, unique table, sat-counting), nor any runtime invariant checks. At the 7x6 scale (over 1.1 billion nodes), a subtle bug in any of these routines could produce plausible-looking but wrong results. I ask for (i) unit tests of the BDD operations against a naive truth-table implementation on small functions, (ii) a description of how reducedness and uniqueness are maintained, and (iii) a full reproduction check of the 6x6 solution that goes beyond total counts, for example by comparing hashes of the generated per-ply BDDs with the previous solution or by verifying a sample of positions with an independent solver.

minor comments (5)

[§1] The phrase "alá alpha-beta pruning" should be "à la alpha-beta pruning", and "trades of memory" should be "trades off memory".
[§2.2] The displayed formula for the transition relation, "trans(S, S′) = W aprea(S) ∧ effa(S′) ∧ framea(S, S′)", appears garbled; it should presumably be a disjunction over actions a of (pre_a(S) ∧ eff_a(S′) ∧ frame_a(S, S′)). Please correct the notation.
[§3.1] "we take following approach" should be "we take the following approach", and the sentence describing the variable ordering for the standard encoding is hard to parse; a small example would help.
[§4.2] "ply 27 takes the most storage to store" is awkward; consider "ply 27 requires the most storage".
[References] References [14] and [15] are both attributed to Tromp, but the text seems to date the 8-ply database to 1995 and the medium-board weak solutions to 2008; please make sure each citation points to the intended work. In addition, the Zenodo artifact entry [5] should include a version and a checksum.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the 7x6 Connect-Four table is computed from the game rules by retrograde equations and checked against independent prior counts.

full rationale

The paper's derivation chain is self-contained and non-circular. The solution is produced by a forward state-space enumeration followed by a retrograde classification: win_i, draw_i, and lost_i are defined directly from pre-image operations on the next ply's classifications, with terminal states handled according to the rules of Connect-Four. No fitted parameter is renamed as a prediction, and no target result is used as an input to the solver. The compressed column-wise encoding is an implementation choice; the paper does not define the win/draw/loss outcome in terms of that encoding. Validation is external: the position counts are confirmed against Tromp's published totals, and the 6x6 solution reproduces the independent result of Edelkamp, Kissmann, and Rohte. The only self-citation, Boeck [5], points to the produced Zenodo artifact and is the output of the computation rather than a load-bearing input. Concerns about the correctness of the hand-written BDD library or the injectivity of the encoding are verification risks, not circularity, because they do not show that any derived claim is equivalent to its own inputs by construction.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

The paper's result is an exact computation; the ledger is clean of fitted parameters and invented entities. The load-bearing assumptions are the correctness of the new compressed encoding and of the hand-written BDD engine, neither of which is formally proved.

assumptions (4)

domain assumption All legal Connect-Four positions on a 7x6 board are reachable within 42 plies and the standard win/loss/draw rules apply.
The retrograde analysis in Section 2.2 and Section 4.2 relies on the standard game definition and bounded ply depth.
ad hoc to paper The compressed column-wise encoding from Section 3.1 maps every legal position to a unique assignment of width times (height plus 1) plus 1 Boolean variables.
The encoding is central to the 47-hour performance, but the paper offers no proof of injectivity or completeness.
ad hoc to paper The custom C BDD library correctly implements reduced ordered BDD operations, reference counting, and sat-counting.
Section 3.2 describes a minimal hand-written BDD library; correctness is assumed and not formally verified.
standard math The external counts from Tromp and the partial solution from Edelkamp et al. are correct as used for validation.
Used as ground truth to confirm position counts and per-ply results.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Strongly Solving $7 \times 6$ Connect-Four on Consumer Grade Hardware." pith.science (2026). https://pith.science/paper/4XODYRZC

@misc{pith2026250705267,
  author       = {Pith},
  title        = {Pith review of: Strongly Solving $7 \times 6$ Connect-Four on Consumer Grade Hardware},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/4XODYRZC}},
  note         = {Machine review of arXiv:2507.05267}
}

abstract

While the game Connect-Four has been solved mathematically and the best move can be effectively computed with search based methods, a strong solution in the form of a look-up table was believed to be infeasible. In this paper, we revisit a symbolic search method based on binary decision diagrams to produce strong solutions. With our efficient implementation we were able to produce a 89.6 GB large look-up table in 47 hours on a single CPU core with 128 GB main memory for the standard $7 \times 6$ board size. In addition to this win-draw-loss evaluation, we include an alpha-beta search in our open source artifact to find the move which achieves the fastest win or slowest loss.

Figures

Figures reproduced from arXiv: 2507.05267 by the authors.

**Figure 2.** Investigation of BDD sizes for the 7 × 6 board configuration [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

Multi-agent imitation learning with function approximation: Linear Markov games and beyond
cs.LG 2026-02 conditional novelty 7.0 of 10

In linear Markov games, behavior cloning's sample complexity hinges on a feature-level concentrability coefficient, and the interactive algorithm LSVI-UCB-ZERO-BC removes concentrability dependence entirely, scaling o...

Reference graph

Works this paper leans on

16 extracted references · 14 canonical work pages · cited by 1 Pith paper

[1]

Puzzle Wright Press (2010)

Allen, J.D.: The Complete Book of Connect 4: History, Strategy, Puzzles. Puzzle Wright Press (2010)

work page 2010
[2]

Allis, L.V.: A knowledge-based approach of connect-four. J. Int. Comput. Games Assoc. 11(4), 165 (1988)

work page 1988
[3]

Lecture notes, avail- able online, IT University of Copenhagen5 (1997)

Andersen, H.R.: An introduction to binary decision diagrams. Lecture notes, avail- able online, IT University of Copenhagen5 (1997)

work page 1997
[4]

Com- puters, IEEE Transactions on100(8), 677–691 (1986)

Bryant, R.E.: Graph-based algorithms for boolean function manipulation. Com- puters, IEEE Transactions on100(8), 677–691 (1986)

work page 1986
[5]

https://doi.org/10.5281/zenodo

Böck, M.: Connect4 7 x 6 strong solution (2025). https://doi.org/10.5281/zenodo. 14582823, https://doi.org/10.5281/zenodo.14582823

doi:10.5281/zenodo 2025
[6]

In: KI 2008: Advances in Artificial Intelligence: 31st Annual German Conference on AI, KI 2008, Kaiserslautern, Germany, September 23-26, 2008

Edelkamp, S., Kissmann, P.: Symbolic classification of general two-player games. In: KI 2008: Advances in Artificial Intelligence: 31st Annual German Conference on AI, KI 2008, Kaiserslautern, Germany, September 23-26, 2008. Proceedings 31. pp. 185–192. Springer (2008)

work page 2008
[7]

In: Proceedings of the AAAI Conference on Artificial Intelligence

Edelkamp, S., Kissmann, P.: On the complexity of bdds for state space search: A case study in connect four. In: Proceedings of the AAAI Conference on Artificial Intelligence. vol. 25, pp. 18–23 (2011)

work page 2011
[8]

In: Proceedings of the International Conference on Automated Planning and Scheduling

Edelkamp, S., Kissmann, P., Rohte, M.: Symbolic and explicit search hybrid through perfect hash functions—a case study in connect four. In: Proceedings of the International Conference on Automated Planning and Scheduling. vol. 24, pp. 101–110 (2014)

work page 2014

Show all 16 references

[9]

Herzberg, D.: Bitboardc4 (2024), https://github.com/denkspuren/BitboardC4

2024
[10]

In: Proceedings of the International Symposium on Combinato- rial Search

Kissmann, P., Edelkamp, S.: Layer-abstraction for symbolically solving general two-player games. In: Proceedings of the International Symposium on Combinato- rial Search. vol. 1, pp. 63–70 (2010)

2010
[11]

Artificial intelli- gence 6(4), 293–326 (1975)

Knuth, D.E., Moore, R.W.: An analysis of alpha-beta pruning. Artificial intelli- gence 6(4), 293–326 (1975)

1975
[12]

gamesolver.org/

Pons, P.: Solving connect4: How to build a perfect ai (2019), http://blog. gamesolver.org/

2019
[13]

Steininger, C.: c4 (2024), https://github.com/ChristopheSteininger/c4

2024
[14]

UCI Machine Learning Repository (1995), DOI: https://doi.org/10.24432/C59P43

Tromp, J.: Connect-4. UCI Machine Learning Repository (1995), DOI: https://doi.org/10.24432/C59P43

1995 doi
[15]

ICGA Journal31(2), 110–112 (2008)

Tromp, J.: Solving connect-4 on medium board sizes. ICGA Journal31(2), 110–112 (2008)

2008
[16]

html 8 M

Tromp, J.: John’s connect four playground (2015), https://tromp.github.io/c4/c4. html 8 M. Böck Appendix Table 1: Number of positions for severalw × h board configurations with com- putation time, percentage spent garbage collecting, RAM used, and maximum number of BDD nodes a...

2015

Pith tools

Reviewed August 6, 2026 · model on record in the stance chip above.

[1] [1]

Puzzle Wright Press (2010)

Allen, J.D.: The Complete Book of Connect 4: History, Strategy, Puzzles. Puzzle Wright Press (2010)

work page 2010

[2] [2]

Allis, L.V.: A knowledge-based approach of connect-four. J. Int. Comput. Games Assoc. 11(4), 165 (1988)

work page 1988

[3] [3]

Lecture notes, avail- able online, IT University of Copenhagen5 (1997)

Andersen, H.R.: An introduction to binary decision diagrams. Lecture notes, avail- able online, IT University of Copenhagen5 (1997)

work page 1997

[4] [4]

Com- puters, IEEE Transactions on100(8), 677–691 (1986)

Bryant, R.E.: Graph-based algorithms for boolean function manipulation. Com- puters, IEEE Transactions on100(8), 677–691 (1986)

work page 1986

[5] [5]

https://doi.org/10.5281/zenodo

Böck, M.: Connect4 7 x 6 strong solution (2025). https://doi.org/10.5281/zenodo. 14582823, https://doi.org/10.5281/zenodo.14582823

doi:10.5281/zenodo 2025

[6] [6]

In: KI 2008: Advances in Artificial Intelligence: 31st Annual German Conference on AI, KI 2008, Kaiserslautern, Germany, September 23-26, 2008

Edelkamp, S., Kissmann, P.: Symbolic classification of general two-player games. In: KI 2008: Advances in Artificial Intelligence: 31st Annual German Conference on AI, KI 2008, Kaiserslautern, Germany, September 23-26, 2008. Proceedings 31. pp. 185–192. Springer (2008)

work page 2008

[7] [7]

In: Proceedings of the AAAI Conference on Artificial Intelligence

Edelkamp, S., Kissmann, P.: On the complexity of bdds for state space search: A case study in connect four. In: Proceedings of the AAAI Conference on Artificial Intelligence. vol. 25, pp. 18–23 (2011)

work page 2011

[8] [8]

In: Proceedings of the International Conference on Automated Planning and Scheduling

Edelkamp, S., Kissmann, P., Rohte, M.: Symbolic and explicit search hybrid through perfect hash functions—a case study in connect four. In: Proceedings of the International Conference on Automated Planning and Scheduling. vol. 24, pp. 101–110 (2014)

work page 2014