Un problème de grille se traduit en SAT par une variable par case et par valeur possible. Le dénombrement se fait avant d'écrire quoi que ce soit, parce qu'il décide si le problème tient ou non.
La convention
Pour une grille de n sur n où chaque case peut prendre v valeurs, on emploie une variable par triplet ligne, colonne, valeur. Chaque case doit porter exactement une valeur.
Objectif
Donner les quatre dénombrements demandés.
Le premier concerne une grille où chaque case ne porte qu'une seule valeur possible, donc une variable par case.