--- First attempt at Hamiltonian Circuit.
--- Two questions:
--- 1. Which graph representation is the best?
--- 2. How to get back home?
--- Graphs:
fmod GRAPH is
sort NodeId . --- application-specific
sort NodeIdSet .
subsort NodeId < NodeIdSet .
op none : -> NodeIdSet [ctor] .
op __ : NodeIdSet NodeIdSet -> NodeIdSet [ctor assoc comm id: none] .
sort Node .
op node:_nbs:_ : NodeId NodeIdSet -> Node [ctor] .
sort Graph . --- multiset of nodes
subsort Node < Graph .
op emptyGraph : -> Graph [ctor] .
op _;_ : Graph Graph -> Graph [ctor assoc comm id: emptyGraph] .
endfm
fmod HAMILTONIAN-CIRCUIT is
including GRAPH .
--- Assume at least three nodes in the graph!!
--- I don't know whether or not a zero/one/two-node graph
--- is defined to have a HC ...
op hamiltonianCircuit : Graph -> Bool .
vars N N1 : NodeId .
vars NBS NBS2 : NodeIdSet .
var NS : Graph .
var NODE : Node .
--- start by picking an arbitrary node N:
eq hamiltonianCircuit((node: N nbs: NBS) ; NS) =
hCircuit(N, NBS, NS) .
op hCircuit : NodeId NodeIdSet Graph -> Bool .
--- hCircuit(startNode, remaining nbs of last node, remainingNodes)
--- should we pick the next neighbor?
eq hCircuit(N, N1 NBS, (node: N1 nbs: NBS2) ; NS)
= --- there is a neighbor N1 of N not yet in the path
hCircuit(N, NBS2, NS) --- try N1 to be the next node in the circuit
or hCircuit(N, NBS, (node: N1 nbs: NBS2) ; NS) . --- or not.
--- cannot pick next neighbor if already in the path:
ceq hCircuit(N, N1 NBS, NODE ; NS) =
hCircuit(N, NBS, NODE ; NS) if not (N1 in NODE ; NS) .
--- still unconnected nodes left, but no remaining edges to them:
eq hCircuit(N, none, NODE ; NS) = false .
--- no remaining nodes to consider; can we get back to the start:
eq hCircuit(N, NBS, emptyGraph) = (N in NBS) .
op _in_ : NodeId NodeIdSet -> Bool .
eq N in none = false .
eq N in N1 NBS = (N == N1) or N in NBS .
op _in_ : NodeId Graph -> Bool .
eq N in ((node: N1 nbs: NBS2) ; NS) = (N == N1) or (N in NS) .
eq N in emptyGraph = false .
ops a b c d e f g h : -> NodeId [ctor] .
ops graph1 graph2 graph3 graph4 graph5 : -> Graph .
eq graph1 = (node: a nbs: b c d) ; (node: b nbs: a d) ; (node: c nbs: a) ; (node: d nbs: a b) . --- no
eq graph2 = (node: a nbs: b c d) ; (node: b nbs: a d) ; (node: c nbs: a d) ; (node: d nbs: a b c) . --- yes
eq graph3 = (node: a nbs: b c) ; (node: b nbs: a c) ; (node: c nbs: a b) ;
(node: d nbs: e f) ; (node: e nbs: d f) ; (node: f nbs: d e) .
eq graph4 = (node: a nbs: b c e) ; (node: b nbs: a f d) ; (node: c nbs: a e) ; --- book
(node: d nbs: b f) ; (node: e nbs: a c f) ; (node: f nbs: b d e) .
eq graph5 = (node: a nbs: c d) ; (node: b nbs: d e) ; (node: c nbs: a d) ; --- butterfly
(node: d nbs: a c b e) ; (node: e nbs: d b) .
endfm
red hamiltonianCircuit(graph1) .
red hamiltonianCircuit(graph2) .
red hamiltonianCircuit(graph3) .
red hamiltonianCircuit(graph4) .
red hamiltonianCircuit(graph5) .