% http://www.cs.kuleuven.be/~dtai/events/ASP-competition/Benchmarks/WeightBoundedDS.shtml
% by J. You, adapted by N.F. Zhou

:-include(base). 

solve(As) :- 
    consult_clauses(As),
    findall(N,vtx(N),Ns), 
    findall(edge(N1,N2),edge(N1,N2),Es),
    bound(K),
    minweight(MinW),
    map(Ns,Vars,MapV), % defined in base.pl
    domain(Vars,0,1),  
    Card #= sum(Vars),
    Card#=<K,
    hold(MapV,Es,MinW),
    minof(labeling([],Vars),Card,output(Ns,Vars)),!,
    format("OPTIMUM FOUND").
solve(_) :-
    format("UNSATISFIABLE~n").

/* 
hold(Vars,Es): For any node v in V, at least one of the following holds
 1. v is in D (the vth variable in Vars is 1)
 2. the weight sum of all the edges from any i in D to v >= minweight.
 3. the weight sum of all the edges from v to any j in D >= minweight, or 
*/

hold(MapV,Es,MinW) :- hold1(MapV,Es,MinW,MapV).

hold1([],_,_,_).
hold1([(N,V)|R],Es,MinW,MapV) :- 
    weight_list2(N,Es,Lst2,MapV),
    weight_list3(N,Es,Lst3,MapV),
    V #= 1 #\/ sum(Lst2) #>= MinW #\/ sum(Lst3) #>= MinW,
    hold1(R,Es,MinW,MapV).

% add W into the sum only if Ni is in D
weight_list2(_,[],[],_).
weight_list2(Nv,[edge(Ni,Nv)|R],[W*Vi|L],MapV) :- !, 
    edgewt(Ni,Nv,W),
    map(Ni,Vi,MapV),
    weight_list2(Nv,R,L,MapV).
weight_list2(N,[_|R],L,MapV) :-
   weight_list2(N,R,L,MapV).

% add W into the sum only if Nj is in D
weight_list3(_,[],[],_).
weight_list3(Nv,[edge(Nv,Nj)|R],[W*Vj|L],MapV) :- !,
    edgewt(Nv,Nj,W),
    map(Nj,Vj,MapV),
    weight_list3(Nv,R,L,MapV).
weight_list3(N,[_|R],L,MapV) :-
    weight_list3(N,R,L,MapV).

output([],_):-nl.
output([N|Ns],[V|Vs]) :- 
    (V==1->
     format("in(~w). ",[N]);
     true),
    output(Ns,Vs).

test:-
    solve([vtx(1),vtx(2),vtx(3),
	   edge(1,2),edge(1,3),edge(3,2),
	   edgewt(1,2,1),edgewt(1,3,2),edgewt(3,2,3),
	   minweight(2),
	   bound(2)]).

/*
when minweight(4): 
Solution: in(1), in(3)

when minweight(3): 
Solution: in(2), in(3)
          in(1), in(2)
          in(1), in(3)

when minweight(2): 
Solution: in(3)
          in(2), in(3)
          in(1), in(2)
          in(1), in(3)
*/