Traduction du problème de diagnostic à SAT

Question

J'ai le problème de diagnostic suivant:
h (a): z1 = pas (in1)
h (d): z2 = pas (in2)
h (b): z3 = z1 ou z2
h (c): out1 = pas (z3)
h (e): out2 = pas (z3)

Ceci est une image du système:

J'ai une observation où je le sais:
in1 = faux
in2 = faux
out1 = vrai
out2 = vrai

Je veux vérifier si {b} est un diagnostic du système, ce qui signifie que je suppose que A, D, C, E est valide, alors que je ne suppose pas la même chose sur B.
Je veux devenir un problème SAT. Alors d'abord, je cartographier chaque variable de mon système à un littéral:
In1: 1
en2: 2
z1 (la sortie de a): 3
z2 (la sortie de d): 4
Z3 (la sortie de b): 5
out1: 6
Out2: 7

Donc, pour vérifier si {b} est un diagnostic du système (ce qui signifie que si je supprime l'hypothèse sur {b}, le système sera OK), je crée un CNF comme tel:

Non (1) et non (2) et 6 et 7 - cela représente mes observations, les variables dont je connais la valeur.

Maintenant, je veux ajouter une représentation pour mes contraintes. Par exemple, je sais que 6 = pas (5), mais je ne connais pas la valeur de 5 (car je ne peux pas supposer la validité du composant b).
Ma question est de savoir comment ajouter ces connaissances à ma représentation CNF? Si j'ajoute "pas (5)" à mon CNF, je suppose que la sortie de B est toujours fausse, et ce n'est pas correct.

Merci beaucoup.