%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% A CHR program for solving Sudoku problems
% 
% Written nov 2005 by Jon Murua Gonz‡lez and Henning Christiansen (c)
% This program solves Sudoku problems in very short time
% - it employs CHR in a procedural way to implement a backtracking
% algorithm based on the heuristics try-most-constrained-field-first.
%
% It has been tested under SICStus Prolog
%
% The board is considered as a 4-dimensional cube with dimensions
% {a,b,c} x {a,b,c} x {1,2,3} x {1,2,3}
% where the letters identify a "big square", each of which has 3x3 atomic squares
% identified by a pait of numbers.
% For example, upper left atomic square is identified as (a,a,1,1)
%
% To use the program, enter the initially given numbers for your problem
% by modifying the 'addinitial' predicate at the bottom of the file and call
% ?- solve.

% A state of the board is represented by 81 constraints of the form
% f( 4 x Coordinates, Value, ListOfPossibleValues)
% ListOfPossibleValues indicates which numbers that can be placed in this atomic field
% without violating the rules of the game.
% 
% If ListOfPossibleValues is not [], Value is 0,
% otherwise it represents the value in that field.

:- use_module(library(chr)).
:- use_module(library(lists)).

handler sudoku.

constraints f/6, mostconstrained/6, renewcolumn/3, renewline/3, renewarea/3.

f(_,_,_,_,0,[]) <=> fail.

f(A,B,C,D,_,_) \ f(A,B,C,D,_,_) # Id <=> true pragma passive(Id).

f(A,B,C,D,0,[X]) # Id \ mostconstrained(A1,B1,C1,D1,L,Finished) <=> L=[X], A=A1,B=B1,C=C1,D=D1, Finished=false pragma passive(Id).
f(A,B,C,D,0,[X1,X2]) # Id \ mostconstrained(A1,B1,C1,D1,L,Finished) <=> L=[X1,X2], A=A1,B=B1,C=C1,D=D1, Finished=false pragma passive(Id).
f(A,B,C,D,0,[X1,X2,X3]) # Id \ mostconstrained(A1,B1,C1,D1,L,Finished) <=> L=[X1,X2,X3], A=A1,B=B1,C=C1,D=D1, Finished=false pragma passive(Id).
f(A,B,C,D,0,[X1,X2,X3,X4]) # Id \ mostconstrained(A1,B1,C1,D1,L,Finished) <=> L=[X1,X2,X3,X4], A=A1,B=B1,C=C1,D=D1, Finished=false pragma passive(Id).
f(A,B,C,D,0,[X1,X2,X3,X4,X5]) # Id \ mostconstrained(A1,B1,C1,D1,L,Finished) <=> L=[X1,X2,X3,X4,X5], A=A1,B=B1,C=C1,D=D1, Finished=false pragma passive(Id).
f(A,B,C,D,0,[X1,X2,X3,X4,X5,X6]) # Id \ mostconstrained(A1,B1,C1,D1,L,Finished) <=> L=[X1,X2,X3,X4,X5,X6], A=A1,B=B1,C=C1,D=D1, Finished=false pragma passive(Id).
f(A,B,C,D,0,[X1,X2,X3,X4,X5,X6,X7]) # Id \ mostconstrained(A1,B1,C1,D1,L,Finished) <=> L=[X1,X2,X3,X4,X5,X6,X7], A=A1,B=B1,C=C1,D=D1, Finished=false pragma passive(Id).
f(A,B,C,D,0,[X1,X2,X3,X4,X5,X6,X7,X8]) # Id \ mostconstrained(A1,B1,C1,D1,L,Finished) <=> L=[X1,X2,X3,X4,X5,X6,X7,X8], A=A1,B=B1,C=C1,D=D1, Finished=false pragma passive(Id).
f(A,B,C,D,0,[X1,X2,X3,X4,X5,X6,X7,X8,X9]) # Id \ mostconstrained(A1,B1,C1,D1,L,Finished) <=> L=[X1,X2,X3,X4,X5,X6,X7,X8,X9], A=A1,B=B1,C=C1,D=D1, Finished=false pragma passive(Id).
mostconstrained(_,_,_,_,_,Finished)<=>Finished=true.

renewcolumn(B,D,V) \ f(A,B,C,D,X,L) #Id <=> delete(L,V,LL), f(A,B,C,D,X,LL) pragma passive(Id).
renewcolumn(_,_,_) <=> true.
renewline(A,C,V) \ f(A,B,C,D,X,L) #Id <=> delete(L,V,LL), f(A,B,C,D,X,LL) pragma passive(Id).
renewline(_,_,_) <=> true.
renewarea(A,B,V) \ f(A,B,C,D,X,L) #Id <=> delete(L,V,LL), f(A,B,C,D,X,LL) pragma passive(Id).
renewarea(_,_,_) <=> true.


solve :- initialize, addinitial, fillall, printsolution.
fillall :- fillone(Finished), (Finished == true -> true; fillall).
fillone(Finished) :- mostconstrained(A,B,C,D,L,Finished), (Finished == true -> true; member(V,L), add(A,B,C,D,V)).

add(A,B,C,D,V):- f(A,B,C,D,V,[]), renew(A,B,C,D,V).

renew(A,B,C,D,V) :- renewcolumn(B,D,V), renewline(A,C,V), renewarea(A,B,V).

initialize :-  fill1(a), fill1(b), fill1(c).
fill1(X) :- fill2(X,a),fill2(X,b),fill2(X,c).
fill2(X,Y) :- fill3(X,Y,1), fill3(X,Y,2), fill3(X,Y,3).
fill3(A,B,C) :- fill4(A,B,C,1), fill4(A,B,C,2), fill4(A,B,C,3).
fill4(A,B,C,D) :- f(A,B,C,D,0,[1,2,3,4,5,6,7,8,9]).

% NB: Different enumaration methods
printsolution:- print1(a), print1(b), print1(c).
print1(X) :- print2(X,1),print2(X,2),print2(X,3), nl.
print2(X,Y) :- print3(X,Y,a), print3(X,Y,b), print3(X,Y,c), nl.
print3(A,B,C) :- print4(A,B,C,1), print4(A,B,C,2), print4(A,B,C,3), write(' ').
print4(A,B,C,D) :-
   find_constraint(f(A,C,B,D,Val,_),Id), write(Val), remove_constraint(Id).

addinitial :-
    %% add( 4xcoordinates, InitialValue) %%
    add(a,a,1,2,6),
	add(a,a,2,3,8),
	add(a,a,3,1,2),
	add(a,b,1,1,1),
	add(a,b,1,3,4),
	add(a,b,2,1,3),
	add(a,b,2,3,5),
	add(a,c,1,2,5),
	add(a,c,2,1,6),
	add(a,c,3,3,1),
	add(b,a,1,1,8),
	add(b,a,2,3,6),
	add(b,a,3,1,7),
	add(b,b,1,1,4),
	add(b,b,1,3,7),
	add(b,b,3,1,9),
	add(b,b,3,3,1),
	add(b,c,1,3,6),
	add(b,c,2,1,3),
	add(b,c,3,3,4),
	add(c,a,1,1,5),
	add(c,a,2,3,7),
	add(c,a,3,2,4),
	add(c,b,2,1,2),
	add(c,b,2,3,6),
	add(c,b,3,1,5),
	add(c,b,3,3,8),
	add(c,c,1,3,2),
	add(c,c,2,1,9),
	add(c,c,3,2,7).