Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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

share|improve this question
    
SAT like the test high school students take? Didn't seem to come up when I took it –  ShawnD Mar 7 '12 at 23:22
2  
    
The problem of deciding who's the winner (under optimal play) is an instance of TQBF. –  Yuval Filmus Mar 8 '12 at 3:29
    
@YuvalFilmus That's not QSAT? –  NickHalden Mar 8 '12 at 4:18
1  
TQBF = QSAT. –  Kyle Jones Mar 8 '12 at 7:15

1 Answer 1

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.

share|improve this answer

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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