reprenez le code fourni et optimisez le selon votre choix pour tenter d’accélérer la résolution. C’est à dire que vous tenterez d’organiser les choix lorsque plusieurs sont possibles à l’activation d’une règle.
appliquez votre algorithme sur les exemples existants dans le code
DPLL (Davis et Putman)
à partir du pseudo-code présenté dans le cours, implémentez l’algorithme de DPLL et optimisez le selon votre choix pour tenter d’accélérer la résolution. C’est à dire que vous tenterez d’organiser les choix lorsque plusieurs sont possibles à l’activation d’une règle.
appliquez votre algorithme sur les exemples existants dans le code précédent
Modèles
implémenter maintenant la version de DPLL permettant de retourner le modèle donnant un succès (cf. algorithme avec la notion de propagation unitaire)
par exemple, vous pouvez implémenter en 1er la fonction def propagation_unitaire(F: list, m: dict) -> tuple:
qui effectue la propagation unitaire sur la formule F ([[1,-2], [3,4]] par exemple) et le modèle m = dictionnaire de littéraux (entiers) affectés à des valeurs booléennes ({1: False, 3: True, 4: True} par exemple) en réutilisant des fonctions fournies dans le support
puis la fonction def DPLL_model(F: list, m: dict = None) -> dict | None:
qui lance la résolution avec un modèle initialement vide et retourne soit un modèle (dictionnaire), soit rien s’il n’y a pas de solution
implémenter une version qui affiche tous les modèles possibles à une formule.
Tests
Testez vos algorithmes sur 3 fichiers issus de uf50 (10 énoncés de 50 variables et +- 200 clauses, chaque énoncé est satisfiable), et de uuf50 (10 énoncés de 50 variables et +- 200 clauses, chaque énoncé est insatisfiable.
Testez avec uuf150 (énoncé de 150 variables sur 645 clauses).
Ces exemples sont issus de www.cs.ubc.ca/~hoos/SATLIB/benchm.html
A rendre
Les codes, commentés en indiquant vos d’optimisations, et idées d’optimisation
Les tests (avec le nombre d’appels aux algorithmes, et temps de résolution)