[TheCog]

From Dave:

Short answer: SAT solvers are hard.

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.

[throwaway81523]

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.