My question is about how the Hasbro game Connect4 can be viewed as a SAT problem.
My initial guess is that it would actually be QSAT, and that the 'problem' would be something along the lines of: "Is there a set of black/white turns such that X will happen" where X is some condition on the board.
I guess you could even specify that X has to be reached after a certain number of turns n.
Any ideas on encoding connect4 as a Q/SAT problem or any ideas on interesting questions that can be asked about it are welcome. Thank you muchly!
For reference if necessary: Thesis about Connect4 from AI perspective