Choose your level and start a new game

Need help ?
You chose level
"too easy"
Warning! One line contains only red cells!
Congratulation, you won!
Rules of the game

The game is won when at least one cell on each line is green. Clicking on a number will color each cell with the same number in green, and each cell with the opposite number in red. Clicking on a colored cell will remove both colors.

points out lines which don't yet contain a green cell

points out lines where there's only one chance left to put a green cell

points out lines which are completely red

click on this undo button to cancel your last choice
click on this traffic light to query the oracle (green=you're on the right way, red=this is a dead end, you have to change your last choices)

The SAT Game is a funny representation of the SAT problem. In this problem, one must find a valuation of Boolean variables (true/false) such that a Boolean CNF formula evaluates to true. A line in the game actually represents a clause, which is a disjunction of literals (variables or their negation connected by logical OR). A clause evaluates to true as soon as one of its literals is true. Since clauses are connected by logical AND, all clauses must evaluate to true so that the formula be true.