La première opération de DPLL n'est pas un choix. Tant qu'une clause impose une valeur, la prendre ne coûte rien et ne ferme aucune porte.
La formule et l'affectation
c1 = (x ou y), c2 = (non x ou z), c3 = (y ou z ou t), c4 = (non y ou t)
L'affectation partielle courante est x = 1, y = 0.
Objectif
Compter les clauses unitaires sous cette affectation, nommer le littéral que la propagation impose, puis répondre aux deux questions de principe.
Rappels
Une clause est unitaire lorsque tous ses littéraux sauf un sont faux, et que le dernier est libre. Ce dernier doit alors être vrai dans tout modèle qui prolonge l'affectation.
Pièges
c1 est déjà satisfaite par x, et c4 l'est par non y. Elles n'imposent rien. c3 compte encore deux littéraux libres. Une seule clause est réellement unitaire.