Number puzzle

Authors: András Salamon, Özgür Akgün

We first show how to solve a classic word addition puzzle, due to Dudeney [Dud24]. This is a small toy example, but already illustrates some interesting features of Conjure.

   SEND
+  MORE
-------
= MONEY

Here each letter represents a numeric digit in an addition, and we are asked to find an assignment of digits to letters so that the number represented by the digits SEND when added to the number represented by MORE yields the number represented by MONEY.

Initial model

We are looking for a mapping (a function) from letters to digits. We can represent the different letters as an enumerated type, with each letter appearing only once.

language Essence 1.3
letting letters be new type enum {S,E,N,D,M,O,R,Y}
find f : function letters --> int(0..9)
such that
                   1000 * f(S) + 100 * f(E) + 10 * f(N) + f(D) +
                   1000 * f(M) + 100 * f(O) + 10 * f(R) + f(E) =
    10000 * f(M) + 1000 * f(O) + 100 * f(N) + 10 * f(E) + f(Y)

Each Essence specification can optionally contain a declaration of which dialect of Essence it is written in. The current version of Essence is 1.3. We leave out this declaration in the remaining examples.

This model is stored in sm1.essence; let’s use Conjure to find the solution:

conjure solve -ac sm1.essence

Unless we specify what to call the solution, it is saved as sm1.solution.

letting f be function(S --> 0, E --> 0, N --> 0, D --> 0, M --> 0, O --> 0, R --> 0, Y --> 0)

This is clearly not what we wanted. We haven’t specified all the constraints in the problem!

Identifying a missing constraint

In these kinds of puzzles, usually we need each letter to map to a different digit: we need an injective function. Let’s replace the line

find f : function letters --> int(0..9)

by

find f : function (injective) letters --> int(0..9)

and save the result in file sm2.essence. Now let’s run Conjure again on the new model:

conjure solve -ac sm2.essence

This time the solution sm2.solution looks more like what we wanted:

letting f be function(S --> 2, E --> 8, N --> 1, D --> 7, M --> 0, O --> 3, R --> 6, Y --> 5)

Final model

There is still something strange with sm2.essence. We usually do not allow a number to begin with a zero digit, but the solution maps M to 0. Let’s add the missing constraints to file sm3.essence:

letting letters be new type enum {S,E,N,D,M,O,R,Y}
find f : function (injective) letters --> int(0..9)
such that
                   1000 * f(S) + 100 * f(E) + 10 * f(N) + f(D) +
                   1000 * f(M) + 100 * f(O) + 10 * f(R) + f(E) =
    10000 * f(M) + 1000 * f(O) + 100 * f(N) + 10 * f(E) + f(Y)

such that f(S) > 0, f(M) > 0

Let’s try again:

conjure solve -ac sm3.essence

This now leads to the solution we expected:

letting f be function(S --> 9, E --> 5, N --> 6, D --> 7, M --> 1, O --> 0, R --> 8, Y --> 2)

Finally, let’s check that there are no more solutions:

conjure solve -ac sm3.essence --number-of-solutions=all

This confirms that there is indeed only one solution. As an exercise, verify that the first two models have multiple solutions, and that the solution given by the third model is among these. (The first has 1155 solutions, the second 25.)