Solveur SAT (Algorithme DPLL)

Ce projet est un solveur SAT performant développé en OCaml. Il implémente l'algorithme complet DPLL (Davis-Putnam-Logemann-Loveland) pour déterminer la satisfaisabilité de formules logiques en Forme Normale Conjonctive (CNF).

Fonctionnalités

Le solveur utilise plusieurs techniques d'optimisation pour réduire l'espace de recherche :

• Propagation unitaire : Simplification automatique lorsqu'une clause ne contient qu'un seul littéral.
• Élimination des littéraux purs : Identification et assignation des littéraux qui n'apparaissent que sous une seule polarité dans la formule.
• Backtracking intelligent : Exploration récursive des branches avec choix de littéral pivot en cas d'absence de simplifications immédiates.

Structure du projet

• lib/dpll.ml : Cœur de l'algorithme (simplifications, heuristiques et solveur récursif).
• lib/dimacs.ml : Parseur pour les fichiers au format standard DIMACS.
• bin/main.ml : Point d'entrée de l'exécutable CLI.

Prérequis

• OCaml (version 4.08.0 ou supérieure recommandée)
• Système de build dune
• Bibliothèque ppx_inline_test pour les tests unitaires

Installation et Compilation

Placez-vous dans le répertoire dpll_solver et lancez la compilation :

dune build

Utilisation

Le programme prend en entrée un fichier au format .cnf :

dune exec dpll_solver <chemin_vers_fichier.cnf>

Tests

Le projet inclut une suite de tests unitaires validant chaque étape de la simplification (littéraux purs, clauses unitaires, etc.).

Exécutez les tests avec :

dune test