I just use cat /usr/share/dict/words | grep 'X' where X is a regex that reflects most of the constraints I’ve uncovered up to that point. In most cases I don’t even need to try very hard with the regex because once the list is pared down to 10 or 15 words I can manually check them.
As much as I like Z3, I don’t think it is the right tool for this problem. I’d be willing to bet that encoding the dictionary into the solver will make it simply check each word separately, and you can probably do that faster and more legibly by iterating over the wordlist manually and checking the constraints like that.
Case in point, the many different constraints implementations shown don’t even cover the full range of possibilities you can encounter. Is that perhaps because it is hard to think about the general solution?
I don’t think the point of this article is to say that Z3 is the right tool for this job, but demonstrate how you might solve a tangible problem using it.
I’m trying an implementation of this out and I don’t know how performant this was for the author. Nowhere in the article details execution time, but adding (most of) the english language as ORs to a Z3 solver is not very performant. I would be interested in a follow up to the article detailing performance issues / improvements.
One thing this solver doesn’t seem to try, but is useful in Wordle is trying a word without the previous matches in order to find more possible letters. But now I wonder what’s the threshold where it’s useful? For example if you have 2 letters known, it’s probably useful to next guess a word without any of them to maximise the chances of finding more letters. But if you have 4 letters in the right place, it’s likely better to try a specific word (if there are only 1-2 options).
With four letters but five possible left over words it is better to guess words that do not contain letters you already know. Assume you find a word w containing three of the candidate letters (which is not unreasonable). Then the average number of guesses you get is w, then either solved, or 1.5 more guesses (since two words are left, for a total average of (3 * 2 + 2 * 2.5) / 5 = 2.2
Guessing the five words in sequence gives you 2.5 guesses on average.
I just use
cat /usr/share/dict/words | grep 'X'whereXis a regex that reflects most of the constraints I’ve uncovered up to that point. In most cases I don’t even need to try very hard with the regex because once the list is pared down to 10 or 15 words I can manually check them.As much as I like Z3, I don’t think it is the right tool for this problem. I’d be willing to bet that encoding the dictionary into the solver will make it simply check each word separately, and you can probably do that faster and more legibly by iterating over the wordlist manually and checking the constraints like that.
Case in point, the many different constraints implementations shown don’t even cover the full range of possibilities you can encounter. Is that perhaps because it is hard to think about the general solution?
I don’t think the point of this article is to say that Z3 is the right tool for this job, but demonstrate how you might solve a tangible problem using it.
I’m trying an implementation of this out and I don’t know how performant this was for the author. Nowhere in the article details execution time, but adding (most of) the english language as ORs to a Z3 solver is not very performant. I would be interested in a follow up to the article detailing performance issues / improvements.
One thing this solver doesn’t seem to try, but is useful in Wordle is trying a word without the previous matches in order to find more possible letters. But now I wonder what’s the threshold where it’s useful? For example if you have 2 letters known, it’s probably useful to next guess a word without any of them to maximise the chances of finding more letters. But if you have 4 letters in the right place, it’s likely better to try a specific word (if there are only 1-2 options).
With four letters but five possible left over words it is better to guess words that do not contain letters you already know. Assume you find a word w containing three of the candidate letters (which is not unreasonable). Then the average number of guesses you get is w, then either solved, or 1.5 more guesses (since two words are left, for a total average of (3 * 2 + 2 * 2.5) / 5 = 2.2
Guessing the five words in sequence gives you 2.5 guesses on average.
On “hard mode” you’re not allowed to do that, you have to include everything you’ve discovered up to that point in the next guess.