\begin{verbatim}

 const k = 4.

 const vsize = 8.

 vertex(1..vsize).

 label(0..k).


 edge(1,5).
 edge(1,8).
 edge(1,7).
 edge(2,6).
 edge(2,7).
 edge(3,5).
 edge(3,7).
 edge(4,5).
 edge(4,7).

% assigning unique label to each vertex.

 label_of(V, L) :-
     vertex(V),
     label(L),
     not other_label(V,L).

 other_label(V,L) :-
        vertex(V),
        label(LL),
        label(L),
        label_of(V,LL),
        not eq(L,LL).

%No two vertices have the same non-zero level.

    :-   vertex(V),
         vertex(VV),
         vertex(L),
         label_of(V,L),
         label_of(VV,L),
         not eq(V,VV),
         not eq(L,0).

%The following enforce that each non-zero label is assigned to some
%vertex.

 assigned(L)    :-  vertex(V),
                    label(L),
                    label_of(V,L).

    :-  label(L),
        not eq(L,0),
        not assigned(L).

% vertex cover condition: if both vertices of an edge are labeled
% 0 then we don't have a vertex cover.

    :-  vertex(V),
        vertex(VV),
        label(L),
        label(LL),
        edge(V,VV),
        label_of(V,L),
        label_of(VV,LL),
        L = 0,
        LL =0.

 vc(V)  :-  vertex(V),
            label(L),
            label_of(V,L),
            not eq(L,0).


 %minimize{vc(1) = 1, vc(2) =2, vc(3) = 10, vc(4) = 4, vc(5) = 5,
 %           vc(6) = 1, vc(7) = 7, vc(8) = 1}.

 weight vc(X) = 12-X.

 minimize{vc(X) : vertex(X)}.

 hide vertex(X).
 hide edge(X,Y).
 hide label(X).
 hide assigned(X).
 hide other_label(X,Y).
 hide label_of(V,L).

\end{verbatim}