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

:-include(base).

solve(As):- 
    extract_companies(As,Cs),
    map(Cs,Bs0,MapC0), /* Bs0=[B01,...,B0n] represents a strategic set */
    map(Cs,Bs1,MapC1), /* Bs1=[B11,...,B1n] represents a subset of Bs0 */
    Bs0 :: 0..1,
    Bs1 :: 0..1,
    sum(Bs1) #< sum(Bs0), 
    sets_notin_notin(Bs0,Bs1), /* Bs1 is a proper subset of Bs0 */
    gen_constrs(As,MapC0,MapC1),
    labeling(Bs0), 
    (labeling(Bs1) -> fail;true),!,
    output(Cs,Bs0).
solve(_):-
    format("UNSATISFIABLE~n").

extract_companies([],Cs):-closetail(Cs).
extract_companies([query(C1,C2)|As],Cs):-
    member(C1,Cs),member(C2,Cs),!,
    extract_companies(As,Cs).
extract_companies([controlled_by(C,C1,C2,C3,C4)|As],Cs):-
    member(C,Cs),member(C1,Cs),member(C2,Cs),member(C3,Cs),member(C4,Cs),!,
    extract_companies(As,Cs).
extract_companies([produced_by(_,C1,C2,C3,C4)|As],Cs):-
    member(C1,Cs),member(C2,Cs),member(C3,Cs),member(C4,Cs),!,    
    extract_companies(As,Cs).

gen_constrs([],_,_).
gen_constrs([query(C1,C2)|As],MapC0,MapC1):-!,
    map(C1,1,MapC0), % C1 and C2 belong to the set S0
    map(C2,1,MapC0),  
    gen_constrs(As,MapC0,MapC1).

% C is strategic if all the controllers are strategic
gen_constrs([controlled_by(C,C1,C2,C3,C4)|As],MapC0,MapC1):-!,  
    map(C,B0,MapC0),
    map(C1,B01,MapC0),
    map(C2,B02,MapC0),
    map(C3,B03,MapC0),
    map(C4,B04,MapC0),
    B01 #/\ B02 #/\ B03 #/\ B04 #=> B0,
    map(C,B1,MapC1), 
    map(C1,B11,MapC1),
    map(C2,B12,MapC1),
    map(C3,B13,MapC1),
    map(C4,B14,MapC1),
    B11 #/\ B12 #/\ B13 #/\ B14 #=> B1,
    gen_constrs(As,MapC0,MapC1).

% this good still is produced
gen_constrs([produced_by(_,C1,C2,C3,C4)|As],MapC0,MapC1):-  
    map(C1,B01,MapC0),
    map(C2,B02,MapC0),
    map(C3,B03,MapC0),
    map(C4,B04,MapC0),
    B01 #\/ B02 #\/ B03 #\/ B04,
    map(C1,B11,MapC1),
    map(C2,B12,MapC1),
    map(C3,B13,MapC1),
    map(C4,B14,MapC1),
    B11 #\/ B12 #\/ B13 #\/ B14,
    gen_constrs(As,MapC0,MapC1).
    
% Bs0=[B01,...,B0n] Bs1=[B11,...,B1n] if B0i=0 then B1i=0
sets_notin_notin([],_).
sets_notin_notin([B0|Bs0],[B1|Bs1]):-
    B0#=0 #=> B1#=0,
    sets_notin_notin(Bs0,Bs1).

output([],_):-nl.
output([C|Cs],[B|Bs]):-
    (B==1->format("strategic(~w). ",[C]);true),
    output(Cs,Bs).

test:-
    solve([produced_by(p,a,a,c,c),
           controlled_by(b,a,a,a,a),
           query(a,b)]).
/*
test:-
    solve([produced_by(pasta,barilla,amato,dececco,divella),produced_by(tonno,callipo,star,almera,asdomar),controlled_by(callipo,star,almera,asdomar,barilla),controlled_by(barilla,callipo,almera,dececco,star),query(callipo,barilla)]).
*/