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

:- include(base). 

solve(As) :- 
    get_largest_atom(As,vtx(N)),
    (member(bound(K),As)->true;true),
    length(Vars,N),
    Vars :: 0..1,
    sum(Vars) #=< K,
    VarsVect=..[v|Vars],
    functor(SCCVarsVect,v,N),  % represent the connectivity
    SCCVarsVect=..[v|SCCVars],
    functor(Graph,v,N),
    edges_to_graph(As,Graph,VarsVect,SCCVarsVect),
    ensure_covered(N,Graph,VarsVect),
    labeling([ffc],Vars),
    check_connected(Vars,SCCVars),
    output(Vars,1).

% also ensure that the dominating set is connected
edges_to_graph([],_,_,_).
edges_to_graph([edge(I,J)|As],Graph,VarsVect,SCCVarsVect):-
    arg(I,Graph,NeighborsI),
    member(J,NeighborsI),
    arg(J,Graph,NeighborsJ),
    member(I,NeighborsJ),!,
    arg(I,VarsVect,VarI),
    arg(J,VarsVect,VarJ),
    arg(I,SCCVarsVect,SCCVarI),
    arg(J,SCCVarsVect,SCCVarJ),
    VarI#=1 #/\ VarJ#=1 #=> SCCVarI#=SCCVarJ,
    edges_to_graph(As,Graph,VarsVect,SCCVarsVect).
edges_to_graph([_|As],Graph,VarsVect,SCCVarsVect):-
    edges_to_graph(As,Graph,VarsVect,SCCVarsVect).

ensure_covered(0,_,_):-!.
ensure_covered(I,Graph,VarsVect):-
    arg(I,Graph,Neighbors),
    closetail(Neighbors),
    get_vars([I|Neighbors],VarsVect,NeighborVars),
    sum(NeighborVars) #>= 1,
    I1 is I-1,
    ensure_covered(I1,Graph,VarsVect).

get_vars([],_,[]).
get_vars([I|Is],VarsVect,[Var|Vars]):-
    arg(I,VarsVect,Var),
    get_vars(Is,VarsVect,Vars).

% two nodes are connected if their SCC variables are identical
check_connected([],_).
check_connected([1|Bs],[SCCVar|SCCVars]):-!,
    check_connected(Bs,SCCVars,SCCVar).
check_connected([_|Bs],[_|SCCVars]):-
    check_connected(Bs,SCCVars).

check_connected([],_,_).
check_connected([B|Bs],[SCCVar|SCCVars],SCCVar1):-
    (B==1->SCCVar==SCCVar1;true),
    check_connected(Bs,SCCVars,SCCVar1).

output([],_):-nl.
output([1|Vars],I):-!,
    format("dom(~w). ",[I]),
    I1 is I+1,
    output(Vars,I1).
output([_|Vars],I):-
    I1 is I+1,
    output(Vars,I1).

test:-
    solve([vtx(1),vtx(2),vtx(3),vtx(4),vtx(5),vtx(6),vtx(7),vtx(8),edge(8,5),edge(7,4),edge(8,7),edge(7,5),edge(6,7),edge(8,1),edge(3,4),edge(6,1),edge(6,2),edge(3,5),edge(1,5),edge(5,4),edge(3,7),edge(5,2),edge(2,8),edge(3,1),edge(7,1),edge(6,4),edge(4,2),edge(8,4),bound(3)]).