• Special Pages
• User

Help

# Bridges Puzzle (Hashiwokakero): Difference between revisions

The Hashiwokakero Puzzle is a logical puzzle where one has to build bridges between islands. The puzzle is also known under the name Ai-Ki-Ai. The puzzles can also be played online.

The requirements for this puzzle are as follows:

• the goal is to build bridges between islands so as to generate a connected graph
• every island has a number on it, indicating exactly how many bridges should be linked with the island
• there is an upper bound (MAXBRIDGES) on the number of bridges that can be built-between two islands
• bridges cannot cross each other

A B model for this puzzle can be found below. The constants and sets of the model are as follows:

• N are the nodes (islands); we have added a constant ignore where one can stipulate which islands should be ignored in this puzzle
• nl (number of links) stipulates for each island how many bridges it should be linked with
• xc, yc are the x- and y-coordinates for every island

A simple puzzle with four islands would be defined as follows, assuming the basic set N is defined as N = {a,b,c,d,e,f,g,h,i,j,k,l,m,n}:

``` xc(a)=0 & xc(b)=1 & xc(c)=0 & xc(d) = 1 &
yc(a)=0 & yc(b)=0 & yc(c)=1 & yc(d) = 1 &
nl = {a|->2, b|->2, c|->2, d|->2} &
ignore = {e,f,g,h,i,j,k,l,m,n}
```

The model then contains the following derived constants:

• plx,ply: the possible links between islands on the x- and y-axis respectively
• pl: the possible links both on the x- and y-axis combined
• cs: the conflict set of links which overlap, i.e., one cannot build bridges on both links (a,b) when the pair (a,b) is in cs
• connected: the set of links on which at least one bridge was built

The model also sets up the goal constant sol which maps every link in pl to a number indicating how many bridges are built on it. The model also stipulates that the graph set up by connected generates a fully connected graph.

Here is the full model:

```MACHINE Bridges
DEFINITIONS
MAXBRIDGES==2;
COORD == 0..10;
p1 == prj1(nodes,nodes);
p2 == prj2(nodes,nodes);
p1i == prj1(nodes,INTEGER)
SETS
// N = {a,b,c,d}
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
PROPERTIES
nodes = N \ ignore &
// target number of links per node:

// coordinates of nodes
xc: nodes --> COORD & yc: nodes --> COORD &

pl : nodes <-> nodes &
plx : nodes <-> nodes &
ply : nodes <-> nodes &

plx = {n1,n2 | xc(n1)=xc(n2) & n1 /= n2 & yc(n2)>yc(n1) &
!n3.(xc(n3)=xc(n1) => yc(n3) /: yc(n1)+1..yc(n2)-1) } &
ply =  {n1,n2 | yc(n1)=yc(n2) & n1 /= n2 & xc(n2)>xc(n1) &
!n3.(yc(n3)=yc(n1) => xc(n3) /: xc(n1)+1..xc(n2)-1)} &
pl = plx \/ ply

&
// compute conflict set (assumes xc,yc coordinates ordered in plx,ply)
cs = {pl1,pl2 | pl1:plx & pl2:ply &
xc(p1(pl1)): xc(p1(pl2))+1..xc(p2(pl2))-1 &
yc(p1(pl2)): yc(p1(pl1))+1..yc(p2(pl1))-1}
&

sol : pl --> 0..MAXBRIDGES &
!nn.(nn:nodes => SIGMA(l).(l:pl &
(p1(l)=nn or p2(l)=nn)|sol(l))=nl(nn)) &

!(pl1,pl2).( (pl1,pl2):cs => sol(pl1)=0 or sol(pl2)=0) // no conflicts
&

// check graph connected
connected = {pl|sol(pl)>0} &
closure1(connected \/ connected~)[{a}] = {nn|nn:nodes & nl(nn)>0}

// encoding of puzzle
&

// A puzzle from bridges.png

xc(a)=1 & yc(a)=1 & nl(a)=4 &
xc(b)=1 & yc(b)=4 & nl(b)=6 &
xc(c)=1 & yc(c)=6 & nl(c)=3 &

xc(d)=2 & yc(d)=2 & nl(d)=1 &
xc(e)=2 & yc(e)=5 & nl(e)=2 &

xc(f)=3 & yc(f)=2 & nl(f)=4 &
xc(g)=3 & yc(g)=4 & nl(g)=6 &
xc(h)=3 & yc(h)=5 & nl(h)=4 &

xc(i)=4 & yc(i)=3 & nl(i)=3 &
xc(j)=4 & yc(j)=6 & nl(j)=3 &

xc(k)=5 & yc(k)=2 & nl(k)=1 &

xc(l)=6 & yc(l)=1 & nl(l)=4 &
xc(m)=6 & yc(m)=3 & nl(m)=5 &
xc(n)=6 & yc(n)=5 & nl(n)=2 &
ignore = {}

END
```

The puzzle encode above can be visualized as follows:

A solution for this puzzle is found by ProB in 0.08 seconds (on a MacBook Air 2.2GHz i7). The conflict set is {((d|->e),(b|->g)), ((i|->j),(h|->n))} and the value for sol is

```{((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)}
```

To show the solution graphically, we can add the following to the DEFINITIONS clause in the model:

``` CUSTOM_GRAPH_NODES == {n,w,w2|(n|->w):nl & w=w2}; // %n1.(n1:nodes|nl(n1));
CUSTOM_GRAPH_EDGES == {n1,w,n2|n1:nl & n2:nl &  (p1i(n1),p1i(n2),w):sol}
```

One can then load the model, perform the initialisation (double clicking on

`INITIALISATION`

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 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: