Fun with SAT Solvers, SQL, and the NY Times Crossword.

Solving the NYT Crossword with a SQL Query

 batch last winter, I spent a few days deep-diving and learning about SAT solvers. SAT solvers are a class of tools used to solve Boolean satisfiability problems.

In computer science, the Boolean satisfiability problem (...) is the problem of determining if there exists an interpretation that satisfies a given Boolean formula.

SAT solvers have myriads of fascinating applications. Any problem that can be expressed as a series of true/false conditions can generally be solved by a SAT solver. I decided to apply SAT solvers to one of my favorite types of problems: crossword puzzles. I find that a lot of solving a problem is asking the right question, or modeling a problem in a way that is convenient. So that was the first part of the project - thinking about how to model a crossword puzzle as a series of boolean conditions.

Eventually, I came up with a way to solve the problem:

The list of answers can be thought of as an array. Moving forward, I'll refer to the list of answers as 

 which is a list of N words. We don't know the actual words ahead of time, but we know certain interesting properties about them that will make problem solving easier:

We know how long every word needs to be, so we can encode this knowledge as constraints to make the problem easier to solve. For example:

We also know where words should intersect, and to intersect they must share a letter. For example, if the third letter (index 2) of the first word (W[0]) intersects with the fourth letter (W[3]) of the second word (index 1), we can express this as 

. This reduces the number of possible solutions.

Even if we know the appropriate word lengths and which letters are shared, actually finding the right words can be hard. Since I wanted to make something quick, I decided to skip actually finding the right words, and instead find any set of words that works. Given a sufficiently large dictionary, the solution would be one of the many solutions proposed by the algorithm. There are some really interesting techniques we could use to help find the right word, but I thought of this as a v2 problem. Given this, I relaxed my goal to be to find a set of possible words that fulfills the crossword puzzle topology. One interesting thought is - if you're certain about one or two words on opposite sides of the puzzle, you can probably cull the number of possible solutions by at least an order of magnitude.

We need one more thing to solve this: a list of all the possible words that might show up in the crossword puzzle. I found a simple 

 and ETL'ed it into a database table. I also made two small adjustments to the table:

I indexed every word on every letter, so that the letter matching conditions would run from an index instead of disk seeks. This way, an operation like “find all words that have the letter R in the fourth position” would be as easy as reading off an index.

I also added a second column to the words table to keep track of the word lengths, since they’re constant.

| word    | length  |
|=========|=========|
| car     | 3       |
| boat    | 4       |
| tiger   | 5       |


Armed with this table, I wrote a SQL query to solve a simple puzzle.

SELECT
  w0.word, w1.word, w2.word, w3.word
FROM
  words w0
    inner join words w1 on (1 = 1)
    inner join words w2 on (1 = 1)
    inner join words w3 on ((substring(w1.word from 1 for 1) = substring(w3.word from 2 for 1))
    and (substring(w0.word from 1 for 1) = substring(w3.word from 1 for 1))
    and (substring(w2.word from 1 for 1) = substring(w3.word from 3 for 1)) )
WHERE
  w0.length = 3 
  and w1.length = 3 
  and w2.length = 3 
  and w3.length = 3
LIMIT 10

Working through this query by its main parts:

SELECT w0.word, w1.word, w2.word, w3.word

: we're solving a four-word crossword puzzle, so we have to reference four copies of the words table. Remember, there are two columns in the table: word and length.

FROM words w0 inner join words w1 on (1 = 1) inner join words w2 on (1 = 1) inner join words w3 on ((substring(w1.word from 1 for 1) = substring(w3.word from 2 for 1))...

: This tells the database how to join the table on itself. Words that do not overlap with each other are joined on an arbitrary condition 

, while words that overlap are joined on a boolean condition (like joining 

). This reduces the number of possible solutions that the database has to check, which in turn makes the problem easier for the database to solve.

: We know how long each word should be, so we can ignore words that are of the wrong length. This also culls the solution set by a lot.

: there are a lot of possible solutions, so only show the first 10.

Bear in mind, this query gets complex very quickly: if you’re solving a three word crossword puzzle, you’re joining a table on itself 3 times (so 10^3 comparisons). With a four-word crossword, 10^4. Generally, if the dictionary has X words and the crossword has N questions, it’s solvable in O(2^N) complexity which gets complex very quickly. This is a video about complexity: 

P vs. NP and the Computational Complexity Zoo

This query takes a few seconds to run, but you get a result that ultimately works!

word0 | word1 | word2 | word3
------+-------+-------+-------
car   | use   | tar   | cut
car   | usa   | tar   | cut
car   | url   | tar   | cut
car   | usr   | tar   | cut
car   | usb   | tar   | cut
car   | ups   | tar   | cut
car   | usd   | tar   | cut
car   | utc   | tar   | cut
car   | und   | tar   | cut
car   | urw   | tar   | cut

I went a lot deeper into this problem - actually going as far as writing tools that convert a crossword puzzle (in PUZ format using 

 ) into a long SQL query. At the moment the caveat about complexity holds true: this technique can't solve puzzles that have more than 8 words (on a powerful machine on EC2), but I have some ideas on how to make the solver scale and solve puzzles that are at least as hard as the ones that appear in the daily papers.

Let me know if you’re interested in collaborating with me on this by messaging me on Twitter: 

. This might be a problem that's already solved in research, but there's undeniably a lot of joy in solving problems that stretch the limits of what we previously thought were not possible.