> It's also fascinating to me that the author attempted to train an ML model to play the game. My initial thought was that an exhaustive search was the only way to approach this (because it's perhaps the only way to arrive at a max score that is provably correct), but I think I am not truly appreciating the vastness of the search space at play here, and exhaustively searching all possible inputs might just be too unimaginably large.
I think when we did the math with our best emulator it would take 100 billion years? There are, by our estimation or a game lasting a thousand moves 10^23 possible wells. With current computing, even if we threw all the resources of the planet at it, we'd still be a few orders of magnitude short of finishing in our lifetimes. It is a very very very large search space.
>Searching for duplicate states and culling any branches that are equivalent.
Branch pruning and comparison are both expensive relatively speaking. You want, in a perfect world, to essentially have a hashmap lookup for duplicate nodes, so deciding if its new or not is O(1), rather than having to look at your node and all its children to know if it's duplicated. It doesn't matter unless you're really chasing performance.
Also this was our first serious rust project so implementing it was a bit more daunting than expected. In a sane codebase it's probably not a bad refactor, at the point we did it we had six methods with a bunch of stuff jammed into them and names like `explore_tree` so it was a challenge, made significantly easier by rust types, and more frustrating by the borrow checker.
Long answer: I actually discussed it with Tim once, long after part 2 of our blog post and after the whole thing settled down. Tim was making an SAT solver based on a post about a homemade Sudoku program that got out of hand (https://t-dillon.github.io/tdoku/), and HATETRIS has a binary grid representation, so it's a logical thing to attempt. So, how would you answer the question of the longest possible game with SAT? The idea would be that you can start with a set of wells S_0, generate a new set S_1, and continue generating sets of all possible wells until you find some N for which S_N is not satisfiable; N-1 is therefore the longest game.
Suppose S_0 consists of the starting well, W_0. W_0 is a conjunction of 160 different clauses, each of which is initially set to 'not':
W_0 = !x_0_0 && !x_0_1 && ... && !x_15_9
Once you have that, you need some way of getting from W_0 to its possible descendants. There are 2457 possible piece positions in a standard 16x10 HATETRIS well, each of which interacts with at most four squares (fewer for the piece positions within the top four lines), and each of which can be reached at most four ways (from another piece moving down, moving right, moving left, or rotating). This puts a rough estimate of ~39,000 clauses needed for a function which converts W_0 into its children: W_0 -> W_1a || W_1b || W_1c || ... = S_1. Which isn't too bad, as far as SAT solvers go.
The problem is that this is very similar to what our first version of the emulator did and that version was a hundred times slower than our current version. SAT is NP-complete in the worst case, and without some huge simplification from putting it in Boolean form, it didn't seem likely to be worth the additional cost.
I think there's still a possibility for some kind of solver to aid searches, e.g. "Given this specific well, you need to clear lines 5 and 6 in order to clear line 4, and you need to clear lines 7, 8, and 9 in order to clear line 6...", and I think certain properties (such as the minimum number of pieces needed to clear a given line) are computable with SAT, maybe even to the point of making a a pruned-but-provably-optimal game tree search feasible.
Putting the raw emulator in SAT form is natural. Putting constraints like these in SAT form requires coming up with a new level of abstraction ourselves. Our only attempt at it was in the Mumble Mumble Graph Theory section; what we learned is that making a new level of abstraction is a lot harder, and we don't know how to do it.
But I mean, what happens if you just chuck those 39,000 clauses into Z3 and let it spin to see what happens? Solvers use a bunch of cute backtracking heuristics to not explore too much of the state space, and they keep getting better at it. Particularly, SAT is sort of like the halting problem, with a class of easily identifiable satisfiable instances and a class of easily identifiable unsatisfiable ones. The difficult instances are a narrow band between the other two classes. SAT solvers are so successful because so many naturally occurring instances turn out to be easy.
I think one of the general takeaways about ML is that barring a few experts, its really challenging to reason about your system. Like, yes, you might expect that a convolutional layer will behave in a specific way under ideal conditions, but the way that behavior manifests is often wildly hard to predict during the early days.
I agree that step 1 for most beginner projects should be to start with something that works and then tweak.
