Zoom Tracks

Problem posted to comp.lang.prolog by Paul Nothman: “This problem was recently in a Mathematics competition. Although I completed it through logic and mathematics, without the aid of a computer, I'm wondering if and how it could be answered using prolog.”

Problem Statement

The problem is as follows:

World theme park has seven attractions which are so far apart that there needs to be a network of monorails, called zoomtracks, to transport the patrons between attractions. There is exactly one zoomtrack between each pair of attractions. Each zoomtrack can only transport patrons in one direction. The network is constructed so that two friends can always meet at a third attraction after exactly one trip each from any two attractions.

Hint: Each attraction leads to and is led to by 3 other attractions. There are 21 zoomtracks altogether.

Find the entire configuration of the theme park given the following:

(The first letter of each line is the attraction from which the zoomtrack comes and the one beside it is where the zoomtrack leads to).

SU SO ST UO UN UP OT ON NP TU

Solution Overview

An interesting aspect of this puzzle is the given partial solution. What is its purpose? Is it supposed to help or hinder?

In fact, the partial solution allows relatively naive methods to find the right answer in reasonable time.

However, I've chosen to implement a method that is not dependent on the partial solution. The key to this approach is the generation of the stations data-structures, which may be partially instantiated with the given solution, before the search for a complete solution begins.

The requirements of the problem are that each attraction will have three destinations that can be reached by a single zoomtrack, and that every pair of attractions must have a destination in common.

This solution uses the insight that every pair of attractions must have exactly one destination in common.

zoom

finds a solution and then prints it.

zoom :-
    zoom_tracks( ZoomTracks ),
    print_zoom_tracks( ZoomTracks ).

zoom_tracks( ?ZoomTracks )

holds when ZoomTracks is a set of Attraction × Links × Destinations tuples, describing a valid configuration of zoomtracks, such that each pair of attractions has exactly one destination in common. The predicate network/2 always generates viable solutions, but a simple assertion is used to demonstrate that the solution is valid directly.

zoom_tracks( ZoomTracks ) :-
    station_origin( Station, Attraction ),
    station_destinations( Station, Destinations ),
    length( Destinations, 3 ),
    findall( Station, attraction( Attraction ), ZoomTracks ),
    findall( [Dest,Dest,Dest], attraction( Dest ), PossibleDestinations ),
    unified_zoomtracks( ZoomTracks ),
    connections( ZoomTracks ),
    network( ZoomTracks, PossibleDestinations ),
    forall(
        pair_of_stations( ZoomTracks, Station1, Station2 ),
        friends_can_meet( Station1, Station2 )
        ).

unified_zoomtracks( +ZoomTracks )

holds when ZoomTracks is a set of Attraction × Links × Destinations tuples such that each link between two Attractions is represented by a variable shared between the two attractions. In each tuple, the Link variable denoting the Attraction is bound to 'self'.

unified_zoomtracks( ZoomTracks ) :-
    station_origin( First, Attraction1 ),
    station_origin( Second, Attraction2 ),
    findall(
        Attraction1-Attraction2,
        pair_of_stations(ZoomTracks, First, Second),
        Linkage
        ),
    unified_links( Linkage, ZoomTracks ).

unified_links( +Linkage, +ZoomTracks )

holds when Linkage is a list of Attraction1-Attraction2 pairs such that in ZoomTracks:

• The link variables denoting Attraction1 for Attraction2 and vice versa are unified.
• The link variables denoting Attraction1 for Attraction1 and Attraction2 for Attraction2 are bound to 'self'.

unified_links( [], _ZoomTracks ).
unified_links( [First-Second|Linkage], ZoomTracks ) :-
    station_origin( Station1, First ),
    station_links( Station1, Links1 ),
    station_origin( Station2, Second ),
    station_links( Station2, Links2 ),
    memberchk( Station1, ZoomTracks ),
    memberchk( Station2, ZoomTracks ),
    link_receiver( First, Links2, Receiver ),
    link_receiver( Second, Links1, Receiver ),
    link_receiver( First, Links1, self ),
    link_receiver( Second, Links2, self ),
    unified_links( Linkage, ZoomTracks ).

connections( ?ZoomTracks )

holds when the given connections have been applied to ZoomTracks.

Note that this can be made vacuous without any significant effect on performance.

connections( ZoomTracks ) :-
    connection( s, u, ZoomTracks ),
    connection( s, o, ZoomTracks ),
    connection( s, t, ZoomTracks ),
    connection( u, o, ZoomTracks ),
    connection( u, n, ZoomTracks ),
    connection( u, p, ZoomTracks ),
    connection( o, t, ZoomTracks ),
    connection( o, n, ZoomTracks ),
    connection( n, p, ZoomTracks ),
    connection( t, u, ZoomTracks ).

connection( +Source, +Destination, +ZoomTracks )

holds when ZoomTracks contains a connection from Source to Destination.

connection( From, To, ZoomTracks ) :-
    station_origin( Station, From ),
    station_links( Station, Links ),
    station_destinations( Station, Destinations ),
    memberchk( Station, ZoomTracks ),
    memberchk( To, Destinations ),
    link_receiver( To, Links, To ).

pair_of_stations( +ZoomTracks, ?Station1, ?Station2 )

holds when Station1 and Station2 are distinct elements of ZoomTracks, avoiding redundant solutions.

pair_of_stations( [Station1|ZoomTracks], Station1, Station2 ) :-
    member( Station2, ZoomTracks ).
pair_of_stations( [_Station0|ZoomTracks], Station1, Station2 ) :-
    pair_of_stations( ZoomTracks, Station1, Station2 ).

friends_can_meet( +Station1, +Station2 )

holds when Station1 and Station2 have a common destination.

friends_can_meet( Station1, Station2 ) :-
    station_destinations( Station1, Destinations1 ),
    station_destinations( Station2, Destinations2 ),
    member( MeetingPoint, Destinations1 ),
    member( MeetingPoint, Destinations2 ).

network( +ZoomTracks, ?Destinations )

holds when ZoomTracks is a set of Attraction → Destinations pairs describing a valid configuration of zoomtracks, such that each pair of attractions has exactly one destination in common. Destinations define the range of ZoomTracks.

network( ZoomTracks, Destinations ) :-
    network1( ZoomTracks, Destinations, [] ).

network1( [], Destinations, _Stations ) :-
    forall( member( Empty, Destinations ), Empty == [] ).
network1( [Station|Stations], Destinations, Assigned ) :-
    destination_assignment( Station, Destinations, Destinations1 ),
    properly_connected( Station, Assigned ),
    network1( Stations, Destinations1, [Station|Assigned] ).

destination_assignment( +Station, +Destinations, ?Destinations1 )

holds when Destinations1 is the difference of Destinations and the destinations of Station, which must not contain the origin of Station.

destination_assignment( Station, Destinations0, Destinations1 ) :-
    station_destinations( Station, Destinations ),
    station_links( Station, Links ),
    matching( Destinations, Links, Destinations0, Destinations1 ).

matching( +Destinations0, +Links, +Destinations1, ?Destinations2 )

holds when Destinations2 is the difference of Destinations0 and Destinations1, and the Links variables corresponding to Destinations0 are instantiated.

matching( [], _Links, Destinations, Destinations ).
matching( [Destination|Destinations], Links, Destinations0,
        [Rest|Destinations1] ) :-
    select( [Destination|Rest], Destinations0, Destinations2 ),
    link_receiver( Destination, Links, Destination ),
    matching( Destinations, Links, Destinations2, Destinations1 ).

properly_connected( +Station, +Stations )

holds when Station and each member of Stations have exactly one destination in common.

properly_connected( Station, Stations ) :-
    station_destinations( Station, Destinations ),
    station_destinations( Station1, Destinations1 ),
    forall(
        member( Station1, Stations ),
        one_common_member( Destinations, Destinations1 )
        ).

one_common_member( ?Set0, ?Set1 )

holds when Set0 and Set1 have exactly one common member.

one_common_member( Set0, Set1 ) :-
    select( Member, Set0, Residue0 ),
    select( Member, Set1, Residue1 ),
    \+ common_member( Residue0, Residue1 ).

common_member( ?Set0, ?Set1 )

holds when Set0 and Set1 have a common member.

common_member( Set0, Set1 ) :-
    member( Member, Set0 ),
    member( Member, Set1 ).

Data Abstraction

attraction( Name ) :-
    link_receiver( Name, _Links, _Value ).

link_receiver( s, links( S,_U,_O,_N,_T,_P,_Q), S ).
link_receiver( u, links(_S, U,_O,_N,_T,_P,_Q), U ).
link_receiver( o, links(_S,_U, O,_N,_T,_P,_Q), O ).
link_receiver( n, links(_S,_U,_O, N,_T,_P,_Q), N ).
link_receiver( t, links(_S,_U,_O,_N, T,_P,_Q), T ).
link_receiver( p, links(_S,_U,_O,_N,_T ,P,_Q), P ).
link_receiver( q, links(_S,_U,_O,_N,_T,_P, Q), Q ).

station_destinations( zoom(_Name, _Links, Destinations), Destinations ).

station_links( zoom(_Name, Links, _Destinations), Links ).

station_origin( zoom(Name, _Links, _Destinations), Name ).

Utility Predicates

Load a small library of Puzzle Utilities.

:- ensure_loaded( misc ).

print_zoom_tracks( +ZoomTracks )

prints all the links in ZoomTracks as origin - destination pairs of stations.

print_zoom_tracks( [] ).
print_zoom_tracks( [ZoomTrack|ZoomTracks] ) :-
    station_origin( ZoomTrack, Origin ),
    station_destinations( ZoomTrack, Destinations ),
    print_zoom_track_links( Destinations, Origin ),
    print_zoom_tracks( ZoomTracks ).

print_zoom_track_links( [], _Origin ).
print_zoom_track_links( [Destination|Destinations], Origin ) :-
    format( '~w~w~n', [Origin,Destination] ),
    print_zoom_track_links( Destinations, Origin ).

The code is available as plain text here.

Result

| ?- zoom.
su
so
st
uo
un
up
ot
on
oq
np
nt
ns
tu
tp
tq
pq
ps
po
qs
qu
qn

yes