% http://www.cs.kuleuven.be/~dtai/events/ASP-competition/Benchmarks/SchurNumbers.shtml
% adapted by Neng-Fa Zhou
:-include(base).

solve(As):-
    findall(N,member(number(N),As),Ns),
    findall(P,member(part(P),As),Ps),
    map(Ps,0,D,MapPs),  % defined in base.pl
    map(Ns,Vars,MapNs), 
    Vars :: D,
    placeAssigned(As,MapPs,MapNs),
    create_nogood_tuples(D,NoGoodTuples),
    constrain(Ns,MapNs,NoGoodTuples),
    labeling([ff_inout],Vars),!,
    output(Ns,Vars,MapPs).
solve(_):-
    format("UNSATISFIABLE~n").

% (I,I,I) is no good for each I in D
create_nogood_tuples([],[]).
create_nogood_tuples([I|Is],[(I,I,I)|NoGoodTuples]):-
    create_nogood_tuples(Is,NoGoodTuples).

placeAssigned([],_MapPs,_MapNs).
placeAssigned([assigned(N,P)|Assigned],MapPs,MapNs):-!,
    map_get(N,Var,MapNs),
    map_get(P,I,MapPs),
    Var=I,
    placeAssigned(Assigned,MapPs,MapNs).
placeAssigned([_|Assigned],MapPs,MapNs):-
    placeAssigned(Assigned,MapPs,MapNs).

constrain([],_MapNs,_NoGoodTuples).
constrain([N|Ns],MapNs,_NoGoodTuples):-
    N2 is N+N,
    map_get(N,Var,MapNs),
    (map_get(N2,Var2,MapNs)->
       Var #\= Var2;
     true),
    constrain(N,Var,Ns,MapNs,_NoGoodTuples),
    constrain(Ns,MapNs,_NoGoodTuples).

constrain(_N,_,[],_MapNs,_NoGoodTuples).
constrain(N1,Var1,[N2|Ns],MapNs,NoGoodTuples):-
    N is N1+N2,
    (map_get(N,Var,MapNs)->
     map_get(N2,Var2,MapNs),
     (Var1,Var2,Var) notin NoGoodTuples;
/*
     (Var1 #= Var2) #=> (Var #\= Var1),
     (Var1 #= Var) #=> (Var2 #\= Var1),
     (Var2 #= Var) #=> (Var1 #\= Var);
*/
     true),
    constrain(N1,Var1,Ns,MapNs,NoGoodTuples).

output([],_Vars,_MapPs):-nl.
output([N|Ns],[V|Vars],MapPs):-
     map_get(P,V,MapPs),
     format("assigned(~w,~w). ",[N,P]),
     output(Ns,Vars,MapPs).
     
test :-
    solve([number(1),number(2),number(3),number(4),number(5),number(6),number(7),number(8),number(9),number(10),number(11),number(12),number(13),number(14),number(15),number(16),number(17),number(18),number(19),number(20),number(21),number(22),number(23),number(24),number(25),number(26),number(27),number(28),number(29),number(30),number(31),number(32),number(33),number(34),number(35),number(36),number(37),number(38),number(39),number(40),number(41),number(42),number(43),number(44),number(45),number(46),number(47),number(48),number(49),number(50),number(51),number(52),number(53),number(54),number(55),number(56),number(57),number(58),number(59),number(60),number(61),number(62),number(63),number(64),number(65),number(66),number(67),number(68),number(69),number(70),number(71),number(72),number(73),number(74),number(75),number(76),number(77),number(78),number(79),number(80),number(81),number(82),number(83),number(84),number(85),number(86),number(87),number(88),number(89),number(90),number(91),number(92),number(93),number(94),number(95),number(96),number(97),number(98),number(99),number(100),number(101),number(102),number(103),number(104),number(105),number(106),number(107),number(108),number(109),number(110),part(1),part(2),part(3),part(4),part(5)]).

/*
test :-
    solve([number(1),number(2),number(3),number(4),number(5),number(6),number(7),number(8),number(9),number(10),number(11),number(12),number(13),number(14),number(15),number(16),number(17),number(18),number(19),number(20),number(21),number(22),number(23),number(24),number(25),number(26),number(27),number(28),number(29),number(30),number(31),number(32),number(33),number(34),number(35),number(36),number(37),number(38),number(39),number(40),number(41),number(42),number(43),number(44),number(45),number(46),number(47),number(48),number(49),number(50),number(51),number(52),number(53),number(54),number(55),number(56),number(57),number(58),number(59),number(60),number(61),number(62),number(63),number(64),number(65),number(66),number(67),number(68),number(69),number(70),number(71),number(72),number(73),number(74),number(75),number(76),number(77),number(78),number(79),number(80),number(81),number(82),number(83),number(84),number(85),number(86),number(87),number(88),number(89),number(90),number(91),number(92),number(93),number(94),number(95),number(96),number(97),number(98),number(99),number(100),number(101),number(102),number(103),number(104),number(105),number(106),number(107),number(108),number(109),number(110),number(111),number(112),number(113),number(114),number(115),number(116),number(117),number(118),number(119),number(120),number(121),number(122),number(123),number(124),number(125),number(126),number(127),number(128),number(129),number(130),part(1),part(2),part(3),part(4),part(5),assigned(1,1)]).
*/
/*
test :-
    solve([number(1),number(2),number(3),number(4),number(5),number(6),number(7),number(8),number(9),number(10),number(11),number(12),number(13),number(14),number(15),number(16),number(17),number(18),number(19),number(20),number(21),number(22),number(23),number(24),number(25),number(26),number(27),number(28),number(29),number(30),number(31),number(32),number(33),number(34),number(35),number(36),number(37),number(38),number(39),number(40),number(41),number(42),number(43),number(44),number(45),number(46),number(47),number(48),number(49),number(50),number(51),number(52),number(53),number(54),number(55),number(56),number(57),number(58),number(59),number(60),number(61),number(62),number(63),number(64),number(65),number(66),number(67),number(68),number(69),number(70),number(71),number(72),number(73),number(74),number(75),number(76),number(77),number(78),number(79),number(80),number(81),number(82),number(83),number(84),number(85),number(86),number(87),number(88),number(89),number(90),number(91),number(92),number(93),number(94),number(95),number(96),number(97),number(98),number(99),number(100),number(101),number(102),number(103),number(104),number(105),number(106),number(107),number(108),number(109),number(110),number(111),number(112),number(113),number(114),number(115),number(116),number(117),number(118),number(119),number(120),number(121),number(122),number(123),number(124),number(125),number(126),number(127),number(128),number(129),number(130),part(1),part(2),part(3),part(4),part(5),assigned(1,1),assigned(10,2),assigned(20,3),assigned(30,4),assigned(40,5)]).
*/