Mini-projet 1 : solveur DPLL récursif

Objectif du mini-projet

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.

Tester son mini-projet

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.

Rendre son mini-projet

• 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 et nom1' 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