Algorithme DPLL

Une procédure de recherche récursive par retour arrière pour la satisfaisabilité propositionnelle qui combine la séparation de variables, la propagation d'unités (propagation des contraintes booléennes), l'élimination des littéraux purs et le retour arrière systématique pour décider si une formule en CNF est satisfiable.