{"id":"481713ce-fd4c-4a08-927b-950d739c6ca4","arxiv_id":"2507.05267","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A compressed BDD encoding makes a full 42-ply win-draw-loss lookup table for 7x6 Connect-Four practical, confirming the first player wins.","lead":"This paper builds an 89.6 GB lookup table that gives the win, loss, or draw outcome for every legal 7 by 6 Connect-Four position, using 47 hours on a single desktop CPU core. It matters because a complete strong solution for this game was previously thought too large to build, and the new encoding technique may carry over to other search problems.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The 89.6 GB table's win/draw/loss labels are never independently validated; per-ply count checks cannot detect a misclassification bug in the custom BDD retrograde implementation.","rationale":"The reader's weakest assumption points to the unproved compressed encoding and the unverified BDD library. I agree that the library correctness is load-bearing, but I would de-emphasize the encoding: the reproduced position counts, summing exactly to Tromp's 4,531,985,219,092 total, are strong evidence that the forward enumeration produces exactly the legal positions and no ghost states. The untested part is the retrograde classification. The reported internal consistencies—per-ply totals, terminal parity, and the 6x6 reproduction—are necessary but not sufficient, because a classification bug could preserve counts. The most direct way to settle the concern is an independent solver comparison on a sample of stored positions; if that passes, the central claim is supported. The reader's CONDITIONAL verdict already reflects this gap, so my read does not move the verdict; it sharpens the condition to an explicit independent label check rather than a proof of encoding injectivity.","tokens_in":10539,"tokens_out":19072,"duration_ms":219354,"concrete_test":"Use Tromp's or Steininger's independent Connect-Four solver to evaluate all 184,275 8-ply positions, where an independent published database already exists, plus a random sample of 10,000 positions per ply drawn from the stored table, and compare each returned win/draw/loss label with the 89.6 GB artifact. Any mismatch would falsify the strong-solution claim; a clean pass would resolve the concern. As an additional sanity check, recompute the row-42 full-board total by counting all full 7x6 columns with 21 discs of each color and confirm it equals 1,459,332,899.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim is that the 89.6 GB artifact contains a correct complete win/draw/loss classification of all 4,531,985,219,092 positions of 7x6 Connect-Four. The evidence offered for correctness is (i) per-ply won/drawn/lost counts summing to Tromp's known position totals, (ii) terminal-count parity, and (iii) reproduction of the 6x6 solution. These checks confirm the forward state enumeration and largely mitigate the injectivity worry about the compressed encoding, since ghost states would inflate the total count. However, they do not constrain the retrograde labels: a bug in the pre-image/complement/negation logic, in the mirrored transition relation, or in the manual reference-counting garbage collector could systematically misclassify positions while preserving the counts. No independent solver is used to cross-check any stored outcome, and the paper offers no verification script or checksum for the table. Thus the strong-solution claim rests entirely on the correctness of an unverified hand-written C BDD library at scales (1.1 billion nodes, 128 GB) far beyond the 6x6 reproduction.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":10707,"tokens_out":6313,"duration_ms":74017,"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":[{"comment":"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.","section":"§4.2, Appendix Table 2"},{"comment":"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.","section":"§3.1"},{"comment":"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.","section":"§3.2"}],"minor_comments":[{"comment":"The phrase \"alá alpha-beta pruning\" should be \"à la alpha-beta pruning\", and \"trades of memory\" should be \"trades off memory\".","section":"§1"},{"comment":"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.","section":"§2.2"},{"comment":"\"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.","section":"§3.1"},{"comment":"\"ply 27 takes the most storage to store\" is awkward; consider \"ply 27 requires the most storage\".","section":"§4.2"},{"comment":"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.","section":"References"}],"recommendation":"major_revision","confidential_remarks":"The paper is an engineering contribution whose central claim rests on the correctness of a large generated artifact. The proposed revisions—independent label checks, a formal encoding argument, and BDD-library tests—are necessary before the strong-solution claim can be accepted. The citation pattern and novelty disclosure are appropriate, and the open-source release is a strength."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","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.\n\nWhat 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.\n\nThe 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.\n\nI 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.\n\nWho 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.","headline":"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.","tokens_in":11275,"tokens_out":1273,"would_cite":true,"duration_ms":19660,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"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.","keywords":["Connect-Four","strong solution","lookup table","binary decision diagrams","symbolic search","retrograde analysis","game solving","combinatorial games"],"falsifier":"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.","tokens_in":10244,"feed_emoji":"🎮","tokens_out":6856,"duration_ms":66238,"temperature":0.7,"pith_summary":"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.","feed_headline":"Complete Connect-Four outcome table built in 47 hours on one core","feed_subtitle":"A 89.6 GB lookup table gives the win/draw/loss verdict for every legal 7x6 board, once believed infeasible.","key_machinery":"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}$.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Supplies the BDD symbolic search method and the exponential-complexity result that motivates the new compressed encoding.","marker":"[7]"},{"why":"Gives the layered forward pass and retrograde analysis approach that the paper reimplements for Connect-Four.","marker":"[10]"},{"why":"The previous attempt at the 7 × 6 board, whose partial solution the paper's table agrees with and whose 93-day estimate is the baseline to beat.","marker":"[8]"},{"why":"Source of the unique position counts the paper reproduces and extends for other board sizes.","marker":"[16]"},{"why":"Establishes the BDD data structure and Boolean operations that form the foundation of the entire computation.","marker":"[4]"},{"why":"The published 7 × 6 strong solution dataset itself, enabling reproducibility and independent checks of the table.","marker":"[5]"},{"why":"The earlier 8-ply database that strongly solved the game via search, serving as the predecessor against which the 'first look-up-table-like solution' claim is positioned.","marker":"[14]"}],"fun_headline_variants":["Complete Connect-Four outcome table in 47 hours on one core","89.6 GB lookup table solves 7x6 Connect-Four","Previously infeasible: full Connect-Four table built in 47h","Consumer hardware yields full Connect-Four solution in 47 hours","One CPU, 47h: all 7x6 Connect-Four positions evaluated"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Complete Connect-Four outcome table in 47 hours on one core","89.6 GB lookup table solves 7x6 Connect-Four","Previously infeasible: full Connect-Four table built in 47h","Consumer hardware yields full Connect-Four solution in 47 hours","One CPU, 47h: all 7x6 Connect-Four positions evaluated"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000634,"raw_usage":{"total_tokens":2896,"prompt_tokens":884,"completion_tokens":2012,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":500,"completion_tokens_details":{"reasoning_tokens":1920}},"tokens_in":500,"tokens_out":2012,"duration_ms":16900,"temperature":1.0,"reasoning_tokens":1920,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-06T21:11:15.737030+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":"In: Proceedings of the AAAI Conference on Artificial Intelligence","cited_arxiv_id":null,"evidence_quote":"Supplies the BDD symbolic search method and the exponential-complexity result that motivates the new compressed encoding."},{"cited_title":"In: Proceedings of the International Symposium on Combinato- rial Search","cited_arxiv_id":null,"evidence_quote":"Gives the layered forward pass and retrograde analysis approach that the paper reimplements for Connect-Four."},{"cited_title":"In: Proceedings of the International Conference on Automated Planning and Scheduling","cited_arxiv_id":null,"evidence_quote":"The previous attempt at the 7 × 6 board, whose partial solution the paper's table agrees with and whose 93-day estimate is the baseline to beat."},{"cited_title":"html 8 M","cited_arxiv_id":null,"evidence_quote":"Source of the unique position counts the paper reproduces and extends for other board sizes."},{"cited_title":"Com- puters, IEEE Transactions on100(8), 677–691 (1986)","cited_arxiv_id":null,"evidence_quote":"Establishes the BDD data structure and Boolean operations that form the foundation of the entire computation."}],"review_version":1}