A SAT Based Game
Written by Mike James   
Saturday, 05 December 2015

The Boolean Satisfiability problem or SAT is the best known NP Complete problem. It is fairly easy to understand if you have some knowledge of Boolean logic but now we have a simple game that helps you really get inside what is going on. 

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. 



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

More Information

SAT as a game Olivier Bailleux

Related Articles

The Computer Science Breakthrough Of The Decade       

The Knapsack Problem   

Candy Crush Is Harder Than It Sounds - NP Hard       

Computational Complexity       

What Is Computable?       

Unshuffling A Square Is NP-Complete       

The Chaos Within Sudoku - A Richter Scale       

Physics Is NP Hard       


To be informed about new articles on I Programmer, sign up for our weekly newsletter, subscribe to the RSS feed and follow us on, Twitter, FacebookGoogle+ or Linkedin



OpenSSF's Siren To Warn About OSS Vulnerabilities

Siren is a new mailing list by the OpenSSF which aims to monitor the threat landscape of open-source project vulnerabilities in order to provide real time alerts to anyone subscribed.

Mirascope-Python's Alternative To Langchain

Mirascope is a Python library that lets you access a range of Large Language Models, but in a more straightforward and Pythonic way.

More News


kotlin book



or email your comment to: comments@i-programmer.info

Last Updated ( Saturday, 05 December 2015 )