There is a neural network running on this page which solves Skyscrapers puzzles, a type of Latin square puzzle which you can learn about and solve in another post. The network, a 15.5-million parameter decoder-only language model over a 454-token vocabulary, was trained to write out step-by-step solutions including guesses and retractions with a success rate of about 99%.
Producing the neural network that runs above gave me an opportunity to dabble in a few ideas standardly used to tackle constraint satisfaction problems. Below I outline some of the thought process that went into the model.
1. Systematic solutions
One way to think about the solution process is in terms of positive possibilities: what numbers, based on our deductions so far, could possibly be placed in each cell? So we start by penciling in the numbers 1-6 in each cell and then erase them as we arrive at eliminations. A standard way to think about these possibilities is generalized arc consistency (GAC; "generalized" here from binary to 6-ary constraints): a value in a particular cell is GAC-supported just if there is some way to assign values to the other cells involved in the constraint such that the constraint is satisfied, and we have eliminated our way down to generalized arc consistency when all values left in all cells in the scope of the constraint are GAC-supported. This naturally splits out into row constraints and column constraints.
Applying GAC means looking at each number we have penciled into a given cell and checking whether there are still any not-yet-eliminated numbers we can assign to the other cells in the row or column that satisfy the constraints of the Skyscrapers puzzle (each row or column must contain all of the numbers 1-6 and the order of those numbers must respect the clues, if any, on that row or column). If there is no way to make the number work, we erase that pencil mark and move on. If we keep checking row and column constraints for every remaining assignment of every cell, we eventually reach a fixed point where further checks yield no new eliminations. If this happens right when the puzzle is solved, great! But if not, we need another step.
Shaving is the process of guess-and-check: hypothetically assign a particular value to a particular cell, then repeat all of the GAC checks under that assumption. If in doing so we end up erasing all of the possibilities from any cell, we have refuted that hypothesis and can rewind everything back to the moment we made that assumption and erase it ("shave" it) as a possibility. Consistency under a single hypothetical assignment is called singleton arc consistency (SAC).
These processes are structurally similar to how you yourself will have thought about these puzzles if you have solved them: the GAC algorithm is similar to the way you will have iteratively incorporated information about the constraints and the evolving state of the grid to narrow down to the only possible value for each cell, and the SAC algorithm has the same branching guess-and-check pattern as the process you will have used when GAC-like iterations gave out. Most of the Skyscrapers puzzles I have sampled could not be solved by GAC iterations alone, so this branching structure is an expected feature of the solution.
2. The dual perspective
The approach above is framed positively, in terms of the remaining penciled-in numbers. But we will be able to express facts about the solution more easily if we instead use the negative framing, in terms of the absence set of values that have already been eliminated. The GAC algorithm adds a number to the absence set of a cell when it can find no assignment of numbers to that cell's row or column that places that number in that cell and satisfies the constraints. When the search for such an assignment fails, there will be some (possibly empty) set of absences across the row or column that rules out every such assignment. The minimal such sets — minimal hitting sets or minimal unsatisfiable cores depending on how one looks at them — are each irreducible reasons why the GAC algorithm must eliminate the number under consideration. If we eliminate value v from cell i, and find a minimal set H of (cell, value) absences that explain it, we can write a rule explaining the elimination as follows:
/\h in H absent(h) ==> absent(i,v).
This is a Horn clause in implication form, and repeatedly deriving eliminations using these Horn clauses gets us to the same fixed point as repeated applications of GAC; assuming a value and then repeatedly deriving eliminations achieves the same result as SAC. But doing so gives us a natural way to explain each step of the derivation: we add v to the absence set of cell i because a specific list of absences in its row or column implies the elimination according to one particular Horn clause. Note that the Horn clause does not mention clues; those become indices by which relevant clauses are selected from the full 62,963-clause library.
3. Motivations
Before I settled on training a language model to emit step-by-step solutions, I trained a number of other models. In some I simply installed the right mechanics to solve the puzzles, but that was unsatisfying since dressing up a solution algorithm in neural network trappings is just a refactor. Other models (such as ones using message passing on graphs with and without a sheaf structure) which attempted to learn the solution process all plateaued at about a 90% solve rate. In each of those cases, the failures looked the same: most botched solutions involved puzzles that required a branching guess-and-check process, and that process proved difficult to train. And so in each of those cases, the most natural route forward with the plateaued model would have been to augment the model with branching behavior orchestrated from outside the model.
But I did not find that approach satisfying for two reasons: I had already implemented search breadth orchestration in the Equilibrium Reasoners post, and a model which can handle a branching search for the solution entirely on its own is the more interesting artifact. I had seen two papers from 2024 that trained transformers to emit tokenized search processes, including searching for solutions to puzzles, so I expected such an approach to work in my case. And since such a model would handle all of the branching itself in a serialized way without relying on external orchestration, it would meet my design requirement.
4. Making the model
I gave the model a vocabulary consisting of 7 clue tokens (clue 0 represents an empty clue slot), 6 tokens for writing out its final answer, 216 tokens for eliminations and 216 for guesses, and 9 structural tokens: 2 to mark the beginning and end of the sequence, 1 padding token used to make everything line up neatly but never emitted by the model, 1 token to mark the beginning of the final answer readout, and then the following 5 tokens which shape the solution.
- ROUND, a round delimiter token which separates rounds of eliminations on the way to a fixed point. One round consists of iterating the elimination algorithm over each row and each column. I adopted the simplifying convention that eliminations do not update the grid state until the end of the round. This does not change the solver's fixed point but it does make eliminations within a round independent of the order in which the elimination algorithm iterates over rows and columns. In the training data, eliminations within a round are ordered lexicographically by row index, column index, and value.
- GUESS, a guess marker token that precedes each guess. Guesses already use distinct tokens, but this gives the model a way to emit a structural fact: "now it is time to guess a value somewhere." This also makes the model's solution easier to read.
- CONTRA, a contradiction marker token that immediately follows a round that eliminated every possible value from at least one cell.
- BACK, a rewind token that retracts a guess that led to a contradiction.
- RESTART, a restart token that discards the entire solution sequence when an error has led to a contradiction not dependent on a guess.
The idea is to never directly teach the model state management. Instead, it receives a prompt consisting of the beginning of sequence token followed by tokens for each clue in a fixed order, and during training it is taught solution sequences. The model must learn how to use the order of the clues and how to produce correct solution sequences from them.
At first the solve rate climbed with more training puzzles and more training epochs. After that, bootstrapped fine-tuning and DAgger fine-tuning lifted the solve rate to 95.7% before further rounds began to just change which puzzles were solved correctly. The next step was to, by varying the choice of branch point, augment the number of solution sequences per puzzle in the training data rather than the number of puzzles. After those gains tapered off I added the RESTART token to the vocabulary for the first time, and the resulting model finally achieved a solve rate of 99%. A few more adjustments got the model to solve a few more puzzles, but did not meaningfully close the gap to 100%.
5. Explaining the solution
I said above that using Horn clauses to write the solution gave us a natural way to explain the validity of each valid elimination in the solution sequence. The model does (rarely) make invalid eliminations, and its learned behavior is not exactly the Horn calculus. In a small sample of eliminations I used for an attribution analysis, I found that the model used a single Horn clause to derive about a quarter of the eliminations, any of several Horn clauses to derive another quarter, and sets of absence premises that are not minimal to derive another third or so.
If you select any of the eliminations in the solution sequence generated above, you can see a Horn calculus justification for the elimination if one exists. This is not in general identical to the model's mechanics; it simply explains instances of the logic the model is mostly implementing. Click elsewhere or hit Escape to deselect the elimination.