In this entry we study how to solve the famous verbal arithmetic SEND-MORE-MONEY puzzle. The task is to find the digits S,E,N,D,M,O,R,Y such that the addition of SEND to MORE leads the decimal number MONEY. There are various ways to solve this problem in B using ProB. The quickest is probably to fire up the probcli REPL and then type the problem into the console. To start up the REPL type the following into your shell or terminal:
probcli -repl
This should give you the following output:
ProB Interactive Expression and Predicate Evaluator Type ":help" for more information. >>>
We can now encode the puzzle as a predicate as follows:
>>> {S,E,N,D, M,O,R, Y} <: 0..9 & S>0 & M>0 & card({S,E,N,D, M,O,R, Y})=8 & S*1000 + E*100 + N*10 + D + M*1000 + O*100 + R*10 + E = M*10000 + O*1000 + N*100 + E*10 + Y
After hitting return, ProB will output the following immediately:
Existentially Quantified Predicate over S,E,N,D,M,O,R,Y is TRUE
Solution:
S = 9 &
E = 5 &
N = 6 &
D = 7 &
M = 1 &
O = 0 &
R = 8 &
Y = 2
We are still not sure if this is the only solution. One way to ensure this is to compute a set comprehension with all solutions:
>>> {S,E,N,D,M,O,R,Y|{S,E,N,D, M,O,R, Y} <: 0..9 & S>0 & M>0 & card({S,E,N,D, M,O,R, Y})=8 & S*1000 + E*100 + N*10 + D + M*1000 + O*100 + R*10 + E = M*10000 + O*1000 + N*100 + E*10 + Y}
Expression Value =
{(((((((9|->5)|->6)|->7)|->1)|->0)|->8)|->2)}