On vous demande de réaliser un solveur pour le problème des pigeons basé sur une modélisation à base de contraintes de cardinalité.
Le projet est à réaliser :
Le projet est à rendre pour le 23 Avril 2021 sous forme d'une archive (.zip, .tgz) par email à jean-michel.richer@univ-angers.fr
Le solveur doit prendre en compte les déductions que permettent d'effectuer les contraintes de cardinalité :
Par exemple pour une contrainte $#(α, β, L)$, si on a trouvé $β$ littéraux à vrai dans L, alors on peut en déduire que les autres littéraux non encore affectés devront être affectés à faux.
Votre solveur devra permettre de modifier le nombre de pigeons $N$, le nombre de pigeonniers $P$ et autorisera le choix de la méthode de résolution (avec ou sans déductions). Par exemple :
python pigeons.py 10 9 2
Lance la résolution du problème des pigeons pour $N=10$, $P=9$ avec la méthode 2 (avec déductions).
Le soveur devra également reporter le nombre d'appels à la fonction de résolution afin de vérifier que les déductions sont bien prises en compte.