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:
A B model for this puzzle can be found below. The constants and sets of the model are as follows:
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}
Below we will use a more complicated puzzle to illustrate the B model.
The model then contains the following derived constants:
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; LINKS == 1..(MAXBRIDGES*4); 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: nl : nodes --> LINKS & /* number of links */ // coordinates of nodes xc: nodes --> COORD & yc: nodes --> COORD & // possible links: 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: