Le but du mini-projet est d'implémenter un solveur DPLL récursif en OCaml. Vous devez compléter pour cela le code dans le fichier dpll.ml :
- la fonction simplifie : int -> int list list -> int list list
- la fonction unitaire : int list list -> int
- la fonction pur : int list list -> int
- la fonction solveur_dpll_rec : int list list -> int list -> int list option
Ces types et les commentaires dans dpll.ml sont indicatifs. D'autres
choix peuvent être pertinents ; par exemple, unitaire et pur
pourraient aussi être de type int list list -> int option. Aussi, les
définitions let foo ...' peuvent être transformées en let rec foo ...' ou
inversement.
Vous devez documenter votre code en remplissant le fichier RENDU. Dans ce fichier, vous trouverez des questions précises sur votre implémentation. Vos réponses à ces questions constitueront une partie importante de votre note. Un mini-projet sans fichier RENDU rempli ne recevra pas de note.
Outre les exemples de test inclus dans dpll.ml (exemple_3_12, exemple_7_2, exemple_7_4, exemple_7_8, systeme, coloriage), vous pouvez utiliser le Makefile en appelant
make
pour compiler un exécutable natif et le tester sur des fichiers au format DIMACS. Vous trouverez des exemples de fichiers à l'adresse
https://www.irif.fr/~schmitz/teach/2021_lo5/dimacs/
Par exemple,
./dpll chemin/vers/sudoku-4x4.cnf
devrait répondre
SAT -111 -112 113 -114 -121 -122 -123 124 -131 132 -133 -134 141 -142 -143 -144 -211 212 -213 -214 221 -222 -223 -224 -231 -232 -233 234 -241 -242 243 -244 311 -312 -313 -314 -321 322 -323 -324 -331 -332 333 -334 -341 -342 -343 344 -411 -412 -413 414 -421 -422 423 -424 431 -432 -433 -434 -441 442 -443 -444 0
Si vous faites des affichages pour vos propres tests, il faudra penser à commenter ces tests pour que votre programme réponde exactement comme indiqué juste ci-dessus.
- date limite : 29 octobre 2021, 23h59
- sur la page Moodle du cours https://moodle.u-paris.fr/course/view.php?id=1657
- sous la forme d'une archive XX-nom1-nom2.zip où
XX' est le numéro de binôme déclaré à la page https://moodle.u-paris.fr/mod/choicegroup/view.php?id=82687 etnom1' et `nom2' sont les noms de famille des deux membres du binôme, contenant l'arborescence suivante : XX-nom1-nom2/dpll.ml XX-nom1-nom2/dimacs.ml XX-nom1-nom2/Makefile XX-nom1-nom2/RENDU