/*
by J. You, March 24, 2009, adapted by N.F. April 7, 2009.
This is a benchmark at the 2nd ASP solver competition:
http://www.cs.kuleuven.be/~dtai/events/ASP-competition/SubmittedBenchmarks.html
conditions:
*/

:- include(base). 

solve(As) :- 
    get_largest_atom(As,vtx(N)),  % N is the number of vertexes
    findall(wtedge(V1,V2,W),member(weight_wtedge(V1,V2,W),As),Es),
    get_largest_atom(As,parts(K)), % K is the number of blocks.
    (member(vtxbound(NumV),As)->true;true),  % number of vertices in each block
    (member(edgebound(Bound),As)->true;true),
    length(Vars,N),
    domain(Vars,1,K),  
    VarsVect=..[v|Vars],
    functor(SccVect,v,N),       % All connected vertexes share a SCC variable
    xcount(1,K,Vars,NumV),      % every block has 1 to NumV vertices
    satisfy_edge_bound(1,K,Es,Bound,VarsVect),   % satisfy cond2 and part of cond3
    connected(Es,VarsVect,SccVect),
    functor(BlockSccVect,v,K),
    labeling([ff],Vars), 
    check_connected(Vars,1,BlockSccVect,SccVect),!,
    output(Vars,1).
solve(_) :- 
    format("UNSATISFIABLE~n").

/* the number of vertices in each block is at least 1 and at most NumV */
xcount(I,K,_,_) :- I>K,!.
xcount(I,K,Vars,NumV) :- 
   count(I,Vars,#=,N), 
   N #>= 1, N #=< NumV, 
   I1 is I+1, 
   xcount(I1,K,Vars,NumV).

/*
2. The sum of the weights of the edges between each two blocks is at most Bound.
*/
satisfy_edge_bound(K,K,_,_,_):-!.
satisfy_edge_bound(I,K,Es,Bound,VarsVect) :- 
   satisfy_edge_bound_aux(I,K,Es,Bound,VarsVect),
   I1 is I+1,
   satisfy_edge_bound(I1,K,Es,Bound,VarsVect).

satisfy_edge_bound_aux(I,I,_,_,_):-!.
satisfy_edge_bound_aux(I,J,Es,Bound,VarsVect) :-
   list_for_sum(I,J,Es,Lst,VarsVect),
   sum(Lst) #=< Bound,
   J1 is J-1,
   satisfy_edge_bound_aux(I,J1,Es,Bound,VarsVect).

list_for_sum(_,_,[],[],_).
list_for_sum(I,J,[wtedge(N1,N2,W)|R],[T|S],VarsVect) :- 
   arg(N1,VarsVect,V1),
   arg(N2,VarsVect,V2),
   (((V1 #= I #/\ V2#=J) #\/ (V1 #= J #/\ V2#=I)) #=> T#=W),
   (((V1 #\= I #\/ V2#\=J) #/\ (V1 #\= J #\/ V2#\=I)) #=> T#=0),
   list_for_sum(I,J,R,S,VarsVect).

/*
3. The subgraph induced by the vertices in each of the blocks is connected.
*/
connected([],_,_).
connected([wtedge(N1,N2,_)|Es],VarsVect,SccVect):-
   arg(N1,VarsVect,V1),
   arg(N2,VarsVect,V2),
   arg(N1,SccVect,Scc1),
   arg(N2,SccVect,Scc2),
   V1#=V2 #<=> Scc1#=Scc2,  % connected
       % the same as  freeze(V1,freeze(V2,(V1==V2->Scc1=Scc2;true))),
   connected(Es,VarsVect,SccVect).

% all vertexes in a block share the same SCC variable
check_connected([],_,_,_).
check_connected([Block|Blocks],I,BlockSccVect,VertexSccVect):-
   arg(I,VertexSccVect,VertexScc),
   arg(Block,BlockSccVect,BlockScc),
   (susp_var(BlockScc)->VertexScc==BlockScc;
    BlockScc=VertexScc),
   I1 is I+1,
   check_connected(Blocks,I1,BlockSccVect,VertexSccVect).

output([],_).
output([Block|Blocks],V) :- 
   format("partition(~w,~w). ",[V,Block]),
   V1 is V+1,
   output(Blocks,V1).

test:-
    solve([vtx(1),vtx(2),vtx(3),vtx(4),vtx(5), 
	   weight_wtedge(4,5,1), 
	   weight_wtedge(2,5,1), 
	   weight_wtedge(2,3,2), 
	   weight_wtedge(4,3,2), 
	   weight_wtedge(4,2,1), 
	   weight_wtedge(1,5,1), 
	   weight_wtedge(1,4,1), 
	   weight_wtedge(5,3,2), 
	   weight_wtedge(1,2,1), 
	   weight_wtedge(3,1,1),   %removing these two will cut solutions from 4 to 2,
	   parts(1), parts(2), parts(3), 
	   vtxbound(3), edgebound(4)]).

/*
4 nonsymmetric solutions without commenting out the above two facts,

partition(1,1), partition(2,1), partition(3,1), partition(4,2), partition(5,3),
partition(1,1), partition(2,1), partition(3,2), partition(4,3), partition(5,3),
partition(1,1), partition(2,2), partition(3,2), partition(4,2), partition(5,3),
partition(1,1), partition(2,2), partition(3,3), partition(4,3), partition(5,3),

2 solutions for the program as it is 

partition(1,1), partition(2,2), partition(3,2), partition(4,2), partition(5,3),
partition(1,1), partition(2,2), partition(3,3), partition(4,3), partition(5,3),
*/