4
$\begingroup$

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

  • 1
    [TQBF = QSAT](http://en.wikipedia.org/wiki/QSAT).2012-03-08

1 Answers 1

0

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.

Quantifiers aren't needed to encode this game. First, you construct a SAT instance whose satisfying assignments encode the legal board positions after the first move of a Connect 4 game. Then you add clauses and new variables whose satisfying assignments encode legal board positions after a second move given a legal first move. Repeat this process, in effect creating a Matrioshka doll of instances, to cover the number of plies you want to allow the SAT solver to explore. Add clauses to recognize a won game by either side which induce a truth value in a special selector variable that satisfies all clauses and short circuits the search.