Consistently Logical

In the recent 538 Riddler, a particular logical puzzle was posted which involves determining who is telling the truth if you assume their claims must all be consistent and that they meet an extra constraint that all liars are older than all truth-tellers. I’m going to show how we can proceed to solve this in code, and specifically using functional programming with Haskell.

Modelling the problem

The first place to start with any problem is deciding how to represent the information in the puzzle. Often the operations on these inputs flow naturally from the structures that we define.

The problem takes the form of a set of claims about the ages of other participants in the puzzle, where each claim states that the age of some person is a value, is not a value, is more than a value, or is less than a value. So lets represent the claims as a tuple of the operation and the value:

We need to decide what the Op is. The most straightforward approach is a sum-type with a constructor for each of the four operations we need, so:

However, when a claimant is lying, it is not that we gain no information, instead we can infer the inverse of the operator - for example if someone is lying that X is 17 then that is equivalent to someone telling the truth that X is not 17. The same goes for > and <, but with the caveat that these require the >= and <= operators to convey the inverses.

Then we need to model the claimants themselves. For our purposes, each of the islanders is identified by a single letter, so we will use Chars for our islander-names:

And a claimant is an islander along with the set of their claims.

For example, if ‘X says Y is more than 10 years old’, we can encode this as:

And this is all we need to encode the problem as specified in the 538 description, which, with a couple of helpers, we can do in such a way that it appears pretty similar to the problem statement itself.

What are you implying?

Once we know what each islander claims to be true, how can we find out whether their claims are mutually consistent. For example we can see that ‘A’ says that ‘B is more than 20’, but ‘D’ says that ‘B is 20’. Clearly they cannot both be right, but how would we determine that algorithmically?

Well, we can look at what each claim implies. Each claim is equivalent to saying that a value lies in one or more range of values. For example Gt 10 is the same as saying ‘in the range 11 ..’, and Is 12 is the same as ‘in the range 12 .. 12’. We can model Isnt as saying that a value must lie in one of two ranges, each of which excludes the value, so Isnt 12 means ‘must lie in the range ..11, or in the range 13..’.

This gives us a concept of the implications of each claim, and how we can represent them:

We can then go ahead and write smart constructors for the different implications of the various claims we can express:

And we can combine these in a single function from a claim to its implications:

Making Inferences

The next step is to look at how we can combine two implications to get the logical consequent. For instance, from Gt 10 and Lt 15 we should be able to infer that the value lies in the range 11..14. This implies some kind of monoidal structure, where implications can be combined to create more detailed ones. In which case we need the mempty base case:

And as a first pass we will look at what we can infer from two implications:

The inference from two implications is what we get by seeing what constraints each range applies to each range on the other side. Any ranges that are invalid as a result are removed by catMaybes, and if we don’t get any ranges at all we can’t return any implication, which means that the two statements are in contradiction.

Lets define a way to pretty print an implication, and then take this inference mechanism for a spin!

Now we can play around with infer:

Great, we seem to have a working inference engine. We can now wrap that up in a Monoid:

Finding a solution

We now have a lot of the pieces we need to find a solution, and one way we can go about that is to enumerate all the possible arrangements of liars and truth-tellers on the island, checking to see which ones are internally consistent, and then checking that all the liars are older than the truth-tellers. In our case that is perfectly tractable, as we only have to consider 2^5, or 32, arrangements.

First of all we need to tag an islander as either a liar or a truth-teller, and while we can use a Bool for this, it is much better to use a specific data-type for our purposes:

Then we need all 32 arrangements of these two values, eg:

  • Honest, Honest, Honest, Honest, Honest
  • Honest, Honest, Honest, Honest, Liar
  • Honest, Honest, Honest, Liar, Honest
  • and so on…

Lets create a small helper for that:

And we can quickly check that this does what we want:

Now we can generate all 32 potential solutions that we need to consider:

In order to find a solution, we need to combine all the claims about the islanders together, potentially inverting them if they come from liars, and then check to see if there were any contradictions, and whether it meets the age rule. First, lets define the types of solutions and their conclusions:

We need a way to turn a solution into a conclusion about all its claims:

and a way to know if a set of conclusions contains any contradictions:

and a way to determine if it meets the age-limit rule, where we check that the oldest honest person is younger than the youngest liar - or in the language of ranges, that the highest lower bound on the age of the honest claimants is lower than the lowest upper bound on the ages of the liars.

With that all in place, we can then proceed to search all the possible arrangements and print out the viable ones we find:

TaDa!

There is just one solution:

Solution: 1
---------------
a Liar 19
b Liar 20
c Honest 18
d Honest ..16
e Liar 20..

And we can clearly see from the conclusions that this is internally consistent. Walking through the puzzle manually with this solution should be enough to convince you that the solution is sound, but to my mind the nicest part is how naturally it flows from observing the way the parts are stuctured, from seeing the idea of ranges just fall out of the claims, to the fact that we can just fold the claims together using their monoidal structure and then being able to read the conclusions back from the consequences we had calculated. Being able to define the solution clearly made proceeding through the solution that much easier.