Translation of diagnosis problem to SAT

Question

I have the following diagnosis problem:
h(A): z1 = not(in1)
h(D): z2 = not(in2)
h(B): z3 = z1 or z2
h(C): out1 = not(z3)
h(E): out2 = not(z3)

This is an image of the system:

I have an observation where I know that:
in1 = false
in2 = false
out1 = true
out2 = true

I want to check if {B} is a diagnosis of the system, meaning that I assume that A,D,C,E are valid, while I don't assume the same about B.
This I want to turn into a sat problem. So first I map each variable in my system to a literal:
in1: 1
in2: 2
z1 (the output of A): 3
z2 (the output of D): 4
z3 (the output of B): 5
out1: 6
out2: 7

So to check if {B} is a diagnosis of the system (meaning that if I remove the assumption about {B} the system will be OK) I create a CNF like so:

not(1) AND not(2) AND 6 AND 7 - this represents my observations, the variables whose value I know for sure.

Now I want to add a representation for my constraints. For example, I know that 6 = not(5), but I don't know the value of 5 (because I can't assume the validity of component B).
My question is how do I add this knowledge to my CNF representation? If I add "not(5)" to my CNF then I assume the output of B is always false, and this isn't correct.

Thank you very much.

Answer 1

In order to express $x = \lnot y$ in CNF form, you add the clauses $$ x \lor y, \lnot x \lor \lnot y. $$ In order to express $x = y \lor z$ in CNF form, you add the clauses $$ \lnot y \lor x, \lnot z \lor x, \lnot x \lor y \lor z. $$ In order to express $x = y \land z$ in CNF form, you add the clauses $$ \lnot x \lor y, \lnot x \lor z, \lnot y \lor \lnot z \lor x. $$