DPLL alterne trois opérations, dont une seule est un pari. Dérouler une trace complète rend la différence visible.
La formule
c1 = (x ou y), c2 = (non x ou z), c3 = (non x ou non z), c4 = (y ou z)
Aucune clause n'est unitaire au départ : la propagation ne peut rien faire, et il faut décider.
La trace
décision x = 1
propagation z = 1 imposée par c2
conflit sur c3
décision x = 0
propagation y = 1 imposée par c1
modèle
Objectif
Compter les décisions, les propagations et les conflits, puis les variables restées libres dans le modèle.
Rappels
Propager est une déduction : aucun modèle n'est perdu, il n'y aura jamais à revenir dessus. Décider est un pari : si la branche échoue, il faudra essayer l'autre valeur. Seules les décisions coûtent.
Pièges
Le modèle trouvé ne fixe pas toutes les variables. Les clauses où figure la dernière sont déjà satisfaites par d'autres littéraux, et le solveur n'a aucune raison de la décider. Un solveur réel lui donnera une valeur arbitraire avant de répondre.