John D. Cook posted a puzzle on his blog which is so short I’ll reproduce it here:

A certain question has the following possible answers.

    a. All of the below
    b. None of the below
    c. All of the above
    d. One of the above
    e. None of the above
    f. None of the above

Which answer is correct?

Now, this is probably where one should find paper and a pencil, write out the implications, simplify, hopefully come up with a solution and then feel clever. But not wanting to feel clever today – or perhaps for fear of not being clever – I decided to try and model the problem in Z3, Microsoft’s open source theorem prover. I installed Z3 and then installed the sbv library which is a frontend for several SMT solvers, but defaults to using Z3. A nice introduction to sbv can be found as part of the “24 days of Hackage” series.

Okay, so let’s encode the formulas. bAll is a generalized all and (<+>) is exclusive or.

import Data.SBV

p a b c d e f = bAll id [pa, pb, pc, pd, pe, pf]
  where pa = a <=> bAll id [b,c,d,e,f]   -- “All of the below”
        pb = b <=> bAll bnot [c,d,e,f]   -- “None of the below”
        pc = c <=> bAll id [a,b]         -- “All of the above”
        pd = d <=> a <+> b <+> c         -- “One of the above”
        pe = e <=> bAll bnot [a,b,c,d]   -- “None of the above”
        pf = f <=> bAll bnot [a,b,c,d,e] -- “None of the above”

Okay, so we have our formulas, and we specify that we want all of them to hold as the body of p. Now let’s see if this is satisfiable.

λ> allSat p
Solution #1:
  s0 = False
  s1 = False
  s2 = False
  s3 = False
  s4 = True
  s5 = False
This is the only solution.
(0.01 secs, 4,361,872 bytes)

Boom! It seems that e is the solution (if my encoding is correct :).