SEND-MORE-MONEY - Revision history

Michael Leuschel at 16:34, 10 February 2017

2017-02-10T16:34:48Z

← Older revision		Revision as of 16:34, 10 February 2017
Line 67:		Line 67:
	CONSTANTS S,E,N,D, M,O,R, Y		CONSTANTS S,E,N,D, M,O,R, Y
	PROPERTIES		PROPERTIES
	S,E,N,D, M,O,R, Y} <: 0..9 & S >0 & M >0 &		{S,E,N,D, M,O,R, Y} <: 0..9 & S >0 & M >0 &
	card({S,E,N,D, M,O,R, Y}) = 8 &		card({S,E,N,D, M,O,R, Y}) = 8 &
	S1000 + E100 + N*10 + D +		S1000 + E100 + N*10 + D +

Michael Leuschel at 16:34, 10 February 2017

2017-02-10T16:34:08Z

← Older revision		Revision as of 16:34, 10 February 2017
Line 75:		Line 75:
	</pre>		</pre>

	This machine can then be loaded, e.g., into the ProB Tcl/Tk animator, or you can load it from the command-line using:		This machine can then be loaded, e.g., into the ProB Tcl/Tk animator, which should give you a picture like this:


			[[File:ProB_SendMoreMoney_Screenshot.png\|600px\|center]]

			Alternatively you can load the B machine from the command-line using, e.g.:
	probcli SendMoreMoney.mch -init -repl		probcli SendMoreMoney.mch -init -repl
	This command will solve the properties and then start the REPL, where you can query the values of the solutions found.		This command will solve the properties and then start the REPL, where you can query the values of the solutions found.

Michael Leuschel at 16:28, 10 February 2017

2017-02-10T16:28:53Z

← Older revision		Revision as of 16:28, 10 February 2017
Line 61:		Line 61:
	Y = 2		Y = 2

	Another alternative is to wrap the predicate into a full B machine, e.g., as PROPERTIES:		Another alternative is to wrap the predicate into a full B machine, e.g., as PROPERTIES, e.g., into a file <tt>SendMoreMoney.mch</tt> with the following content:

	<pre>		<pre>

Michael Leuschel at 16:28, 10 February 2017

2017-02-10T16:28:09Z

@@ Line 45: / Line 45: @@
   {(((((((9|->5)|->6)|->7)|->1)|->0)|->8)|->2)}
 As you can see, only one solution tuple was found.
 == KISS*KISS = PASSION ==

Michael Leuschel: /* KISSKISS = PASSION /

2017-02-10T16:21:27Z

KISS*KISS = PASSION

← Older revision		Revision as of 16:21, 10 February 2017
Line 48:		Line 48:
	== KISS*KISS = PASSION ==		== KISS*KISS = PASSION ==

	A similar puzzle, this times involving multiplication is the ~~[http://www.cse.unsw.edu.au/~cs4418/2010/Lectures/~~ KISS*KISS=PASSION] puzzle.		A similar puzzle, this times involving multiplication is the KISS*KISS=PASSION puzzle.
	It can be described and solved in a fashion very similar to the problem above:		Here we again have distinct digits K, I, S, P, A, O, N such that the square of KISS equals the decimal number passion.
			The puzzle can be described and solved in a fashion very similar to the problem above:

	>>> {K,P} <: 1..9 & {I,S,A,O,N} <: 0..9 & (1000K+100I+10S+S) (1000K+100I+10S+S) = 1000000P+100000A+10000S+1000S+100I+10*O+N & card({K, I, S, P, A, O, N}) = 7		>>> {K,P} <: 1..9 & {I,S,A,O,N} <: 0..9 & (1000K+100I+10S+S) (1000K+100I+10S+S) = 1000000P+100000A+10000S+1000S+100I+10*O+N & card({K, I, S, P, A, O, N}) = 7

Michael Leuschel: /* KISSKISS = PASSION /

2017-02-10T16:19:05Z

KISS*KISS = PASSION

← Older revision		Revision as of 16:19, 10 February 2017
Line 48:		Line 48:
	== KISS*KISS = PASSION ==		== KISS*KISS = PASSION ==

	A similar puzzle, this times involving multiplication is the KISS*KISS=PASSION puzzle.		A similar puzzle, this times involving multiplication is the [http://www.cse.unsw.edu.au/~cs4418/2010/Lectures/ KISS*KISS=PASSION] puzzle.
	It can be described and solved in a fashion very similar to the problem above:		It can be described and solved in a fashion very similar to the problem above:

Michael Leuschel at 16:16, 10 February 2017

2017-02-10T16:16:08Z

@@ Line 9: / Line 9: @@
   Type ":help" for more information.
   >>>
+Note, you can also use the [[Eval_Console|Eval Console in ProB Tcl/Tk]] or the [[ProB_Logic_Calculator|online Logic Calculator]].
 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
@@ Line 45: / Line 45: @@
   {(((((((9|->5)|->6)|->7)|->1)|->0)|->8)|->2)}
 As you can see, only one solution tuple was found.

Michael Leuschel at 16:11, 10 February 2017

2017-02-10T16:11:04Z

@@ Line 25: / Line 25: @@
         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:
@@ Line 30: / Line 43: @@
   >>> {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)}
+ {(((((((9|->5)|->6)|->7)|->1)|->0)|->8)|->2)}

Michael Leuschel: Created page with "In this entry we study how to solve the famous [https://en.wikipedia.org/wiki/Verbal_arithmetic verbal arithmetic SEND-MORE-MONEY] puzzle. The task is to find the digits S,E,N..."

2017-02-10T16:06:20Z

Created page with "In this entry we study how to solve the famous [https://en.wikipedia.org/wiki/Verbal_arithmetic verbal arithmetic SEND-MORE-MONEY] puzzle. The task is to find the digits S,E,N..."

New page

In this entry we study how to solve the famous [https://en.wikipedia.org/wiki/Verbal_arithmetic 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)}

SEND-MORE-MONEY - Revision history

Michael Leuschel at 16:34, 10 February 2017

Michael Leuschel at 16:34, 10 February 2017

Michael Leuschel at 16:28, 10 February 2017

Michael Leuschel at 16:28, 10 February 2017

Michael Leuschel: /* KISS*KISS = PASSION */

Michael Leuschel: /* KISS*KISS = PASSION */

Michael Leuschel at 16:16, 10 February 2017

Michael Leuschel at 16:11, 10 February 2017

Michael Leuschel: Created page with "In this entry we study how to solve the famous [https://en.wikipedia.org/wiki/Verbal_arithmetic verbal arithmetic SEND-MORE-MONEY] puzzle. The task is to find the digits S,E,N..."

Michael Leuschel: /* KISSKISS = PASSION /

Michael Leuschel: /* KISSKISS = PASSION /