Rush Hour Puzzle - Revision history

David Geleßus: Update Wikipedia link

2021-02-03T13:53:49Z

Update Wikipedia link

← Older revision		Revision as of 13:53, 3 February 2021
Line 1:		Line 1:
	== B Encoding of the Rush Hour Puzzle ==		== B Encoding of the Rush Hour Puzzle ==

	This case studies tackles encoding the [~~http~~://en.wikipedia.org/wiki/Rush_Hour_(~~board_game~~) rush hour board game] in which cars are packed on a 6-by-6 grid and can either move horizontally or vertically. The goal is to move the red car to the exit. In this particular instance we try to solve the [http://www.puzzles.com/products/RushHour/RHfromMarkRiedel/Jam.html?40 hardest puzzle of the original game Nr. 40].		This case studies tackles encoding the [https://en.wikipedia.org/wiki/Rush_Hour_(puzzle) rush hour board game] in which cars are packed on a 6-by-6 grid and can either move horizontally or vertically. The goal is to move the red car to the exit. In this particular instance we try to solve the [http://www.puzzles.com/products/RushHour/RHfromMarkRiedel/Jam.html?40 hardest puzzle of the original game Nr. 40].

	Inspired by discussions with Neng-Fa Zhou at ICLP'14 in Vienna, we now have a new version of the B model for this puzzle.		Inspired by discussions with Neng-Fa Zhou at ICLP'14 in Vienna, we now have a new version of the B model for this puzzle.

Michael Leuschel: /* B Encoding of the Rush Hour Puzzle */

2014-08-05T08:07:54Z

B Encoding of the Rush Hour Puzzle

← Older revision		Revision as of 08:07, 5 August 2014
Line 6:		Line 6:

	The old version can still be found below.		The old version can still be found below.
	There is also a Prolog [[Other_languages\|XTL]] encoding of the [[Rush_Hour_XTL\|same problem available]]~~. Here~~ ProB finds the example in one second or less.		There is also a Prolog [[Other_languages\|XTL]] encoding of the [[Rush_Hour_XTL\|same problem available]], where ProB finds the example in one second or less.
	Explanations and comparison with the [http://picat-lang.org/exs/prob_rushhour.pi Picat solution] will follow soon.		Explanations and comparison with the [http://picat-lang.org/exs/prob_rushhour.pi Picat solution] will follow soon.

Michael Leuschel: /* B Encoding of the Rush Hour Puzzle */

2014-08-05T08:07:29Z

B Encoding of the Rush Hour Puzzle

← Older revision		Revision as of 08:07, 5 August 2014
Line 6:		Line 6:

	The old version can still be found below.		The old version can still be found below.
	There is also a [[Other_languages\|~~Prolog~~ XTL ~~encoding~~]] of the [[Rush_Hour_XTL\|same problem available]]. Here ProB finds the example in one second.		There is also a Prolog [[Other_languages\|XTL]] encoding of the [[Rush_Hour_XTL\|same problem available]]. Here ProB finds the example in one second or less.
	Explanations and comparison with the [http://picat-lang.org/exs/prob_rushhour.pi Picat solution] will follow soon.		Explanations and comparison with the [http://picat-lang.org/exs/prob_rushhour.pi Picat solution] will follow soon.

Line 263:		Line 263:
	Result: NoError		Result: NoError
	</pre>		</pre>


	== Old Solution ==		== Old Solution ==

Michael Leuschel at 08:05, 5 August 2014

2014-08-05T08:05:07Z

← Older revision		Revision as of 08:05, 5 August 2014
Line 1:		Line 1:
			== B Encoding of the Rush Hour Puzzle ==

	This case studies tackles encoding the [http://en.wikipedia.org/wiki/Rush_Hour_(board_game) rush hour board game] in which cars are packed on a 6-by-6 grid and can either move horizontally or vertically. The goal is to move the red car to the exit. In this particular instance we try to solve the [http://www.puzzles.com/products/RushHour/RHfromMarkRiedel/Jam.html?40 hardest puzzle of the original game Nr. 40].		This case studies tackles encoding the [http://en.wikipedia.org/wiki/Rush_Hour_(board_game) rush hour board game] in which cars are packed on a 6-by-6 grid and can either move horizontally or vertically. The goal is to move the red car to the exit. In this particular instance we try to solve the [http://www.puzzles.com/products/RushHour/RHfromMarkRiedel/Jam.html?40 hardest puzzle of the original game Nr. 40].

Line 79:		Line 81:
	END		END
	</pre>		</pre>

			=== Finding a Solution with ProB ===

	To find a solution you need to run the ProB [[Consistency Checking\|"Model Check" command]] in the "Verify" menu. Be sure to enable the "Find GOAL (from DEFINITIONS)" checkbox, as above we have specified the target state <tt>col(red) = 4</tt> inside the <tt>GOAL</tt> definition.		To find a solution you need to run the ProB [[Consistency Checking\|"Model Check" command]] in the "Verify" menu. Be sure to enable the "Find GOAL (from DEFINITIONS)" checkbox, as above we have specified the target state <tt>col(red) = 4</tt> inside the <tt>GOAL</tt> definition.
Line 88:		Line 92:
	[[File:ProB_RushHour_v2_Screenshot.png\|600px\|center]]		[[File:ProB_RushHour_v2_Screenshot.png\|600px\|center]]

	=== Exporting ~~the~~ Solution Trace ===		=== Exporting a Solution Trace ===

	You can inspect or export the solution trace found by ProB in various ways:		You can inspect or export the solution trace found by ProB in various ways:

Michael Leuschel at 08:04, 5 August 2014

2014-08-05T08:04:01Z

← Older revision		Revision as of 08:04, 5 August 2014
Line 88:		Line 88:
	[[File:ProB_RushHour_v2_Screenshot.png\|600px\|center]]		[[File:ProB_RushHour_v2_Screenshot.png\|600px\|center]]

	You can also find the solution from the command line using [[Using_the_Command-Line_Version_of_ProB\|probcli]]: <tt>probcli -mc 10000 RushHour.mch</tt>.		=== Exporting the Solution Trace ===

			You can inspect or export the solution trace found by ProB in various ways:
			* using the command "History to Current State" in the "Traces" submenu of the "Visualize" menu
			* using various commands in the "Trace Checking" submenu of the "Verify" menu, e.g.:
			** "Save History to Trace File": this generates a Prolog trace file that can be replayed later using the "Check Trace from Trace File" command
			** "Save History to B File...": this saves the trace in B format and it can be parsed by a B parser

			Note: you can also find the solution from the command line using [[Using_the_Command-Line_Version_of_ProB\|probcli]]: <tt>probcli -mc 10000 RushHour.mch</tt>. The command line version probcli will output the trace on the console, but also provides various commands to save the history to file.

	=== Finding the shortest solution using the TLC backend ===		=== Finding the shortest solution using the TLC backend ===

Michael Leuschel at 07:56, 5 August 2014

2014-08-05T07:56:12Z

← Older revision		Revision as of 07:56, 5 August 2014
Line 87:		Line 87:

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

			You can also find the solution from the command line using [[Using_the_Command-Line_Version_of_ProB\|probcli]]: <tt>probcli -mc 10000 RushHour.mch</tt>.

	=== Finding the shortest solution using the TLC backend ===		=== Finding the shortest solution using the TLC backend ===

			If you want to find the shortest solution with ProB you should set the "Search Strategy" in the ProB [[Consistency Checking\|"Model Check" command]] to "Breadth First".
	The shortest solution has 81 moves (if one allows a car to move multiple spaces in one move then the shortest solution has 51 moves).		The shortest solution has 81 moves (if one allows a car to move multiple spaces in one move then the shortest solution has 51 moves).

			You can also use ou
	It was found in 3 seconds (about 1 second model checking time) using our [[TLC\|TLC model checking backend]] on a Mac Book Air 1.7 GHz i7:		It was found in 3 seconds (about 1 second model checking time) using our [[TLC\|TLC model checking backend]] on a Mac Book Air 1.7 GHz i7:

Michael Leuschel at 07:51, 5 August 2014

2014-08-05T07:51:20Z

← Older revision		Revision as of 07:51, 5 August 2014
Line 7:		Line 7:
	Explanations and comparison with the [http://picat-lang.org/exs/prob_rushhour.pi Picat solution] will follow soon.		Explanations and comparison with the [http://picat-lang.org/exs/prob_rushhour.pi Picat solution] will follow soon.

	~~The~~ shortest solution can be found very quickly using our new feature to use [[TLC\|TLC for model checking B specifications]] (about 1 second model checking time; rest of time needed to replay counter example).		As we show below, the shortest solution can be found very quickly using our new feature to use [[TLC\|TLC for model checking B specifications]] (about 1 second model checking time; rest of time needed to replay counter example).

			First, here is the B model of the Rush Hour puzzle:

	<pre>		<pre>
Line 77:		Line 79:
	END		END
	</pre>		</pre>

			To find a solution you need to run the ProB [[Consistency Checking\|"Model Check" command]] in the "Verify" menu. Be sure to enable the "Find GOAL (from DEFINITIONS)" checkbox, as above we have specified the target state <tt>col(red) = 4</tt> inside the <tt>GOAL</tt> definition.

	Here is a screenshot of ProB after finding the shortest solution using model checking.		Here is a screenshot of ProB after finding the shortest solution using model checking.
Line 84:		Line 88:
	[[File:ProB_RushHour_v2_Screenshot.png\|600px\|center]]		[[File:ProB_RushHour_v2_Screenshot.png\|600px\|center]]

			=== Finding the shortest solution using the TLC backend ===

	The shortest solution has 81 moves (if one allows a car to move multiple spaces in one move then the shortest solution has 51 moves).		The shortest solution has 81 moves (if one allows a car to move multiple spaces in one move then the shortest solution has 51 moves).

Michael Leuschel at 10:37, 23 July 2014

2014-07-23T10:37:14Z

← Older revision		Revision as of 10:37, 23 July 2014
Line 1:		Line 1:
	This case studies tackles encoding the [http://en.wikipedia.org/wiki/Rush_Hour_(board_game) rush hour board game] in which cars are packed on a 6-by-6 grid and can either move horizontally or vertically. The goal is to move the red car to the exit. In this particular instance we try to solve the [http://www.puzzles.com/products/RushHour/RHfromMarkRiedel/Jam.html?40 hardest puzzle Nr 40].		This case studies tackles encoding the [http://en.wikipedia.org/wiki/Rush_Hour_(board_game) rush hour board game] in which cars are packed on a 6-by-6 grid and can either move horizontally or vertically. The goal is to move the red car to the exit. In this particular instance we try to solve the [http://www.puzzles.com/products/RushHour/RHfromMarkRiedel/Jam.html?40 hardest puzzle of the original game Nr. 40].

	Inspired by discussions with Neng-Fa Zhou at ICLP'14 in Vienna, we now have a new version of the B model for this puzzle.		Inspired by discussions with Neng-Fa Zhou at ICLP'14 in Vienna, we now have a new version of the B model for this puzzle.

Michael Leuschel at 10:29, 23 July 2014

2014-07-23T10:29:43Z

@@ Line 213: / Line 213: @@
 UNCOVERED_OPERATIONS
 </pre>
 == Old Solution ==

Michael Leuschel at 10:22, 23 July 2014

2014-07-23T10:22:56Z

@@ Line 190: / Line 190: @@
 mv_down(11,(5|->5));
 mv_right(13,(2|->5))
 </pre>