satisfiablity modulo wordle

surdle

#!/usr/bin/env python3
#
# Satisfiability modulo wordle: solving that annoying game for you, once and
# for all.
#
# Usage:
# $ python3 -m venv ./venv
# $ source ./venv/bin/activate
# (venv) $ pip install z3-solver
# (venv) $ python surdle.py

import argparse
import logging
import sys
import z3

from typing import Dict, List


solver = z3.Solver()
solver.set(unsat_core=True)
solver.set(':core.minimize', True)
letters = z3.Ints('l1 l2 l3 l4 l5')

clauses: Dict[z3.Bool, z3.ExprRef] = {}

def parse_args(argv: List[str]) -> argparse.Namespace:
    parser = argparse.ArgumentParser(
        description="Wordle cheater",
        formatter_class=argparse.ArgumentDefaultsHelpFormatter)

    ivyp = parser.add_argument_group("Parameters")
    ivyp.add_argument("-d", "--dictfile",
            help="The path to a newline-separated file of English words.",
            default="/usr/share/dict/words")
    ivyp.add_argument("-v", "--verbose",
            help="Dump more info.  More 'v's ==> more info.",
            action='count', default=0)
    args = parser.parse_args(argv)
    init_logging(args)

    return args

def init_logging(args: argparse.Namespace):
    if args.verbose == 0:
        l = logging.WARNING
    if args.verbose == 1:
        l = logging.INFO
    elif args.verbose >= 2:
        #z3.set_option(verbose=5)
        l = logging.DEBUG
    else:
        raise Exception(f"Unxpected verbosity level {args.verbose}")
    logging.basicConfig(format='surdle:%(levelname)s:%(message)s', level=l)

def remember_expr(e: z3.ExprRef):
    """ Inserts the expr into the solver, and remembers it with a fresh
    identifier so unsat_core can tell us something useful."""
    fresh_id = z3.Bool("b" + str(len(clauses)))
    clauses[fresh_id] = e
    solver.assert_and_track(e, fresh_id)

def encode_char(i: int, c: str) -> z3.ExprRef:
    assert(len(c) == 1)
    assert(c.islower())
    return letters[i] == ord(c)

def encode(s: str) -> List[z3.ExprRef]:
    assert(len(s) == 5)
    return [encode_char(i,c) for i,c in enumerate(s)]

def decode(model: List[z3.ExprRef]) -> str:
    ords: List[int] = [model[l].as_long() for l in letters]
    s = "".join([chr(i) for i in ords])

    assert(len(s) == 5)
    assert(s.islower())
    return s

def domain_constraints() -> z3.And:
    """ Adds a conjunction constraining the range of all letters. """
    return z3.And([
        z3.And([l >= ord('a'),
                l <= ord('z')]) for l in letters])

def dictionary_constraints(fn: str) -> z3.Or:
    """Adds a disjunction of five-letter English words."""

    constraints: List[z3.And] = []
    with open(fn) as f:
        logging.info(f"Reading dictionary at {fn}...")
        for line in f:
            line = line.lower().strip()
            if len(line) != 5:
                continue
            constraints.append(z3.And(*encode(line)))
        logging.info(f"Added {len(constraints)} dictionary constraints.")
    return z3.Or(*constraints)

def green_constraint(i: int, c: str) -> z3.ExprRef:
    """ Encodes the fact that letter i is exactly c. """
    logging.debug(f"Remembering that letter {i} is {c}")
    return letters[i] == ord(c)

def yellow_constraint(i: int, c: str) -> z3.ExprRef:
    """" Encodes the fact that c is in the word but not at position i."""
    constraints = []
    candidates = []
    for j in range(len(letters)):
        if j != i:
            candidates.append(j)
            constraints.append(letters[j] == ord(c))
    logging.debug(f"Remembering that one or more of {str(candidates)} is {c}")
    return z3.And(
            letters[i] != ord(c),
            z3.Or(constraints))

def black_constraint(i: int, c: str) -> z3.ExprRef:
    """ Encodes the fact that c is nowhere in the word."""
    logging.debug(f"Remembering that no letter is {c}")
    constraints = [letters[j] != ord(c) for j in range(5)]
    return z3.And(*constraints)

def read_resp() -> str:
    while True:
        feedback = input("> ").strip()
        valid = [c in "🟩🟨⬛gyb" for c in feedback]
        if len(feedback) == 5 and all(valid):
            return feedback

def main(argv: List[str]) -> int:
    args = parse_args(argv[1:])
    solver.add(domain_constraints())
    solver.add(dictionary_constraints(args.dictfile))

    action_table = {
        '⬛': black_constraint,
        '🟨': yellow_constraint,
        '🟩': green_constraint,
        'b': black_constraint,
        'y': yellow_constraint,
        'g': green_constraint
    }

    while True:
        solver.push()
        while solver.check() == z3.sat:
            logging.info("Solving...")

            m = solver.model()
            guess = decode(m)
            print(f"Guessing {guess}")

            # Check for unique solutions
            solver.push()
            solver.add(z3.Not(z3.And(*encode(guess))))
            sat = solver.check()
            solver.pop()
            if sat == z3.unsat:
                print("Unique!")
                break

            feedback = read_resp()

            for i, c in enumerate(feedback):
                remember_expr(action_table[c](i,guess[i]))

        else:
            unsats = [clauses[u] for u in solver.unsat_core()]
            logging.error(f"Contradiction involving some of these clauses!  {[clauses[u] for u in solver.unsat_core()]}...")
            break

        logging.info("Resetting solver state...")
        solver.pop()

    return 0

if __name__ == "__main__":
    sys.exit(main(sys.argv))

Using Z3 is a neat idea - I've been dinking around with a solution myself and never considered it.

I did load this up with the word list from Wordle's source though and the solver fails on most words after 3 guesses with an empty unsat core.

Happy to help troubleshooting - would be fun to get this working.

Interesting, with OSX's stock words file it does converge for me but admittedly at least personally it's hard to play the game against myself and not accidentally introduce a contradiction :) Did the Wordle word list get leaked somewhere?

The empty unsat core is a bit interesting; that ought to show the minimally-contradicting set of clauses, so if it's empty then I wonder what's up...

The word list didn't leak - it's in the client side code. There are two lists of words - a list of ~2k of words used for the puzzles and another ~12k it accepts for guesses. Happy to send it your way to reproduce.

Oh, sure, I'd appreciate that, thank you! I am n b taylor at gmail dot com !