The SAT problem is well known. Take a long Boolean expression in k variables and find an assignment of true and false to the k variables which makes the expression true. This might not be possible, but if it is the expression is said to be satisfied - hence the name of the problem.

The decision version of the problem is to simply decided if the given formula is satisfiable or not.

For k=3 and greater the SAT problem is known to be NP-Complete.

An NP problem is one that you can check a proposed solution for in polynomial time, but you can't necessarily find a solution in polynomial time. The SAT problem is clearly in NP because if I give you an assignment of values to the variable it is easy for you to check that the formula is true - in which case it is satisfiable.

The "Complete" part of the description is there because if you can solve the SAT problem in polynomial time then all of the NP problems can be solved in polynomial time. That is, SAT is a representative of all of the problem in NP.

You can see it is an important problem, but how can we understand it better?

Olivier Bailleux at Universite de Bourgogne Franche-Comte has invented a nice game that is equivalent to the SAT problem.

This is how it works. The starting configuration is a set of boxes with round and square tokens in different colors. All you have to do is remove all the round or square tokens of a particular color. That is, the final configuration should have each color assigned to one of the shapes and at least one shape in each box.

This figure, taken from the paper, shows a complete game:

The order in which tokens are removed makes no difference; it is only the starting and final states that matter.

Not all starting configurations can be converted into the desired final state and the ones that can are called feasible.

The game is not easy to play, but it is engaging. Normally complexity theorists spend time proving that some game or other is NP, but in this case the game has been derived from the SAT problem and so it is NP complete.  

How does it relate to the SAT problem?

Each of the boxes is a logical clause. Each color is a variable and square corresponds to a true and round to a false.  

The initial configuration can be read as a logical expression - a square is a positive variable and a round is a negative. So the initial configuration in the figure above corresponds to:

(r or  b or  not p)
  and ( not r or  b or not p)
   and  (r or  not b or  not p)
    and  (not r or not b or not p)
     and (p or y)
      and (r or not y)
       and (b or not y)

The SAT problem is to find a true/false assignment to r, b and p such that each clause it true - they all have to be true for the AND of all of them to be true.

Going back to the game, this is equivalent to assigning each color to one of the shapes. If you can do this and have at least one shape in each box then each box evaluates to true - as it is the OR of each of the variables you only need one to make the entire box true.

If you think about it for a while it starts to make sense.

If you play the game for then you start to appreciate the difficulties of the SAT problem.

One word of warning: don't reduce the game to two colors just to see how things work because the SAT problem on 2 variables is in P not NP.

satgameicon

Now all we need is for someone to implement it as a web or mobile based game and we can all start playing it.