Choose your level and start a new game too easy easy average hard too hard Need help ? Choose a cell for me ! You chose level "too hard" Warning! One line contains only red cells! Congratulation, you won! Start a new game

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)

3 -5 2 -5 -8 -6 -7 1 5 6 -4 8 1 -8 -5 2 3 4 -4 9 -5 1 8 -5 2 -5 -9 6 2 8 -2 -3 1 9 -1 -4 -6 5 3 7 3 -2 6 -8 5 2 -8 -3 7 1 -8 -6 5 8 -4 -6 -1 -7 -9 8

8 4 5 3 -6 2 6 -9 4 1 -5 -9 -8 1 -7 -3 -7 2 -4 -6 -2 8 -3 -6 -2 -4 -7 6 -8 1 -2 1 -6 2 4 -6 7 4 5 -4 -3 -9 -2 1 6 -7 3 1 1 8 3 -2 -7 8 -1 8 -4 -2 5 -1

-8 6 3 9 -5 -4 -9 -6 1 -4 8 -6 -4 8 1 -6 -2 -8 -7 -9 8 4 1 -3 -9 -1 -5 4 -9 1 -7 9 8 -3 -1 -6 -5 -4 9 -4 1 -3 -7 -1 -2 6 5 -3 9 3 1 -9 -7 4 9 8 2 -8 -5 9

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.