%
% M12 problem in MiniZinc.
%
% See 
% Igor Kriz and Paul Siegel: 
%     Rubik's Cube Inspired Puzzles Demonstrate Math's "Simple Groups"
% http://www.sciam.com/article.cfm?id=simple-groups-at-play
%
% Programs:
%  http://www.math.lsa.umich.edu/~ikriz/
%  http://www.sciam.com/article.cfm?id=puzzles-simple-groups-at-play
%
% This model implements the M12 puzzle:
%  - length is 12 (2*6)
%  - the two operations are 
%      * merge (shuffle) and 
%      * inverse (reverse)
%  - some init configuration

%
% For a group theoretic solution of the M12 puzzle using the abstract algebra system GAP, 
% see http://www.hakank.org/group_theory/M12_gap.txt
% It is presented in the (swedish) blog post
% "Gruppteoretisk lösning av M12 puzzle i GAP" (Group theoretical solution of the M12 puzzle in GAP)
% http://www.hakank.org/webblogg/archives/001226.html

%
% Model created by Hakan Kjellerstrand, hakank@bonetmail.com
% See also my MiniZinc page: http://www.hakank.org/minizinc
%

int: n = 6; % we will use 2*n below
int: t = 2*n; % t for twice
int: rows; % the number of rows


% The results of the operations, starting with the init as first row
array[1..rows, 1..t] of var 1..t: x;

array[1..t] of var 1..t: init; % init array

% is this row the same as the original?
array[1..rows] of var 0..1: check;
var 2..rows: check_ix;

% the operations: 0: same, 1: shuffle, 2: reverse, 3: rotate
array[1..rows] of var 0..2: operations;

%
% The merge operator in M12 puzzle
%
% This will change 
%    1 12  2 11  3 10  4  9  5  8  6  7  to
%    1  2  3  4  5  6  7  8  9 10 11 12 
%
predicate merge(array[int] of var int: x, array[int] of var int: y, int: nn) = 

% minizinc 0.7.1
% 0-based
%    forall(i in 0..nn-1) (
%      % place the odd indices
%      y[i] = x[2*i]
%      /\ % place the even indices
%      y[2*nn-i-1] = x[2*i+1]
%    )


   % 0.8
     forall(i in 1..nn) (
       % place the odd indices
       x[2*i-1] = y[i]
       /\ % place the even indices
       x[2*i] = y[2*nn-(i-1)]
     )


;


%
% y is x reversed
%
predicate reverse(array[int] of var int: x, array[int] of var int: y) =
   let { 
     int: n = card(index_set(x))
   }
   in
% 0.7.1
%    forall(i in 0..n-1) (y[n-i-1] = x[i] )

   % v. 0.8
    forall(i in 1..n) ( y[n-i+1] = x[i])
;

% 
% y is the same as x
%
predicate same(array[int] of var int: x, array[int] of var int: y) =
   let { 
     int: n = card(index_set(x))
   }
   in
%  0.7.1
%  forall(i in 0..n-1) ( y[i] = x[i] )

%    % v. 0.8
    forall(i in 1..n) ( y[i] = x[i] )
;


% solve minimize check_ix;
% solve maximize check_ix;
% solve satisfy;
% flatzinc and ic can handle this, but not fz
solve :: int_search([x[i,j] | i,j in 1..t], "first_fail", "indomain", "complete") minimize check_ix;

constraint
   % init = [10,5,4,7,1,2,8,3,12,11,9,6] % this is random generated from M12proj.exe. rows = 16  1:10 minutes
   % init = [10,8,6,12,5,2,1,4,11,7,9,3] % another generated from M12proj.exe. harder  rows = 23   54 sec
   % init = [11,7,3,8,5,2,12,1,9,10,4,6] % another generated from M12proj.exe rows=23  1:15 min
   % init = [7,5,8,3,1,11,2,9,4,12,6,10] % generated from M12proj.exe rows=20  32 sec
   % init = [8,11,6,1,10,9,4,3,12,7,2,5] % rows=28 (11:50 minutes)
   % init = [1,4,9,3,11,6,8,5,10,2,7,12] % rows > 24
   % init = [3,8,6,12,4,7,5,11,1,10,9,2]

   % This is generated from the following moves  M2I1M
   % init = [4,1,10,7,9,12,3,6,5,2,11,8]  % rows = 5  < 1 sec
   init = [7,1,8,9,12,5,3,10,4,11,6,2] % generated by [r,s,s,s,s,r,s,s,r,r,s]
   % init = [5,6,11,10,8,2,3,12,7,4,9,1] % 14 operations
   % init = [5,6,10,4,1,11,9,2,12,8,3,7] % 13 operations
   % init = [3,4,6,10,11,1,9,7,8,2,12,5]
   % init = [1,12,2,11,3,10,4,9,5,8,6,7]
   % init = [1,4,7,10,12,9,6,3,2,5,8,11]
   % init = [11,2,9,7,1,10,6,5,8,3,12,4] % sssrsss
   % init = [12,11,10,9,8,7,6,5,4,3,2,1]
   /\

   check[1] = 0
   /\
   operations[1] = 0
   /\

   % initialize the first row of matrix.
   forall(i in 1..t) (
      x[1, i] = init[i]
   )
   /\ % select the operations
   forall(i in 2..rows) (
     ( % check if this row is 1..t. Then we're done.
       (check[i] = 1 <-> same([j | j in 1..t], [x[i,j] | j in 1..t ]))
     )
     /\ % select operations
     (
         ( % same
            same([x[i-1,j] | j in 1..t], [x[i,j] | j in 1..t ])
            /\ 
            operations[i] = 0
         )
         \/
         ( % merge (shuffle)
          merge([x[i-1,j] | j in 1..t], [x[i,j] | j in 1..t ], n) 
          /\ 
          operations[i] = 1
         )
         \/
         ( % reverse
          reverse([x[i-1,j] | j in 1..t], [x[i,j] | j in 1..t ])
          /\ 
          operations[i] = 2
         )
     )
   )
   /\ % no 2 reverse in row (symmetry breaking)
   forall(i in 2..rows) (
      not(operations[i] = 2 /\ operations[i-1] = 2)
   )
   /\ % check_ix is the first index where we have a row = init
   exists(i in 2..rows) (
     check_ix = i
     /\
     check[i] = 1
      /\ % no other solutions before check_ix = i
      forall(j in 2..i-1) ( check[j] != 1) 
   )
   /\ % another efficiency constraint: no two rows may be alike 
      % unless it is the solution.
      % Note: This is a real time saver.
   forall(i in 2..rows) (
      (check[i] = 0 
      -> 
      not forall(j in 1..t) (x[i-1,j] = x[i,j])
      )
   )

;

output 
[
  "\ninit: ", show(init), "\n",
  "check: ", show(check), "\n",
  "check_ix: ", show(check_ix), "\n", 
  "operations: ", show(operations), 
]
++
[
  if j = 1 then "\n" ++  show(operations[i]) ++ ": "  else " " endif ++
   show(x[i,j])
  | i in 1..rows, j in 1..t
]
;

%
% data
%
rows = t;