Solveur DPLL récursif en OCaml

Projet universitaire réalisé dans le cadre du cours Logique (LO5) – L3 Informatique, Université Paris Cité (UFR Informatique).
Ce mini-projet consistait à implémenter un solveur récursif du problème SAT à l’aide de l’algorithme DPLL (Davis–Putnam–Logemann–Loveland).

---

Objectif du projet

Le but du projet est d’implémenter un solveur DPLL récursif en OCaml, capable de déterminer si une formule booléenne en forme normale conjonctive (CNF) est satisfiable ou non.

L’algorithme DPLL est un algorithme récursif de recherche de modèle utilisé dans de nombreux solveurs SAT modernes.
Il repose sur plusieurs étapes clés :

1. Simplification de la formule à chaque affectation d’un littéral.
2. Propagation unitaire : si une clause contient un seul littéral non satisfait, celui-ci doit être vrai.
3. Élimination des littéraux purs : un littéral apparaissant toujours avec le même signe peut être fixé pour satisfaire les clauses où il figure.
4. Choix récursif d’un littéral et exploration des deux cas possibles (vrai/faux).

---

Structure du projet

dpll_solver/
├── dune-project
├── dune
├── lib/
│   ├── dpll.ml          # Implémentation principale du solveur DPLL
│   ├── dimacs.ml        # Parsing des fichiers CNF au format DIMACS
│   └── ...
├── examples/
│   └── SAT/
│       ├── sudoku-4x4.cnf
│       ├── coloriage.cnf
│       └── ...
├── test/
│   ├── exemple_3_12.cnf
│   ├── exemple_7_2.cnf
│   └── ...

---

Fonctions principales à implémenter

Le projet demandait notamment de réaliser l'implémentation des fonctions suivantes :

• simplifie : literal -> cnf -> cnf
  → simplifie la CNF après l’affectation d’un littéral.

• unitaire : cnf -> literal option
  → recherche d’un littéral unitaire.

• pur : cnf -> literal option
  → détection d’un littéral pur (positif ou négatif).

• solveur_dpll_rec : cnf -> interpretation -> interpretation option
  → cœur récursif du solveur DPLL.

Chaque fonction a été soigneusement documentée et testée à l’aide de tests unitaires inline.

---

Compilation et exécution

1. Compilation

Le projet utilise le système de build Dune.

cd dpll_solver
dune build

Il peut être nécessaire d’installer quelques dépendances :

sudo apt-get install ocaml-dune libppx-inline-test-ocaml-dev > libppx-assert-ocaml libppx-hash-ocaml libppx-enumerate-ocaml > libjane-street-headers-ocaml

---

2. Exécution

Pour exécuter le solveur sur un fichier .cnf :

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

Exemple de sortie attendue :

SAT
-111 -112 113 -114 -121 -122 -123 124 -131 132 -133 -134 141 -142 -143 -144 ...

---

Tests unitaires et validation

Des tests unitaires inline ont été ajoutés directement dans dpll.ml pour valider le comportement des fonctions :

dune test

Exemples de jeux de tests utilisés :

• examples/SAT/sudoku-4x4.cnf
• examples/SAT/coloriage.cnf
• test/exemple_7_2.cnf, test/exemple_7_4.cnf, test/systeme.cnf, etc.

Les tests couvrent à la fois :

• la correction fonctionnelle (résultat SAT/UNSAT attendu),
• la robustesse de la simplification,
• et les performances sur des instances plus volumineuses.

---

Performance & méthodologie

L’évaluation du projet reposait sur trois volets :

Critère	Description	Pondération
Documentation	Code clair, bien commenté, fichier RENDU complet	40 %
Correction	Fonctionnement global conforme, bons résultats sur les exemples	40 %
Optimisation	Heuristiques et structures de données efficaces	20 %

---

Exemples d'utilisation

# Test d’un fichier DIMACS SAT
dune exec dpll_solver ../examples/SAT/coloriage.cnf

# Lancer tous les tests unitaires
dune test

# Recompiler après modification
dune build

---

Le DPLL est la base de nombreux solveurs SAT modernes — ce projet en est une implémentation pédagogique fidèle et documentée.