Encoding Class HamiltonianCycle

Class Tree
Description A Hamiltonian cycle (or HC for short) in an undirected graph G=(V,E), where V is the set of vertices and E is the set of edges, is a cycle in G such that every vertex v in V occurs exactly once in the cycle.

The input of the HC problem is an undirected graph. The goal is to find a HC in the graph.

Input Format
============
Each input graph is stored in a plain text file. The format of the file is as follows:

a. The first line defines the number of vertices in the graph, using the predicate "bound(...)." For instance:
bound(17).
specifies that the graph has 17 vertices.

b. Given that "bound(n)." is the first line, the next n lines define vertices by means of a predicate "vtx" .

vtx(1).
vtx(2).
...
vtx(n).

c. The definition of edges follows that of the vertices. The predicate used to define edges is a binary predicate "edge" with edge(i,j) meaning that i and j are connected with an edge:

edge(1,3).
edge(4,2).
...

Loops are disallowed (no line of the form "edge(i,i)."). In addition, if there is a line "edge(i,j).", there will not be the line
"edge(j,i).".

Example
vtx(1).
vtx(2).
vtx(3).
vtx(4).
edge(1,2).
edge(3,2).
edge(4,3).
edge(1,4).

Output Requirement
==================
The solution must be represented by means of a binary predicate "hc". That is atoms of the form "hc(i,j)" must describe all edges of the hamiltonian cycle. An atom hc(i,j) belongs to the answer-set if and only if 1) edge(i,j) belongs to the Hamiltonian cycle; and 2) edge(i,j) is defined in the input instance. For example, if edge(2,3) is defined in
the input instance and it belongs to the Hamiltonian cycle, then hc(2,3) belongs to the answer-set (instead of hc(3,2)).

For our example input, the following set of ground atoms specifies a valid HC:
hc(1,2)
hc(3,2)
hc(4,3)
hc(1,4)

Authors: Lengning Liu and Miroslaw Truszczynski
Affiliation: University of Kentucky
Email: {lliu1, mirek}@cs.uky.edu
Encodings
1 - 6 of 6