Fun with Alloy Model Checker

I'm trying to learn how to use and leverage the Alloy model checker in my day job and side projects but there doesn't seem to be much material in the way of basic examples for beginners. So to fill in those gaps here's the classic SEND + MORE = MONEY cryptarithmetic puzzle expressed as an Alloy model.

First we need to specify the objects we will be working with

// Non-negative numbers
abstract sig Num { val: Int } { val >= 0 && val <= 9 }

// Digits in SEND + MORE = MONEY
one sig S, E, N, D, M, O, R, Y extends Num { }

The objects we are working with are digits so we enumerate the digits and specify that there is only one instance of each digit ( one sig ... ). We also specify that the value of each digit must be between 0 and 9 ( ... { val >= 0 && val <= 9 } ).

Next we specify a basic fact about the digits all being different

// Digits must all be different
fact {
  all m, n : Num | m != n => n.val != m.val
}

There are also predicates and functions and we will get to those shortly. If we translate the above into plain english then we get the following statement: for every m and n that are numbers if m does not equal n then m and n must have different values.

That's pretty much it for the statement of the problem. Next we have to translate the constraint SEND + MORE = MONEY into actual facts. To do that I'm going to define a function so that I don't have to type as much when expressing the constraints

// Function for computing the sum and the carry at the same time
fun sumCarry(a: Num, b: Num): (Int -> Int) {
  let summand = a.val + b.val |
    summand -> (summand > 9 => 1 else 0)
}

The syntax is a little weird if you are used to programming languages using -> as a way to specify function types but in Alloy -> means tuple. So in the above function we are computing the sum and carry and then returning it as a tuple. In more programmer friendly notation the above function could be written in pseudo code as

function sumCarry(a, b): (Int, Int) {
  return (a + b, (a + b > 9) ? 1 : 0)
}

Now we express the constraints of the puzzle

// Constraints for SEND + MORE = MONEY
fact {
  M.val > 0
  let YSumCarry = sumCarry[D, E], 
    ESumCarry = sumCarry[N, R],
    NSumCarry = sumCarry[E, O],
    OSumCarry = sumCarry[S, M] |
    Y.val = rem[YSumCarry.univ, 10] &&
    E.val = rem[ESumCarry.univ + univ.YSumCarry, 10] &&
    N.val = rem[NSumCarry.univ + univ.ESumCarry, 10] &&
    O.val = rem[OSumCarry.univ + univ.NSumCarry, 10] &&
    M.val = univ.OSumCarry
}

It's a little bit long but hopefully it should be obvious what is going on. We express the constraints of the sum in terms of the digits and then we specify what the values of the digits should be in terms of the sums and carries. Sit with it for a bit and it will make sense. It took me a while to understand why this works and if you are used to thinking imperatively then meditating on the above will help rewire your neurons to think more declaratively. It might help to try to translate the constraint into english. Here is a hint: it is the basic algorithm for doing sums that everyone learns in grade school.

The one part I probably have to explain is univ.A and A.univ syntax. Our sumCarry functions returns a tuple of (sum, carry) and we want to extract the first and second components of that tuple. Alloy has a weird way of expressing that using univ which is the set of all atoms and is a keyword built into the language so it can't be reduced to other primitives in the language. By joining the universal set with our tuple we get the first and second components of the tuple we got from the function. The first component is A.univ because joins in Alloy throw away the element being joined, i.e. (a, b).(b, c) == (a, c) , and if the tuple only had 2 elements to begin with then joining with univ leaves us with 1 element. By symmetry the the second element is univ.A .

Everything up until this point has been setting up the constraints and in order to get a solution we must "run" the model for a predicate so we are going to use an empty predicate which from what I gathered is usually called "show"

pred show { }
run show for 5 Int

Again some more weird syntax here. That 5 in front of Int specifies the bit width which is another way of saying our signed integers have 5 bits (think about why 4 bits would not be enough when working with signed integers).

So everything all together now

// SEND + MORE = MONEY

// Non-negative numbers
abstract sig Num { val: Int } { val >= 0 && val <= 9 }

// Digits
one sig S, E, N, D, M, O, R, Y extends Num { }

// Digits must all be different and in 0..9
fact {
  all m, n : Num | m != n => n.val != m.val
}

// Function for computing the sum and the carry at the same time
fun sumCarry(a: Num, b: Num): (Int -> Int) {
  let summand = a.val + b.val |
    summand -> (summand > 9 => 1 else 0)
}

// Constraints for SEND + MORE = MONEY
fact {
  M.val > 0
  let YSumCarry = sumCarry[D, E], 
    ESumCarry = sumCarry[N, R],
    NSumCarry = sumCarry[E, O],
    OSumCarry = sumCarry[S, M] |
    Y.val = rem[YSumCarry.univ, 10] &&
    E.val = rem[ESumCarry.univ + univ.YSumCarry, 10] &&
    N.val = rem[NSumCarry.univ + univ.ESumCarry, 10] &&
    O.val = rem[OSumCarry.univ + univ.NSumCarry, 10] &&
    M.val = univ.OSumCarry
}

pred show { }

run show for 5 Int

Running the example and getting the solution is left as an exercise for the reader.