[LO5] 7.1. Recherche de modèle par énumération
Channel: Sylvain Schmitz
Date: 02/10/2020

Comment déterminer si un ensemble de clauses est satisfiable ? Une méthode naïve est d'essayer toutes les interprétations de ses propositions les unes après les autres, et de retourner « satistiable » si au moins une de ces interprétations satisfait l'ensemble de clauses. Cette méthode peut utiliser un algorithme récursif, dont les appels récursifs construisent un arbre de recherche de modèle : chaque branche de l'arbre correspond à une interprétation des propositions, et une fois arrivé à une feuille on teste si cette interprétation satisfait l'ensemble de clauses.