Layton Puzzle in IDP-Z3

A few days ago, I came across a post titled Solving a "Layton Puzzle" with Prolog, in which the author describes a Prolog implementation of a puzzle from one of the Professor Layton games. It's quite an elegant implementation (check it out!), and it made me think about how we could solve it using the IDP-Z3 reasoning engine instead.

First, let's learn more about the puzzle. The description in text is essentially as follows:

Mary, Dan, Lisa and Colin answered the same 10 A/B questions. Mary (BBABABBAB) got a total grade of 70, Dan (BAAABABAAA) got 50, and Lisa (BAAABBBABA) got 30. Given these answers, how much did Colin (BBAAABBAAA) get?

The key of the puzzle is that we are not given the correct answers, and need to derive them ourselves.

IDP-Z3 knowledge base

In IDP-Z3, we model problems by creating a knowledge base that consists of three blocks:

• a vocabulary, declaring symbols we use to describe a problem
• a structure, optionally defining the values of symbols
• a theory, in which we can write logical formulas

Given these three blocks, IDP-Z3 can perform a number of logical reasoning tasks. Let's try it!

Vocabulary

The first thing we typically add to our vocabulary are types, which you can loosely see as domains of elements. For this puzzle, we add three types: one for the answers, one for the questions, and one for the students:

    type Answer := {A, B}
    type Question := {1..10}
    type Student := {Mary, Dan, Lisa, Colin}

Using these, we can now define predicates and functions. Let's start simple, and add a function to denote each student's score.

    score: Student -> Int

You can think of a function as a mapping of an input value on an output value, as in the mathematical sense. In this case, score will map each element of type Student on an integer number.

Similarly, we introduce a function to map each (Student, Question) pair on an Answer, and a function to represent the correct answer for each question.

    answered: Student * Question -> Answer
    correct: Question -> Answer

Structure

In the structure, we interpret symbols for which we already know the values. Both answered and score can thusly be interpreted:

    answered := {
        (Mary, 1) -> B,  (Mary, 2) -> B,  ..., (Mary, 10) -> B,
        (Dan, 1) -> B,   (Dan, 2) -> A,   ..., (Dan, 10) -> A,
        (Lisa, 1) -> B,  (Lisa, 2) -> A,  ..., (Lisa, 10) -> A,
        (Colin, 1) -> B, (Colin, 2) -> B, ..., (Colin, 10) -> A,
        }.
    score :> {Mary -> 7, Dan -> 5, Lisa -> 3}.

Note that we use two interpretation operators here: := fully interprets a function, whereas :> partially interprets a symbol. This is important, as Colin's score is not yet fixed, so we cannot fully interpret the symbol.

Theory

For the final part of our solution, we now model the actual logic of the problem. Basically, we want to state that "the score of each student is equal to the number of questions they answered correctly". In IDP-Z3's language, FO(·), we can do so in just one rule:

!s in Student:
    score(s) = #{q in Question: answered(s, q) = correct(q)}.

Some clarification:

• ! is the universal quantifier (∀).
• !s in Student" quantifies over all students, and can be read as "For all s in Student".
• #{t in Type: p(t)} is a count aggregate, which counts the number of elements in a Type for which formula p holds. In this case, we count the number of questions which the student answered correctly.

As score and answered are already interpreted, this formula is in essence a constraint for the value of correct. Because IDP-Z3 is purely declarative, it can reason about the values of any symbol in its KB: it has no notion of "input" or "output" variables.

With our KB finished, we can now have IDP-Z3 reason over it using a multitude of reasoning tasks. For instance, we can generate all possible solutions using its model expand reasoning task:

Model 1
==========
score := {Mary -> 7, Dan -> 5, Lisa -> 3, Colin -> 6}.
correct := {1 -> B, 2 -> B, 3 -> B, 4 -> B, 5 -> A, 6 -> A, 7 -> B, 8 -> A, 9 -> A, 10 -> B}.


Model 2
==========
score := {Mary -> 7, Dan -> 5, Lisa -> 3, Colin -> 6}.
correct := {1 -> A, 2 -> B, 3 -> A, 4 -> B, 5 -> A, 6 -> A, 7 -> B, 8 -> A, 9 -> A, 10 -> B}.


Model 3
==========
score := {Mary -> 7, Dan -> 5, Lisa -> 3, Colin -> 6}.
correct := {1 -> B, 2 -> B, 3 -> A, 4 -> B, 5 -> A, 6 -> A, 7 -> A, 8 -> A, 9 -> A, 10 -> B}.


Model 4
==========
score := {Mary -> 7, Dan -> 5, Lisa -> 3, Colin -> 6}.
correct := {1 -> B, 2 -> B, 3 -> A, 4 -> B, 5 -> A, 6 -> A, 7 -> B, 8 -> B, 9 -> A, 10 -> B}

Interestingly, this shows us that there are actually four possible ways to interpret the correctness. Yet, in each of them, Colin's score will be 6, which is indeed the correct answer to the puzzle. Nifty! :-)

IDP-Z3 actually has a dedicated reasoning task to find out what all possible solutions have in common, which is called propagation. If we were to run that instead, we would get the following:

correct(10) -> B
correct(4) -> B
correct(2) -> B
correct(9) -> A
correct(5) -> A
correct(6) -> A
score(Colin) -> 6
No more consequences.

So indeed, Colin's score is 6 in all possible solutions. Moreover, propagation clearly shows that the correctness of some questions is fixed (e.g., 10, 4, ..) whilst that of other can still vary between solutions (e.g., 1, 3, ...).

That concludes our solution to the puzzle. All in all, quite elegant in my opinion, thanks to IDP-Z3's declarative nature. If you are interested to try it for yourself, you can view, modify and run the solution in our online environment. Eager to learn more about IDP-Z3? Visit our website or our interactive tutorial site.