10 ms·

Solving Wordle with Z3

82 points by zdw 5y ago

GoodJokes 5y ago
throwaway81523 5y ago
This was a fun read, and it's cool that using z3 like that works at all, but the takeaway for me is that a SAT solver isn't that great a way to solve wordles. Using some basic probability and scanning the word list for max-entropy guesses seems like a more natural match to the problem. If you want to encapsulate the searching in an external library, sqlite3 might be a good choice from Python. Sqlite3's Python bindings let you connect Python functions to your sqlite3 instance, so you can call them from SQL. So you'd write Python functions for "matched letter in the right place", "matched letter in the wrong place", and "no match for that letter". Then all your searches would be simple SQL queries.
- toppy 5y ago
  Don't get me wrong but what's your idea about representing 'matched letter in wrong place' in SQL instead of string indexing in Python for instance?
  - jeremysalwen 5y ago
    > Python bindings let you connect Python functions to your sqlite3 instance, so you can call them from SQL I think the idea is calling python functions from SQL to check 'matched letter in wrong place'.
  - notafraudster 5y ago
    I treated yellow squares as two sequential rules: (1) regex with [A-Z] character classes less the characters you know are not in the exact spots -- this certifies you've eliminated the characters that shouldn't be there. These can be directly encoded into a single SQL query; (2) a series of in operators to check that the character is there at all. In SQL this could be `word LIKE '%S%'` after the initial (1) rule.
- hiyer 5y ago
  > the takeaway for me is that a SAT solver isn't that great a way to solve wordles. It may not be the best way, but it seems to lead to very clean, compact and understandable code. I have no background with Z3 (or any SAT solver for that matter) but I didn't have much trouble following the author's approach.
grenoire 5y ago
A little tip, you don't really have to generate the 5-letter word list, as Wordle's client-side script already does this validation over a known list of around 2200~ words. It's unobfuscated, you should be able to pick it up easily.
- ghusbands 5y ago
  WARNING: Do not do this if you care to try the puzzle in future. All of the past and future target words are listed in sequence in the source. (I only got spoiled for tomorrow before I noticed.)
  - caitlinface 5y ago
    This gave me an idea for a fun experiment... Take the future word list, and each day use tomorrow's word as much as can be naturally fit into normal conversation. Then see if all of my friends start to score better, since they were primed. (I am too protective of spoilers to actually do this, but still.)
  - grenoire 5y ago
    In order!? Oh man, I was just planning on reverse-engineering the network connection, it seems like there's none!
aaronsdevera 5y ago
or, you know, you could just paste this into the javascript console. JSON.parse(window.localStorage.getItem("gameState")).solution
dejawu 5y ago
We can do a lot better than random on our first guess, though. Playing the game as a human, I found that it helped to eliminate (or confirm the presence of) vowels and common consonants ASAP. A quick search for five-letter words with three distinct vowels (can't get more than that without straying beyond common English) and the most common consonants (R, S, T) yields words like "autos", "raise", and "suite", which I've anecdotally found to make for great starting words.
- thom 5y ago
  I generally start with TEARS, INDOL and CHUMP, which seemed to match the 15 most common letters in the right order in the word list I had available at the time.
- sgk284 5y ago
  ADIEU seems to be a popular four vowel choice. Seems to work pretty well in practice.
- bryans 5y ago
  I almost feel like packing the first word with vowels isn't even particularly helpful. I've kept with the same two starting words -- slate and round -- and it has been very easy to guess by the third turn every day. In fact, the only day it took more (5) is when I strayed from using round as the second word. If nothing from those two words hits, the remaining letters leave only very obvious words using I and/or Y. There really aren't that many 5-letter words, so there's going to be a few specific combinations of two starting words that rapidly whittle the list.
  - dfan 5y ago
    You might enjoy the extra challenge of hard mode (access it through the gear icon), where every guess you make has to be a potential solution based on the existing history.
    - IanCal 5y ago
      Something it doesn't stop is reusing eliminated letters, which adds a little more to it. You can do that yourself though.
andopp 5y ago
Cool! I made a solver myself, yesterday. For every move, it ranks each legal word based on how much information that word will gain. It figures this out by trying all possible solutions that are still compatible with the information acquired so far. The word that gives the biggest reduction (worst case) in size of candidate solution pool, is the chosen word. For yesterday's word, it yielded the following sequence of guesses: AESIR, DROPT, ABCEE, QUERY! Most useful for us humans is that AESIR seems to be the best starting word. Here is my java source code for this solver: https://pastebin.com/k1tTCyUR https://pastebin.com/k1tTCyUR A bit obfuscated by some necessary optimziations.
- ghusbands 5y ago
  "Aesir" wouldn't be an accepted word in most word games, being a proper noun (capitalised). But "raise" uses the same letters, though obviously reveals differently positional info.
  - notafraudster 5y ago
    ARISE and SERAI also have the same letters and different positional info. In the dictionary I used, SERAI was the optimal 5 letter word to start with.
  - andopp 5y ago
    When I tried with the /usr/share/dict/words dictionary it guessed "raise" first, so I can confirm it's a great way to start the game.
- thom 5y ago
  These guesses seem counterintuitive in that they waste letters by repeating previous guesses. Interesting if this is optimal though.
  - ghusbands 5y ago
    Reducing the possible position of letters can drastically reduce the set of possible words; but intuition probably tends towards getting more information about the presence or lack rather than the position of letters. I don't think anyone has released an 'optimal' player, yet. I imagine getting all target words (in the wordle dictionary) in four guesses is doable and three is probably not.
pil0u 5y ago
In France, there is a TV show called Motus which is basically the same as Wordle but with 8-letter words (https://fr.wikipedia.org/wiki/Motus_(jeu_t%C3%A9l%C3%A9vis%C3%A9) https://fr.wikipedia.org/wiki/Motus_(jeu_t%C3%A9l%C3%A9vis%C...) Two young CS researchers took part in the competition after building their home-made algorithm (I suppose based on tree search) to find optimal words to search for, given the constraints. They learnt these optimal words/paths by heart before the show. They never lost a game. Opponents scores were embarrassingly low, they actually broke the game. It was also very funny to watch because they spelled words that most people didn't know they exist. I'll edit if I can find a video link (which is surprisingly struggling).
- desdiv 5y ago
  >It was also very funny to watch because they spelled words that most people didn't know they exist. This kinda reminds me of the New Zealand Scrabble player who won multiple French World Scrabble Championships despite not speaking French. He just memorized the French Scrabble dictionary. [1] https://en.wikipedia.org/wiki/Nigel_Richards_(Scrabble_player) https://en.wikipedia.org/wiki/Nigel_Richards_(Scrabble_playe...
- a_imho 5y ago
  In Hungary we have this table top game, iiuc this has the same mechanics just with colors. It was (maybe still is) popular in primary school aged 8-12. https://okosjatek.cdn.shoprenter.hu/custom/okosjatek/image/data/product/Retro%20j%C3%A1t%C3%A9kok/retro_mesterlogika_kek_550_550.jpg?lastmod=1631023233.1639238329 https://okosjatek.cdn.shoprenter.hu/custom/okosjatek/image/d...
  - jhgb 5y ago
    Basically Mastermind. We had Logik instead: https://cs.wikipedia.org/wiki/Logik_(hra) https://cs.wikipedia.org/wiki/Logik_(hra) But in Mastermind, you for example aren't told which pins are in correct positions, whereas in Wordle you are told that.
  - croon 5y ago
    Yes, it's called Mastermind [0]. Just fewer colors than letters. [0] https://en.wikipedia.org/wiki/Mastermind_(board_game) https://en.wikipedia.org/wiki/Mastermind_(board_game)
RobertoG 5y ago
I would appreciate recommendations for learning about SMT solvers. A good book, for instance?
- ahelwer 5y ago
  Programming Z3 https://theory.stanford.edu/~nikolaj/programmingz3.html https://theory.stanford.edu/~nikolaj/programmingz3.html
- fallingmeat 5y ago
  Another "popular" option is Yices: https://yices.csl.sri.com https://yices.csl.sri.com
bfung 5y ago
Tangent: for people on the job interview circuit, wordle is basically a modified on hangman game. It's worth coding an algorithm here here in case you're asked to do a take home hangman code up!
zvrba 5y ago
So someone "reinvented" mastermind with letters instead of colors.
Imnimo 5y ago
It would be interesting to see if you could solve the puzzle by looking at the grids people post on Twitter. Each grid shows you the colors they got from the guesses, but not the letters. For a particular grid to be possible, there must be a sequence of valid words that produce that grid given the day's answer. If you have hundreds of peoples' grids for the day, is that sufficient to narrow down the space of possible words to 1?

82 points by zdw 5y ago

This was a fun read, and it's cool that using z3 like that works at all, but the takeaway for me is that a SAT solver isn't that great a way to solve wordles. Using some basic probability and scanning the word list for max-entropy guesses seems like a more natural match to the problem. If you want to encapsulate the searching in an external library, sqlite3 might be a good choice from Python. Sqlite3's Python bindings let you connect Python functions to your sqlite3 instance, so you can call them from SQL. So you'd write Python functions for "matched letter in the right place", "matched letter in the wrong place", and "no match for that letter". Then all your searches would be simple SQL queries.

toppy 5y ago
Don't get me wrong but what's your idea about representing 'matched letter in wrong place' in SQL instead of string indexing in Python for instance?
- jeremysalwen 5y ago
  > Python bindings let you connect Python functions to your sqlite3 instance, so you can call them from SQL I think the idea is calling python functions from SQL to check 'matched letter in wrong place'.
- notafraudster 5y ago
  I treated yellow squares as two sequential rules: (1) regex with [A-Z] character classes less the characters you know are not in the exact spots -- this certifies you've eliminated the characters that shouldn't be there. These can be directly encoded into a single SQL query; (2) a series of in operators to check that the character is there at all. In SQL this could be `word LIKE '%S%'` after the initial (1) rule.
hiyer 5y ago
> the takeaway for me is that a SAT solver isn't that great a way to solve wordles. It may not be the best way, but it seems to lead to very clean, compact and understandable code. I have no background with Z3 (or any SAT solver for that matter) but I didn't have much trouble following the author's approach.

grenoire 5y ago

A little tip, you don't really have to generate the 5-letter word list, as Wordle's client-side script already does this validation over a known list of around 2200~ words. It's unobfuscated, you should be able to pick it up easily.

ghusbands 5y ago
WARNING: Do not do this if you care to try the puzzle in future. All of the past and future target words are listed in sequence in the source. (I only got spoiled for tomorrow before I noticed.)
- caitlinface 5y ago
  This gave me an idea for a fun experiment... Take the future word list, and each day use tomorrow's word as much as can be naturally fit into normal conversation. Then see if all of my friends start to score better, since they were primed. (I am too protective of spoilers to actually do this, but still.)
- grenoire 5y ago
  In order!? Oh man, I was just planning on reverse-engineering the network connection, it seems like there's none!

aaronsdevera 5y ago

or, you know, you could just paste this into the javascript console. JSON.parse(window.localStorage.getItem("gameState")).solution

dejawu 5y ago

We can do a lot better than random on our first guess, though. Playing the game as a human, I found that it helped to eliminate (or confirm the presence of) vowels and common consonants ASAP. A quick search for five-letter words with three distinct vowels (can't get more than that without straying beyond common English) and the most common consonants (R, S, T) yields words like "autos", "raise", and "suite", which I've anecdotally found to make for great starting words.

thom 5y ago
I generally start with TEARS, INDOL and CHUMP, which seemed to match the 15 most common letters in the right order in the word list I had available at the time.
sgk284 5y ago
ADIEU seems to be a popular four vowel choice. Seems to work pretty well in practice.
bryans 5y ago
I almost feel like packing the first word with vowels isn't even particularly helpful. I've kept with the same two starting words -- slate and round -- and it has been very easy to guess by the third turn every day. In fact, the only day it took more (5) is when I strayed from using round as the second word. If nothing from those two words hits, the remaining letters leave only very obvious words using I and/or Y. There really aren't that many 5-letter words, so there's going to be a few specific combinations of two starting words that rapidly whittle the list.
- dfan 5y ago
  You might enjoy the extra challenge of hard mode (access it through the gear icon), where every guess you make has to be a potential solution based on the existing history.
  - IanCal 5y ago
    Something it doesn't stop is reusing eliminated letters, which adds a little more to it. You can do that yourself though.

andopp 5y ago

Cool! I made a solver myself, yesterday. For every move, it ranks each legal word based on how much information that word will gain. It figures this out by trying all possible solutions that are still compatible with the information acquired so far. The word that gives the biggest reduction (worst case) in size of candidate solution pool, is the chosen word. For yesterday's word, it yielded the following sequence of guesses: AESIR, DROPT, ABCEE, QUERY! Most useful for us humans is that AESIR seems to be the best starting word. Here is my java source code for this solver: https://pastebin.com/k1tTCyUR https://pastebin.com/k1tTCyUR A bit obfuscated by some necessary optimziations.

ghusbands 5y ago
"Aesir" wouldn't be an accepted word in most word games, being a proper noun (capitalised). But "raise" uses the same letters, though obviously reveals differently positional info.
- notafraudster 5y ago
  ARISE and SERAI also have the same letters and different positional info. In the dictionary I used, SERAI was the optimal 5 letter word to start with.
- andopp 5y ago
  When I tried with the /usr/share/dict/words dictionary it guessed "raise" first, so I can confirm it's a great way to start the game.
thom 5y ago
These guesses seem counterintuitive in that they waste letters by repeating previous guesses. Interesting if this is optimal though.
- ghusbands 5y ago
  Reducing the possible position of letters can drastically reduce the set of possible words; but intuition probably tends towards getting more information about the presence or lack rather than the position of letters. I don't think anyone has released an 'optimal' player, yet. I imagine getting all target words (in the wordle dictionary) in four guesses is doable and three is probably not.

pil0u 5y ago

In France, there is a TV show called Motus which is basically the same as Wordle but with 8-letter words (https://fr.wikipedia.org/wiki/Motus_(jeu_t%C3%A9l%C3%A9vis%C3%A9) https://fr.wikipedia.org/wiki/Motus_(jeu_t%C3%A9l%C3%A9vis%C...) Two young CS researchers took part in the competition after building their home-made algorithm (I suppose based on tree search) to find optimal words to search for, given the constraints. They learnt these optimal words/paths by heart before the show. They never lost a game. Opponents scores were embarrassingly low, they actually broke the game. It was also very funny to watch because they spelled words that most people didn't know they exist. I'll edit if I can find a video link (which is surprisingly struggling).

desdiv 5y ago
>It was also very funny to watch because they spelled words that most people didn't know they exist. This kinda reminds me of the New Zealand Scrabble player who won multiple French World Scrabble Championships despite not speaking French. He just memorized the French Scrabble dictionary. [1] https://en.wikipedia.org/wiki/Nigel_Richards_(Scrabble_player) https://en.wikipedia.org/wiki/Nigel_Richards_(Scrabble_playe...
a_imho 5y ago
In Hungary we have this table top game, iiuc this has the same mechanics just with colors. It was (maybe still is) popular in primary school aged 8-12. https://okosjatek.cdn.shoprenter.hu/custom/okosjatek/image/data/product/Retro%20j%C3%A1t%C3%A9kok/retro_mesterlogika_kek_550_550.jpg?lastmod=1631023233.1639238329 https://okosjatek.cdn.shoprenter.hu/custom/okosjatek/image/d...
- jhgb 5y ago
  Basically Mastermind. We had Logik instead: https://cs.wikipedia.org/wiki/Logik_(hra) https://cs.wikipedia.org/wiki/Logik_(hra) But in Mastermind, you for example aren't told which pins are in correct positions, whereas in Wordle you are told that.
- croon 5y ago
  Yes, it's called Mastermind [0]. Just fewer colors than letters. [0] https://en.wikipedia.org/wiki/Mastermind_(board_game) https://en.wikipedia.org/wiki/Mastermind_(board_game)

RobertoG 5y ago

I would appreciate recommendations for learning about SMT solvers. A good book, for instance?

ahelwer 5y ago
Programming Z3 https://theory.stanford.edu/~nikolaj/programmingz3.html https://theory.stanford.edu/~nikolaj/programmingz3.html
fallingmeat 5y ago
Another "popular" option is Yices: https://yices.csl.sri.com https://yices.csl.sri.com

bfung 5y ago

Tangent: for people on the job interview circuit, wordle is basically a modified on hangman game. It's worth coding an algorithm here here in case you're asked to do a take home hangman code up!

zvrba 5y ago

So someone "reinvented" mastermind with letters instead of colors.

Imnimo 5y ago

It would be interesting to see if you could solve the puzzle by looking at the grids people post on Twitter. Each grid shows you the colors they got from the guesses, but not the letters. For a particular grid to be possible, there must be a sequence of valid words that produce that grid given the day's answer. If you have hundreds of peoples' grids for the day, is that sufficient to narrow down the space of possible words to 1?