L'autre issue de DPLL est l'échec de toutes les branches. La plus petite formule qui l'illustre sans contenir la moindre clause unitaire tient sur deux variables.
La formule
c1 = (x ou y), c2 = (non x ou y), c3 = (x ou non y), c4 = (non x ou non y)
Objectif
Compter les affectations possibles, celles qui satisfont la formule, conclure sur la satisfiabilité, et compter les clauses.
Rappels
Quatre clauses sur deux variables : chacune interdit exactement une des quatre affectations possibles, et ensemble elles les interdisent toutes.
Pièges
Répondre « satisfiable » demande une seule affectation. Répondre « insatisfiable » demande d'avoir épuisé toutes les branches, et c'est pour cela que la seconde réponse coûte structurellement plus cher que la première.