:- use_module(library(clpfd)).

% Takuzu - Solve Binary Puzzle
takuzu(Rows) :-
  append(Rows, Vars), Vars ins 0..1,
  maplist(triplets, Rows),
  unique(Rows),
  transpose(Rows, Columns),
  unique(Columns),
  maplist(triplets, Columns),
  maplist(label, Rows).

% Triplets
triplets(Vs) :- length(Vs, N), N2 is div(N, 2), 
  automaton(_, _, Vs,
    [source(a),sink(b),sink(c),sink(d),sink(e),sink(a)],
    [ arc(a,1,b,[Z]), arc(b,0,c,[Z+1]), arc(b,1,d,[Z]), arc(d,0,c,[Z+1])
    , arc(a,0,c,[Z+1]), arc(c,1,b,[Z]), arc(c,0,e,[Z+1]), arc(e,1,b,[Z])],
    [Z], [0], [N2]).

% Each row is unique
unique([]).
unique([Q|Qz]) :- unique(Q, Qz), unique(Qz).

unique(_Ps, []).
unique(Ps, [Q|Qz]) :- not_identical(Ps, Q), unique(Ps, Qz).

not_identical(Ps, Qs) :- 
  unique_signatures(Ps, Qs, Sigs),
  automaton(_, _, Sigs,
    [source(s),sink(i)],
    [arc(s,0,s),arc(s,1,i),arc(i,0,i),arc(i,1,i)],
    [_], [0], [_]).

unique_signatures([], [], []).
unique_signatures([P|Ps], [Q|Qs], [S|Sigs]) :-
  P #= Q  #<==> S #= 0,
  P #\= Q #<==> S #= 1,
  unique_signatures(Ps, Qs, Sigs).

% Sample Binary Puzzle
puzzle(1, [[0,_,0,_,_,_,_,_],
           [_,_,_,_,_,_,_,_],
           [_,_,_,_,_,1,1,_],
           [0,0,_,_,_,_,_,_],
           [0,_,_,_,_,_,_,0],
           [_,_,_,1,_,_,_,_],
           [_,_,_,_,_,_,_,_],
           [_,_,_,1,_,_,_,0]]).

% Sample Query
solve(N) :- puzzle(N, Rows), takuzu(Rows), maplist(writeln, Rows).

/** <examples>

?- solve(1).
*/
