Translation of diagnosis problem to SAT
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.
$$