Writing in CNF that only one statement can be true

Question

Consider 5 Boolean variables $x_1, x_2, x_3, x_4, x_5$.

1. Write a propositional formula that expresses the fact that one and at most one among the Boolean variables $x_1, x_2, x_3, x_4, x_5$ is true.

2. Compute a conjunctive normal form of this formula.

Your answer must be justified.

I thought this was straightforward as I could just define $\phi_i$ as the conjunction of $x_i$ and not the others, but I'm not seeing a nice way to put that into CNF.

Answer 1

The proposition for "none are true" is: $(\neg x_1\wedge\neg x_2\wedge\neg x_3\wedge\neg x_4\wedge\neg x_5)$

The proposition for "only $x_1$ is true" is: $(x_1\wedge\neg x_2\wedge\neg x_3\wedge\neg x_4\wedge\neg x_5)$

And so forth. Use that to build a DNF for "at most one from the five is true," and simplify it (hint: use idempotence, distribution, and complementation).

Convert this to CNF.

Answer 2

I assume that for a) the task is to come up with a formula that says that exactly one of the variables is true.

This can be done fairly easily in DNF:

$$(x_1 \land \neg x_2 \land \neg x_3 \land \neg x_4 \land \neg x_5) \lor (\neg x_1 \land x_2 \land \neg x_3 \land \neg x_4 \land \neg x_5) \lor ...$$

(You can do the rest ... obviously you'll get $5$ terms like this)

However, how do we express this in CNF, as b) asks?

Well, you can always take a formula in DNF, and transform it into CNF by Distribution of $\lor$ over $\land$

For example:

$$(P \land Q) \lor (R \land S) \Leftrightarrow (P \lor R) \land (P \lor S) \land (Q \lor R) \land (Q \lor S)$$

(This should be reminiscent of the FOIL principle)

In your case, however, you'd get $5^5=3125$ terms .... and while many of them can be eliminated by further logical principles, this is not something you'd actually want to do ...

OK, can we do something else?

Yes, consider all possible ways in which it would be false that exactly one of the variables is true. So that would be when they are either all false, or when two or more of them are true, i.e.:

$$(\neg x_1 \land \neg x_2 \land \neg x_3 \land \neg x_4 \land \neg x_5) \lor (x_1 \land x_2) \lor (x_1 \land x_3) \lor ... \lor (x_1 \land x_5) \lor (x_2 \land x_3) \lor ...$$

(again, you can do the rest ... you'll get $1 + {5 \choose 2}=11$ terms)

OK, so since this statement is the negation of the statement you want, simply negate this statement to get the statement you want. And note: by doing a bunch of DeMorgan's, you'll get a statement nicely in CNF!

Answer 3

If you cannot use a computer to solve the problem, you can still use it to verify your solution:

>>> from sympy import *
>>> x1, x2, x3, x4, x5 = symbols('x1 x2 x3 x4 x5')
>>> Phi1 =     x1  & Not(x2) & Not(x3) & Not(x4) & Not(x5)
>>> Phi2 = Not(x1) &     x2  & Not(x3) & Not(x4) & Not(x5)
>>> Phi3 = Not(x1) & Not(x2) &     x3  & Not(x4) & Not(x5)
>>> Phi4 = Not(x1) & Not(x2) & Not(x3) &     x4  & Not(x5)
>>> Phi5 = Not(x1) & Not(x2) & Not(x3) & Not(x4) &     x5
>>> Psi = Phi1 | Phi2 | Phi3 | Phi4 | Phi5
>>> to_cnf(Psi, simplify=True)
And(Or(Not(x1), Not(x2)), Or(Not(x1), Not(x3)), Or(Not(x1), Not(x4)), Or(Not(x1), Not(x5)), Or(Not(x2), Not(x3)), Or(Not(x2), Not(x4)), Or(Not(x2), Not(x5)), Or(Not(x3), Not(x4)), Or(Not(x3), Not(x5)), Or(Not(x4), Not(x5)), Or(x1, x2, x3, x4, x5))

Hence, the formula in CNF is

$$\left(\neg x_{1} \vee \neg x_{2}\right) \wedge \left(\neg x_{1} \vee \neg x_{3}\right) \wedge \left(\neg x_{1} \vee \neg x_{4}\right) \wedge \left(\neg x_{1} \vee \neg x_{5}\right) \wedge \left(\neg x_{2} \vee \neg x_{3}\right) \wedge \left(\neg x_{2} \vee \neg x_{4}\right) \wedge \left(\neg x_{2} \vee \neg x_{5}\right) \wedge \left(\neg x_{3} \vee \neg x_{4}\right) \wedge \left(\neg x_{3} \vee \neg x_{5}\right) \wedge \left(\neg x_{4} \vee \neg x_{5}\right) \wedge \left(x_{1} \vee x_{2} \vee x_{3} \vee x_{4} \vee x_{5}\right)$$

Note that we have $11$ clauses, as Bram predicted.