2
$\begingroup$

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:
enter image description here

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.

$\endgroup$
1
$\begingroup$

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. $$

$\endgroup$
  • $\begingroup$ thanks! Is there any way I can derive other formulas? such as x = y XOR z, or x = y NAND z? I understand the derivations but it's not so intuitive for me to come up with new ones. $\endgroup$ – erap129 May 19 at 9:13
  • $\begingroup$ It’s the CNF representation of the Boolean function corresponding to the equation. You will probably learn about it, if you haven’t already. $\endgroup$ – Yuval Filmus May 19 at 10:10

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.