For this problem, an enumerative solver may be more optimal (and faster); where optimality is finding the word with the least number of guesses: There are ~158k 5-letter words. Start with a word containing letters with the highest frequency of occurrence amongst 5 letter words (this prob distr is likely to be close to the distr in the english language). Make that guess. Eliminate any words containing black letters, or not having green letters in the right place, or missing a yellow letter. Pick the highest probability word from the remaining. Repeat.

This should almost always get you the answer in 3 guesses. [Edit: Realized after writing that 3 is too optimistic given you might not have enough constraints after the 2nd guess, and agree with dzdt's comment. 4 might be where we end up at.]

I would be curious to see the distribution of #guesses needed across the 158k words.

Does anybody know good resources for learning z3. I find the docs hard and material is pretty scarce on the topic.
is this game the new flappy bird? Why are dozens of posts made every day?