/* 

  Sudoku 9x9 in Picat.

  Prolog benchmark problem (BProlog)
  """
  File   : sudoku81.pl (in B-Prolog)
  Author : Neng-Fa ZHOU
  Date   : 1996
  Purpose: solve a Japanese arithmetic puzzle (25*25)
  """
  
  This is a port of the B-Prolog model.
  However, it's a plain old 9x9 Sudoku...

  See sudoku250.pl for a 25x25 instance.
  And see sudoku.pi for a lot of 25x25 instances.

  This program was created by Hakan Kjellerstrand, hakank@gmail.com
  See also my Picat page: http://www.hakank.org/picat/

*/

import cp.

main => go.

go =>
  vars(Vars),
  solve(Vars),
  display_board(Vars),
  nl.

go2 =>
  statistics(runtime,[_,Start]),
  go,
  statistics(runtime,[_,End]),
  T is End-Start,
  print('execution time is '),print(T), print(' milliseconds'),nl.


vars(Vars):-
    Vars=[A11,A12,A13,B11,B12,B13,C11,C12,C13,
	  A21,A22,A23,B21,B22,B23,C21,C22,C23,
	  A31,A32,A33,B31,B32,B33,C31,C32,C33,
	  D11,D12,D13,E11,E12,E13,F11,F12,F13,
	  D21,D22,D23,E21,E22,E23,F21,F22,F23,
	  D31,D32,D33,E31,E32,E33,F31,F32,F33,
	  G11,G12,G13,H11,H12,H13,I11,I12,I13,
	  G21,G22,G23,H21,H22,H23,I21,I22,I23,
	  G31,G32,G33,H31,H32,H33,I31,I32,I33],
    Vars :: 1..9,
    A12 #= 6,B11 #= 2,B13 #= 4,C12 #= 5,
    A21 #= 4,A22 #= 7,B22 #= 6,C22 #= 8,C23 #= 3,
    A33 #= 5,
    B32 #= 7,
    C31 #= 1,
    D11 #= 9,E11 #= 1,E13 #= 3,F13 #= 2,
    D22 #= 1,D23 #= 2,F23 #= 9,
    D31 #= 6,E31 #= 7,E33 #= 9,F33 #= 8,
    G13 #= 6,H12 #= 8,I11 #= 7,
    G21 #= 1,G22 #= 4,H22 #= 9,I22 #= 2,I23 #= 5,
    G32 #= 8,H31 #= 3,H33 #= 5,I32 #= 9,
    % block
    all_different([A11,A12,A13,A21,A22,A23,A31,A32,A33]),
    all_different([B11,B12,B13,B21,B22,B23,B31,B32,B33]),
    all_different([C11,C12,C13,C21,C22,C23,C31,C32,C33]),
    all_different([D11,D12,D13,D21,D22,D23,D31,D32,D33]),
    all_different([E11,E12,E13,E21,E22,E23,E31,E32,E33]),
    all_different([F11,F12,F13,F21,F22,F23,F31,F32,F33]),
    all_different([G11,G12,G13,G21,G22,G23,G31,G32,G33]),
    all_different([H11,H12,H13,H21,H22,H23,H31,H32,H33]),
    all_different([I11,I12,I13,I21,I22,I23,I31,I32,I33]),
    % horizontal
    all_different([A11,A12,A13,B11,B12,B13,C11,C12,C13]),
    all_different([A21,A22,A23,B21,B22,B23,C21,C22,C23]),
    all_different([A31,A32,A33,B31,B32,B33,C31,C32,C33]),
    all_different([D11,D12,D13,E11,E12,E13,F11,F12,F13]),
    all_different([D21,D22,D23,E21,E22,E23,F21,F22,F23]),
    all_different([D31,D32,D33,E31,E32,E33,F31,F32,F33]),
    all_different([G11,G12,G13,H11,H12,H13,I11,I12,I13]),
    all_different([G21,G22,G23,H21,H22,H23,I21,I22,I23]),
    all_different([G31,G32,G33,H31,H32,H33,I31,I32,I33]),
    % vertical
    all_different([A11,A21,A31,D11,D21,D31,G11,G21,G31]),
    all_different([A12,A22,A32,D12,D22,D32,G12,G22,G32]),
    all_different([A13,A23,A33,D13,D23,D33,G13,G23,G33]),
    all_different([B11,B21,B31,E11,E21,E31,H11,H21,H31]),
    all_different([B12,B22,B32,E12,E22,E32,H12,H22,H32]),
    all_different([B13,B23,B33,E13,E23,E33,H13,H23,H33]),
    all_different([C11,C21,C31,F11,F21,F31,I11,I21,I31]),
    all_different([C12,C22,C32,F12,F22,F32,I12,I22,I32]),
    all_different([C13,C23,C33,F13,F23,F33,I13,I23,I33]).
    

display_board([A11,A12,A13,B11,B12,B13,C11,C12,C13,
	       A21,A22,A23,B21,B22,B23,C21,C22,C23,
	       A31,A32,A33,B31,B32,B33,C31,C32,C33,
	       D11,D12,D13,E11,E12,E13,F11,F12,F13,
	       D21,D22,D23,E21,E22,E23,F21,F22,F23,
	       D31,D32,D33,E31,E32,E33,F31,F32,F33,
	       G11,G12,G13,H11,H12,H13,I11,I12,I13,
	       G21,G22,G23,H21,H22,H23,I21,I22,I23,
	       G31,G32,G33,H31,H32,H33,I31,I32,I33]):-
    print([A11,A12,A13,B11,B12,B13,C11,C12,C13]),nl,
    print([A21,A22,A23,B21,B22,B23,C21,C22,C23]),nl,
    print([A31,A32,A33,B31,B32,B33,C31,C32,C33]),nl,
    print([D11,D12,D13,E11,E12,E13,F11,F12,F13]),nl,
    print([D21,D22,D23,E21,E22,E23,F21,F22,F23]),nl,
    print([D31,D32,D33,E31,E32,E33,F31,F32,F33]),nl,
    print([G11,G12,G13,H11,H12,H13,I11,I12,I13]),nl,
    print([G21,G22,G23,H21,H22,H23,I21,I22,I23]),nl,
    print([G31,G32,G33,H31,H32,H33,I31,I32,I33]),nl.