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)
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)