***
*** Graph m-coloring and hamiltonian cycle problems,
*** using the generic backtracking algorithm.
***

sload backtracking

fmod GRAPHS is
	pr NAT .

	*** Edge (unordered pairs of naturals)
	sort Edge .

	op p : Nat Nat -> Edge [ctor comm] .

	*** Adjacency set
	sort Adjacency .
	subsort Edge < Adjacency .

	op nil : -> Adjacency [ctor] .
	op __ : Adjacency Adjacency -> Adjacency [ctor assoc comm id: nil] .


	var  E   : Edge .
	var  As  : Adjacency .
	vars K L : Nat .

	*** Adjacency is a set
	eq E E = E .

	*** Are two vertices neighbors?
	op neighbor : Nat Nat Adjacency -> Bool .

	eq neighbor(K, L, p(K, L) As) = true .
	eq neighbor(K, L, As) = false [owise] .
endfm


***
***	m-coloring problem

mod COLORING is
	pr GRAPHS .
	pr NAT-LIST .
	pr EXT-BOOL .

	*** A graph with its coloring
	sort Graph .

	*** The number of vertices, the number of colors available,
	*** the adjacency set and the vertex coloring list
	op graph		: Nat Nat Adjacency NatList -> Graph [ctor] .
	op numColors		: Graph -> Nat .
	op alreadyColored	: Graph -> Nat .

	eq numColors(graph(N, M, As, Cs)) = M .
	eq alreadyColored(graph(N, M, As, Cs)) = size(Cs) .


	vars N M K K' C C' : Nat .
	var As             : Adjacency .
	var Cs             : NatList .
	var G              : Graph .

	op isSolution 		: Graph -> Bool .
	op isOk			: Graph -> Bool .


	*** The color is admissible for the vertex K
	op admissibleColor	: Nat Nat Graph -> Bool .
	op admissibleColor	: Nat Nat Adjacency Nat NatList -> Bool .

	eq isSolution(graph(N, M, As, Cs)) = N == size(Cs) .
	eq isOk(G) = true .

	eq admissibleColor(C, K, graph(N, M, As, Cs)) = admissibleColor(C, K, As, 0, Cs) .
	eq admissibleColor(C, K, As, K', nil) = true .
	eq admissibleColor(C, K, As, K', C' Cs) = (C =/= C' or not neighbor(K, K', As))
		and-then admissibleColor(C, K, As, s(K'), Cs) .

	rl [next] : graph(N, M, As, Cs) => graph(N, M, As, Cs C) [nonexec] .
endm

smod COLORING-STRAT is
	pr COLORING .

	strat expand @ Graph .
	strat expand : Nat @ Graph .

	sd expand := expand(0) .

	var C : Nat .
	var G : Graph .

	sd expand(C) :=
		match G s.t. admissibleColor(C, alreadyColored(G), G) ; next[C <- C]
		| match G s.t. s(C) < numColors(G) ; expand(s(C)) .
endsm

view ColoringBT from BT-ELEMS to COLORING-STRAT is
	sort State to Graph .

	strat expand to expand .
endv

smod COLORING-BT-STRAT is
	including BT-STRAT{ColoringBT} .
endsm


***
***	Hamiltonian cycle

mod HAMILTONIAN is
	pr GRAPHS .
	pr NAT-LIST .

	*** A graph with a cycle
	sort Graph .

	*** The number of vertices, the adjacency list, and the path
	op graph		: Nat Adjacency NatList -> Graph [ctor] .


	vars N M V K : Nat .
	var  As      : Adjacency .
	vars P Q R   : NatList .

	op isSolution 		: Graph -> Bool .
	op isOk			: Graph -> Bool .

	eq isSolution(graph(N, As, V P V)) = N == size(V P) .
	eq isSolution(G:Graph) = false [owise] .

	*** Has the path a cycle?
	op noCross		: NatList -> Bool .

	eq noCross(P K Q K R) = false .
	eq noCross(P) = true [owise] .

	eq isOk(graph(N, As, V P V)) = noCross(V P) .
	eq isOk(graph(N, As, P)) = noCross(P) [owise] .

	rl [next] : graph(N, p(V, K) As, P V) => graph(N, As, P V K) .
endm

view HamiltonianBT from BT-ELEMS to HAMILTONIAN is
	sort State to Graph .

	strat expand to expr next .
endv

smod HAMILTONIAN-BT-STRAT is
	including BT-STRAT{HamiltonianBT} .
endsm

eof

*** For coloring
srew in COLORING-BT-STRAT :
	graph(10, 3, p(0, 1) p(0, 4) p(0, 5) p(1, 2) p(1, 6)
	p(2, 3) p(2, 7) p(3, 4) p(3, 8) p(4, 9)
	p(5, 7) p(5, 8) p(6, 8) p(6, 9) p(7, 9), nil) using solve .

*** For Hamiltonian cycles
srew in HAMILTONIAN-BT-STRAT :
	graph(5, p(0, 1) p(0, 2) p(0, 3) p(0, 4)
	p(1, 2) p(3, 4), 1) using solve .

srew graph(3, p(0, 1) p(1, 2) p(2, 0), 0) using solve .