I created a solver using a SAT/SMT solver that guesses a solution that is consistent with all the previous guesses and their corresponding feedback. It always returns a solution in a small number of guesses. I don’t think it is the optimal solving algorithm but it was a fun exercise!