Le SAT Game

Le jeu SAT Game est une présentation amusante du problème SAT. Ce problème consiste à déterminer si une formule booléenne (sous forme CNF) peut être rendue vraie en choisissant correctement les valeurs des variables booléennes (soit vrai, soit faux) qu’elle contient. Une ligne dans le jeu représente en fait une clause, c’est à dire une disjonction de littéraux (des variables ou leur négation reliées par des OU logiques). Une clause est vraie aussitôt qu’un de ses littéraux est vrai (il est représenté en vert dans le jeu). Comme les clauses sont reliées par des ET logiques, il faut que toutes les clauses soit vraies pour que la formule soit vraie.