Bridges Puzzle (Hashiwokakero) - Revision history

Michael Leuschel: /* Adding graphical visualization */

2024-01-06T16:50:15Z

Adding graphical visualization

← Older revision		Revision as of 16:50, 6 January 2024
Line 127:		Line 127:
	== Adding graphical visualization ==		== Adding graphical visualization ==

	To show the solution graphically, we can add the following [[~~CUSTOM_GRAPH~~\|custom graph]] to the <tt>DEFINITIONS</tt> clause in the model:		To show the solution graphically, we can add the following [[Custom_Graph\|custom graph]] to the <tt>DEFINITIONS</tt> clause in the model:
	<pre>		<pre>
	CUSTOM_GRAPH_NODES == {n,w,w2\|(n\|->w):nl & w=w2}; // %n1.(n1:nodes\|nl(n1));		CUSTOM_GRAPH_NODES == {n,w,w2\|(n\|->w):nl & w=w2}; // %n1.(n1:nodes\|nl(n1));

2024-01-06T16:46:44Z

Adding graphical visualization

← Older revision		Revision as of 16:46, 6 January 2024
Line 127:		Line 127:
	== Adding graphical visualization ==		== Adding graphical visualization ==

	To show the solution graphically, we can add the following to the <tt>DEFINITIONS</tt> clause in the model:		To show the solution graphically, we can add the following [[CUSTOM_GRAPH\|custom graph]] to the <tt>DEFINITIONS</tt> clause in the model:
	<pre>		<pre>
	CUSTOM_GRAPH_NODES == {n,w,w2\|(n\|->w):nl & w=w2}; // %n1.(n1:nodes\|nl(n1));		CUSTOM_GRAPH_NODES == {n,w,w2\|(n\|->w):nl & w=w2}; // %n1.(n1:nodes\|nl(n1));

2015-12-15T15:01:54Z

← Older revision		Revision as of 15:01, 15 December 2015
Line 44:		Line 44:
	p1i == prj1(nodes,INTEGER)		p1i == prj1(nodes,INTEGER)
	SETS		SETS
	~~// N = {a,b,c,d}~~
	N = {a,b,c,d,e,f,g,h,i,j,k,l,m,n}		N = {a,b,c,d,e,f,g,h,i,j,k,l,m,n}
	CONSTANTS nodes, ignore, nl, xc,yc, plx,ply,pl, cs, sol, connected		CONSTANTS nodes, ignore, nl, xc,yc, plx,ply,pl, cs, sol, connected

2015-12-15T15:01:23Z

Adding graphical visualization

← Older revision		Revision as of 15:01, 15 December 2015
Line 134:		Line 134:
	</pre>		</pre>

	One can then load the model, perform the initialisation (double clicking on <~~pre~~>INITIALISATION</~~pre~~> in the operations pane) and the execute the command "Current State as Custom Graph" in the States sub-menu of the Visualize menu. This leads to the following picture:		One can then load the model, perform the initialisation (double clicking on <tt>INITIALISATION</tt> in the operations pane) and the execute the command "Current State as Custom Graph" in the States sub-menu of the Visualize menu. This leads to the following picture:

	[[File:ProB_BridgesSol.png\|400px\|center]]		[[File:ProB_BridgesSol.png\|400px\|center]]

2015-12-15T15:01:02Z

← Older revision		Revision as of 15:01, 15 December 2015
Line 21:		Line 21:
	ignore = {e,f,g,h,i,j,k,l,m,n}		ignore = {e,f,g,h,i,j,k,l,m,n}
	</pre>		</pre>
			Below we will use a more complicated puzzle to illustrate the B model.

	The model then contains the following derived constants:		The model then contains the following derived constants:

2015-12-15T14:59:26Z

Adding graphical visualization

← Older revision		Revision as of 14:59, 15 December 2015
Line 136:		Line 136:

	[[File:ProB_BridgesSol.png\|400px\|center]]		[[File:ProB_BridgesSol.png\|400px\|center]]

			One can load the Dot file generated by ProB into another tool (e.g., OmniGraffle) and then re-arrange the nodes to obtain the rectangular layout respecting the x- and y-coordinates:


			[[File:ProB_BridgesSolOmni.png\|400px\|center]]

2015-12-15T14:52:13Z

← Older revision		Revision as of 14:52, 15 December 2015
Line 118:		Line 118:

	A solution for this puzzle is found by ProB in 0.08 seconds (on a MacBook Air 2.2GHz i7).		A solution for this puzzle is found by ProB in 0.08 seconds (on a MacBook Air 2.2GHz i7).
			The conflict set is <tt>{((d\|->e),(b\|->g)), ((i\|->j),(h\|->n))}</tt> and the value for sol is
			<pre>
			{((a\|->b)\|->2),((a\|->l)\|->2),((b\|->c)\|->2),((b\|->g)\|->2),((c\|->j)\|->1),
			((d\|->e)\|->0),((d\|->f)\|->1),((e\|->h)\|->2),((f\|->g)\|->2),((f\|->k)\|->1),
			((g\|->h)\|->2),((h\|->n)\|->0),((i\|->j)\|->2),((i\|->m)\|->1),((l\|->m)\|->2),((m\|->n)\|->2)}
			</pre>

	== Adding graphical visualization ==		== Adding graphical visualization ==

2015-12-15T14:47:25Z

← Older revision		Revision as of 14:47, 15 December 2015
Line 113:		Line 113:
	</pre>		</pre>

	A solution for ~~the above Puzzle (in Bridges.png)~~ is found by ProB in 0.08 seconds (on a MacBook Air 2.2GHz i7).		The puzzle encode above can be visualized as follows:

			[[File:ProB_BridgesPuzzle.png\|400px\|center]]

			A solution for this puzzle is found by ProB in 0.08 seconds (on a MacBook Air 2.2GHz i7).

2015-12-15T14:43:26Z

Adding graphical visualization

← Older revision		Revision as of 14:43, 15 December 2015
Line 126:		Line 126:
	One can then load the model, perform the initialisation (double clicking on <pre>INITIALISATION</pre> in the operations pane) and the execute the command "Current State as Custom Graph" in the States sub-menu of the Visualize menu. This leads to the following picture:		One can then load the model, perform the initialisation (double clicking on <pre>INITIALISATION</pre> in the operations pane) and the execute the command "Current State as Custom Graph" in the States sub-menu of the Visualize menu. This leads to the following picture:

	[[File:ProB_BridgesSol.png\|~~600px~~\|center]]		[[File:ProB_BridgesSol.png\|400px\|center]]

2015-12-15T14:43:03Z

Adding graphical visualization

← Older revision		Revision as of 14:43, 15 December 2015
Line 126:		Line 126:
	One can then load the model, perform the initialisation (double clicking on <pre>INITIALISATION</pre> in the operations pane) and the execute the command "Current State as Custom Graph" in the States sub-menu of the Visualize menu. This leads to the following picture:		One can then load the model, perform the initialisation (double clicking on <pre>INITIALISATION</pre> in the operations pane) and the execute the command "Current State as Custom Graph" in the States sub-menu of the Visualize menu. This leads to the following picture:

	[[File:ProB_BridgesSol.~~pdf~~\|600px\|center]]		[[File:ProB_BridgesSol.png\|600px\|center]]