# Playing With SBV

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

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 :).