3 ms·

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.

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.

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.