Boolean satisfiability

Solution

1. AND gives us X AND Y, which cannot be simplified further.

2. XOR gives us (X AND (NOT Y)) OR ((NOT X) AND Y), which cannot be simplified further.

3. XNOR gives us ((NOT X) AND (NOT Y)) OR (X AND Y), which cannot be simplified further.

Solution

1. The first circuit consists of two NOT’s which are combined with an AND and the output fed into a NOT. That is:

   NOT((NOT X) AND (NOT Y))

   This is an implementation of OR. In fact, the representation is neither in DNF nor CNF and if you transform it, you end up with

   X OR Y

   after an application of the De Morgan Identities and the law of Double Negation. This is both the DNF and CNF of the representation.

2. The second circuit is a bit more complex. On the right-hand side, we feed both inputs into an AND and apply NOT to the output,

   NOT(X AND Y)

   The right-hand side is actually the first circuit, which we know corresponds to

   NOT((NOT X) AND (NOT Y))

   The outputs of these two circuits are fed into an AND, which gives us the final representation:

   (NOT(X AND Y)) AND (NOT((NOT X) AND (NOT Y)))

   This formula can be simplified in various ways. One route is via the observation that the first circuit boils down to X OR Y. This means our circuit is just:

   (NOT(X AND Y)) AND (X OR Y)

   Maybe you can already see that this is the XOR function.

   Applying De Morgan, we can transform this into the CNF:

   ((NOT X) OR (NOT Y)) AND (X OR Y)

   To bring it into DNF, we need to apply Distributivity a bunch of times, but eventually, we can obtain:

   (X AND (NOT Y)) OR ((NOT X) AND Y)

Solution

1. The simplest representation is

   NOT(X XOR Y),

   that is XNOR is the negation of XOR. You can see this in the table by observing that everywhere the table of XOR has a 1, the table for XNOR has a 0, and everywhere XOR is 0, XNOR is 1. The values are just switched, using NOT.

   Note that this formula is neither in CNF nor DNF, of course.

2. Suppose we have two Boolean expressions A and B, which may be complex and use various variables, Boolean operations, etc. We can then check whether A and B are equivalent by checking whether

   A XOR B

   is SAT. Because by the function table for XOR,

   A XOR B = 1

   just in case A = 1 and B = 0 or A = 0 and B = 1, that is, just in case the values of A and B are different.

Solution

1. Here is the complete truth-table:

   

   Since there is no row where both expressions have the value 1, the two formulas are not jointly satisfiable.

2. Here’s the complete truth-table:

   

   Again, since there is no row where both expressions have the value 1, the two formulas are not jointly satisfiable.

Solution

The “brute force” DNF method yields the following monstrosity:

But if you analyze the truth-table a bit more carefully, then you can notice that in each case where SUN is true, the entire formula is true. And the only other cases where SUN is false and the formula is true are the two cases where WIND is false.

This means that we can equivalently write the formula as:

There are various algorithms for doing these kinds of simplifications, an important one of them is to use the Karnaugh map (opens in a new tab) , which is closely related to the Quine-McCluskey algorithm (opens in a new tab) .

Solution

1. If you apply the rewrite rule r₃ to this formula, you obtain

   RAIN ∧ ¬SUN ∧ ¬¬RAIN,
   which after one application of r₁ becomes
   RAIN ∧ ¬SUN ∧ RAIN.
   This is both the DNF and the CNF of the formula.

2. Here, applying r₃ yields:

   ¬RAIN∨ (¬¬ RAIN∧ ¬WIND).
   An application of r₁ gives
   ¬RAIN∨ (RAIN∧ ¬WIND).
   This is the DNF of the formula. To transform it into CNF, we need to apply r₄ to obtain:

3. This formula is in DNF. We need to apply distribution to get it into CNF. First, with r₄ we get:
   ((RAIN∧ ¬SUN)∨ ¬RAIN) ∧ ((RAIN∧ ¬SUN)∨¬SUN).
   Then, applying r₄’ twice, we get:
   (RAIN∨ ¬RAIN)∧ (¬SUN∨ ¬RAIN) ∧ (RAIN∨¬SUN) ∧ (¬SUN∧¬SUN),
   which is the formula’s CNF.

Solution

1. The formula is already in CNF, so we can directly transform it into sets to obtain:

   { SUN, RAIN, ¬WIND } { SUN, ¬ RAIN, ¬ WIND }.
   There is one possible application of resolution (eliminating RAIN and ¬RAIN), which yields
   { SUN, ¬WIND }.
   Since there are no more resolutions possible and we haven’t derived { }, we conclude that the formula is satisfiable. E.g. by setting v(SUN) = 1.

2. This formula, we need to transform into CNF first. Applying r₂, we obtain:

   (¬SUN∨ ¬RAIN) ∨ (WIND∧ ¬ WIND).
   An application of r₄ gives us from that:
   (¬SUN∨ ¬RAIN ∨ WIND)∧ (¬SUN∨ ¬RAIN ∨¬ WIND).
   Now, we can translate to sets to get:
   {¬SUN, ¬RAIN , WIND}   { ¬SUN, ¬RAIN, ¬ WIND}.
   But just one resolution is possible, which eliminates WIND and ¬WIND to give us:
   {¬SUN, ¬RAIN }.
   Since there are no more resolutions possible and we haven’t derived { }, we conclude that the formula is satisfiable. E.g. by setting v(SUN) = 0.

3. This formula is in CNF, so we directly go to the sets:

   { SUN, RAIN }  {SUN, ¬ RAIN}  {¬ SUN, RAIN}  {¬ SUN, ¬ RAIN}.
   The following is a derivation of { } from these using resolution:
   

   Note that we needed to use { SUN }, which was the result of the first resolution again in the last resolution. This is why it’s important to recursively resolve, meaning adding the results of the resolutions to our base and keeping on resolving until we can’t anymore.

   The conclusion is that the formula is unsatisfiable.

4. This formula is in CNF, so we can directly go to the sets:

   { SUN }  { SUN, RAIN }  { RAIN }  { RAIN, SUN }
   But since there are no ¬’s in this, we can not resolve and conclude that the formula is satisfiable, simply by setting v(SUN) = v(RAIN) = 1.

Solution

1. To check whether the inference is valid, we need to check whether

   SAT {¬RAIN, ¬(RAIN∨ (¬RAIN∧ SUN))}.
   Here’s how the truth-table method shows that the set is SAT:
   

   The red row shows that there’s a model where the premise is true and the conclusion false, thus the inference is invalid.

   To apply the resolution method, we first need to bring both formulas into CNF. ¬RAIN already is in CNF, so we focus on ¬(RAIN∨ (¬RAIN∧ SUN)) and apply r₃ to obtain:

   ¬RAIN∧ ¬(¬RAIN∧ SUN)).
   A following application of r₂ yields:
   ¬RAIN∧ (¬¬RAIN∨ ¬SUN)).
   Finally, applying r₁ gives us the CNF:
   ¬RAIN∧ (RAIN∨ ¬SUN)).

   We obtain the sets:

   { ¬RAIN } { RAIN, ¬SUN }
   Note that { ¬RAIN } is already there. One application of resolution eliminates RAIN and ¬ RAIN, giving us the set {¬SUN}. Since we cannot resolve any further, we conclude the set is satisfiable and the inference thus invalid. We can read off the same counter-model as before, if we so desire.

   Comparisons in terms of speed on this abstract level are tricky, but one way to compare the two is how many operations we needed to carry out. The truth-table method required us to generate 4 valuations and carry out 7 Boolean calculations each. That is a total 4 + (4 x 7) = = 32 operations. We were lucky that the first row yielded the correct answer, so we only needed to carry out 32 + 1 = 33 operations to obtain the correct result.

   For the resolution method, the main bottle neck is the transformation into CNF. Here, it took 3 steps. Add to this the single resolution step and 2 checks for possible further resolutions, this leaves us with a grand total of 3 + 1 + 2 = 6 steps.

   Of course, a real comparison in terms of speed depends on a lot of implementation details: how we enumerate the valuations, calculate the Boolean operations, recursively re-write formulas, check for resolvability, etc. In fact, we can imagine a smarter implementation of the truth-table method, where rather than first generating all the rows and columns and then checking, we first generate each row and then check whether it’s a countermodel and only continue if it isn’t. In this case, this would provide a speed-up, where we only need to generate one row, carry out 7 Boolean calculations, and do a final check. Since Boolean operations are fairly “low-level”—certainly lower level than recursive rewrites—it’s plausible that this smarter truth-table algorithm could outperform resolution in real world use-cases. In fact, there are various smarter ways of implementing truth-tables.

   But note that this depends on the counter-example occurring “early” in our truth-table, here in the first row. If the counter-example happens later in the table, or not at all because the inference is valid, resolution has a good chance to outperform truth-tables.

2. To check whether the inference is valid, we need to check whether

   SAT { RAIN∨ (RAIN∧ WIND), ¬(RAIN∨SUN)}
   Here’s the truth-table showing the unsatisfiability of the set:
   

   Note that we need to generate the full truth-table to see that there are no counter-examples.

   Resolution, instead, is much faster. First, we bring both formulas into CNF:

   • RAIN∨ (RAIN∧ WIND) requires one distribution r₄ to become (RAIN∨ RAIN )∧ (RAIN ∨ WIND).

   • ¬(RAIN∨SUN) requires one De Morgan re-write using r₂, giving us the CNF ¬RAIN ∧¬SUN

   The resulting sets of literals (clauses) are:

   { RAIN }   { RAIN, WIND } {¬ RAIN} {¬ SUN}.
   A single application of resolution on { RAIN } and {¬ RAIN} derives the empty clause { }, showing the unsatisfiability of the set, and thus validity of the inference.