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

$\endgroup$
5
  • $\begingroup$ SAT like the test high school students take? Didn't seem to come up when I took it $\endgroup$
    – ShawnD
    Mar 7 '12 at 23:22
  • 2
    $\begingroup$ @ShawnD: en.wikipedia.org/wiki/Boolean_satisfiability_problem $\endgroup$ Mar 7 '12 at 23:33
  • $\begingroup$ The problem of deciding who's the winner (under optimal play) is an instance of TQBF. $\endgroup$ Mar 8 '12 at 3:29
  • $\begingroup$ @YuvalFilmus That's not QSAT? $\endgroup$
    – NickHalden
    Mar 8 '12 at 4:18
  • 1
    $\begingroup$ TQBF = QSAT. $\endgroup$
    – Kyle Jones
    Mar 8 '12 at 7:15
0
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.