3-SAT in Clue

Consider a game of clue. Now consider the set of queries answered by a given player by showing the queries a card. That player’s hand must satisfy the expression:

At first glace it looks a lot like 3-SAT! There are a few reasons I can think of that it might not by 3-SAT though.

  • Many tuples cannot occur i.e. (knife or wrench or gun)
  • Setting all variables to true satisfies the expression. We need to also encode the size of the hand somehow. I can’t think of a way to do so that guarantees we stay in 3CNF.
  • We gain a ton of information when a player cannot show a card. We now know three cards they don’ t have. This could potentially simplify our 3-SAT to 2-SAT (boring).
    • Similarly we know that several variables are false since the player can’t have cards that we have. That will also help us simplify to 2-SAT.
  • We have one 3CNF expression for each player but they aren’t independent. If one player has the wrench then the other does not.

I’m pretty convinced that there is no trivial reduction from determing a clue hand to 3-SAT but am not yet convinced one way or the other if it is NP. It seems like we have some pretty strong tools to simplify the problem but I’m not sure if they are enough to bring us down from NP.

Written on September 29, 2015