% http://www.cs.kuleuven.be/~dtai/events/ASP-competition/Benchmarks/HClustering.shtml
% by Neng-Fa Zhou, April 17, 2009

:-include(base).

solve(As):-
    get_largest_atom(As,vtx(N)),  % N vertexes 
    a2_new(Edges,N,N),
    init_edges(As,Edges),
    (member(bound(B),As)->true;true),
    get_largest_atom(As,levels(MaxLevel)),
    create_vertexes(Vtxes,1,N,MaxLevel,Levels,Parents,GVars),
    count(1,Levels,#=<,B),   % clique at level 1
    clique_bound(Parents,N,B),
    parent_chid(Vtxes,Vtxes,Edges,MaxLevel),
    labeling([ff],GVars),!,
    output(Vtxes).
solve(_):-
    format("UNSATISFIABLE~n").

init_edges([],_).
init_edges([edge(X,Y)|As],Edges):-!,
    a2_get(Edges,X,Y,1),
    a2_get(Edges,Y,X,1),
    init_edges(As,Edges).
init_edges([_|As],Edges):-
    init_edges(As,Edges).
    
create_vertexes(Vtxes,I,N,_,Levels,Parents,GVars):-I>N,!,
    Vtxes=[],Levels=[],Parents=[],GVars=[].
create_vertexes([vtx(I,Level,Parent)|Vtxes],I,N,MaxLevel,[Level|Levels],[Parent|Parents],[GVar|GVars]):-
    I1 is I+1,
    Level :: 1..MaxLevel,
    Parent :: 0..N,
    GVar :: 1..MaxLevel*(N+1),
    Parent #= (GVar-1)//MaxLevel,    
    Level #= (GVar-1) mod MaxLevel+1,
    (Level#=1 #<=> Parent#=0),
    (Level#>1 #<=> Parent#\=0),
    Parent#\=I,
    create_vertexes(Vtxes,I1,N,MaxLevel,Levels,Parents,GVars).
    
% every clique has at most B elements
clique_bound(_,I,_):-I<0,!.
clique_bound(Parents,I,B):-
    count(I,Parents,#=<,B),
    I1 is I-1,
    clique_bound(Parents,I1,B).
	   
% A parent's level is one less than its children's
% A vertex can't be anybody's parent if its level is MaxLevel
% Two vertexes can't share the same parent if they are not connected
parent_chid([],_,_,_).
parent_chid([V|Vs],AllVs,Edges,MaxLevel):-
    parent_chid_aux(V,AllVs,Edges,NoParentIsI),
    V=vtx(_,LevelI,_),
    LevelI#=MaxLevel #=> NoParentIsI,
    parent_chid(Vs,AllVs,Edges,MaxLevel).

parent_chid_aux(_,[],_,1).
parent_chid_aux(Vi,[vtx(I,_,_)|Vs],Edges,NoParentIsI):-
    Vi=vtx(I,_,_),!,
    parent_chid_aux(Vi,Vs,Edges,NoParentIsI).
parent_chid_aux(Vi,[vtx(J,LevelJ,ParentJ)|Vs],Edges,(ParentJ#\=I #/\ NoParentIsI)):-
    Vi=vtx(I,LevelI,ParentI),
    ParentI#=J #=>LevelJ#=LevelI-1,
    a2_get(Edges,I,J,Eij),
    (var(Eij)-> % I and J are not connected
        ParentI#\=J,
        (I<J->ParentI#\=ParentJ;true);
        true),
    parent_chid_aux(Vi,Vs,Edges,NoParentIsI).

output(Vtxes):-
    output_level(Vtxes),
    output_parent(Vtxes),
    nl.

output_level([]).
output_level([vtx(I,Level,_)|Vtxes]):-
    format("levelvtx(~w,~w). ",[Level,I]),
    output_level(Vtxes).

output_parent([]).
output_parent([vtx(I,_,Parent)|Vtxes]):-
    (Parent==0->true;
     format("parentedge(~w,~w). ",[Parent,I])),
    output_parent(Vtxes).
     
test:-
    solve([vtx(1),vtx(2),vtx(3),vtx(4),vtx(5),vtx(6),vtx(7),vtx(8),edge(8, 3),edge(8, 6),edge(8, 5),edge(8, 1),edge(3, 5),edge(3, 1),edge(7, 6),edge(7, 5),edge(7, 4),edge(6, 5),edge(6, 1),edge(5, 1),edge(5, 2),edge(4, 2),bound(2),levels(1),levels(2),levels(3)]).