Solveur DPLL récursif en OCaml

Présentation du projet

Ce projet implémente un solveur DPLL récursif pour résoudre des formules SAT exprimées en CNF (Conjunctive Normal Form).
Le code est écrit en OCaml, structuré de manière modulaire et commenté pour assurer clarté et maintenabilité.

L’objectif principal était de :

• Implémenter les fonctions clés du solveur : simplifie, unitaire, pur et solveur_dpll_rec.
• Garantir la correction et l’exactitude du solveur pour des instances SAT/UNSAT fournies.
• Concevoir une architecture flexible permettant d’ajouter des heuristiques ou des optimisations futures.

Ce dépôt inclut également :

• Le fichier RENDU détaillant notre méthodologie, les tests effectués et les choix d’implémentation.
• Des tests unitaires pour chacune des fonctions principales.
• Des exemples pour vérifier le fonctionnement global (examples/SAT, examples/UNSAT).

---

Structure du dépôt

dpll-solver/
├─ dpll_solver/
│  ├─ lib/
│  │  └─ dpll.ml         # Implémentation des fonctions du solveur
│  ├─ test/              # Tests unitaires et exemples
│  └─ dune-project
├─ examples/
│  ├─ SAT/
│  └─ UNSAT/
├─ Makefile              # Simplifie la compilation, les tests et l'exécution
├─ RENDU                 # Réponses détaillées aux questions du mini-projet
└─ README.md             # Ce fichier

---

Compilation et exécution

Méthode Make (depuis la racine du projet)

make dpll                  # Compilation
make test                  # Lancement des tests unitaires
make run FILE=examples/SAT/sudoku-4x4.cnf  # Exécution sur un fichier CNF
make clean                 # Nettoyage

Méthode Dune (depuis le dossier dpll_solver)

dune build
dune test
dune exec dpll_solver ../examples/SAT/sudoku-4x4.cnf
dune clean

Résultats attendus :

• Compilation sans erreurs ni warnings bloquants ✅
• Exécution correcte de sudoku-4x4.cnf ✅
• Tous les tests unitaires passent ✅
• Résultats corrects sur tous les exemples SAT/UNSAT ✅

---

Méthodologie et bonnes pratiques

• Fonction simplifie : utilisation de filter_map pour reconstruire efficacement la CNF en une seule passe.
• Fonction unitaire : détection récursive des clauses unitaires à l’aide de List.length et List.hd.
• Fonction pur : parcours des littéraux et utilisation de List.mem pour identifier les littéraux purs.
• Fonction solveur_dpll_rec : propagation unitaire et des littéraux purs avant le split pour réduire l’espace de recherche.

Tests et validation :

1. Tests unitaires sur les fonctions intermédiaires (simplifie, unitaire, pur).
2. Tests de bout en bout sur les instances examples/SAT et examples/UNSAT.
3. Vérification que le modèle SAT satisfait bien la CNF.

Philosophie :

"Do it right, then do it better" : code correct et clair d'abord, optimisation ensuite. Architecture modulaire et extensible pour intégrer facilement de futures heuristiques.

---

Contributeurs

• Abderrahman AJINOU
• Ahmed Moncef CHABIRA

Les deux membres ont contribué à l’ensemble des fonctionnalités et tests.

---

Fichier des consignes officielles

Pour référence, toutes les consignes fournies par le responsable sont disponibles dans le fichier : Consigne_du_Responsable.md

---

Licence

Projet interne pour le cours de L3 Informatique – Université Paris Cité.