/*

  Langford's number problem (generalized version) in Picat.

  Langford's number problem (CSP lib problem 24)
  http://www.csplib.org/Problems/prob024/
  """
  Consider two sets of the numbers from 1 to 4. The problem is to arrange the eight numbers 
  in the two sets into a single sequence in which the two 1’s appear one number apart, the two 
  2’s appear two numbers apart, the two 3’s appear three numbers apart, and the two 4’s appear four numbers apart.
 
  The problem generalizes to the L(k,n) problem, which is to arrange k sets of numbers 1 to n, 
  so that each appearance of the number m is m numbers on from the last. For example, the 
  L(3,9) problem is to arrange 3 sets of the numbers 1 to 9 so that the first two 1’s and 
  the second two 1’s appear one number apart, the first two 2’s and the second two 2’s appear 
  two numbers apart, etc.
  """
 
  Also see:
  * John E. Miller: Langford's Problem
    http://dialectrix.com/langford.html
  
  * Encyclopedia of Integer Sequences for the number of solutions for each k
    http://www.research.att.com/cgi-bin/access.cgi/as/njas/sequences/eisA.cgi?Anum=014552

  This model is (compared to http://hakank.org/picat/langford.pi) 
  a generalized version, i.e. where K >= 2.


  Note: For k=4,n=2 there are two different solutions:

     solution:[4,1,3,1,2,4,3,2]
     position:[2,5,3,1,4,8,7,6]
  and
     solution:[2,3,4,2,1,3,1,4]
     position:[5,1,2,3,7,4,6,8]

  Which this symmetry breaking

     Solution[1] #< Solution[K2],

  then just the second solution is shown.

  More interestingly, here are some observations for k> 2.

  For n=9 k=3 there are 3 solutions (with symmetry breaking):

   [1,9,1,6,1,8,2,5,7,2,6,9,2,5,8,4,7,6,3,5,4,9,3,8,7,4,3]
   [1,9,1,2,1,8,2,4,6,2,7,9,4,5,8,6,3,4,7,5,3,9,6,8,3,5,7]
   [1,8,1,9,1,5,2,6,7,2,8,5,2,9,6,4,7,5,3,8,4,6,3,9,7,4,3]

  Some solutions for k=3. 

  There's a solution for k=3 only of n mod 9 == (0,1,8):
     Picat> X=[I : I in 1..100, (I mod 9 <= 1 ; I mod 9 == 8)]
     X = [1,8,9,10,17,18,19,26,27,28,35,36,37,44,45,46,53,54,55,62,63,64,71,72,73,80,81,82,89,90,91,98,99,100]

   * n=9 k=3
     [1,9,1,2,1,8,2,4,6,2,7,9,4,5,8,6,3,4,7,5,3,9,6,8,3,5,7]

   * n=10, k=3 (SAT: 0.047s)
     [1,10,1,6,1,7,9,3,5,8,6,3,10,7,5,3,9,6,8,4,5,7,2,10,4,2,9,8,2,4]

   * n=17, k=3 (SAT: 1.573s)
     [4,17,5,12,16,4,11,15,5,2,4,10,2,13,5,2,12,14,11,17,3,16,10,15,3,9,7,13,3,12,11,8,14,10,7,9,6,17,16,15,8,13,7,6,1,9,1,14,1,8,6]

   * n=18, k=3 (SAT: 2.124s)
     [5,18,11,6,17,2,5,16,2,13,6,2,5,7,11,14,8,6,12,15,18,7,17,13,16,8,11,10,3,7,14,12,3,9,8,15,3,13,10,18,17,16,4,9,12,14,1,4,1,10,1,15,4,9]

   * n=19, k=3 (SAT: 2.536s)
     [6,19,17,4,18,5,9,6,4,12,16,5,11,4,6,14,9,5,15,8,17,19,12,18,11,13,9,16,8,1,14,1,10,1,15,12,11,8,17,13,7,19,18,10,16,14,2,3,7,2,15,3,2,13,10,3,7]

   * n=26, k=3 (CP:1899.1s SAT:24.477s)
     [20,26,24,7,25,23,6,14,17,2,12,7,2,6,9,2,16,21,13,7,6,20,14,12,9,19,17,24,26,23,25,22,13,16,9,5,12,14,18,21,8,5,20,15,17,19,13,5,11,8,16,10,24,23,22,26,25,18,8,15,11,21,10,3,4,19,1,3,1,4,1,3,11,10,4,15,18,22]

   * n=27, k=3 (SAT: 81.11s)
     [1,25,1,20,1,27,3,7,17,12,3,8,26,2,3,7,2,16,24,2,8,18,12,7,20,23,17,25,21,8,5,22,13,27,16,12,5,9,19,26,18,14,5,24,17,20,13,9,15,23,21,16,10,25,22,11,14,9,19,18,13,27,6,10,15,4,26,11,24,6,4,14,21,23,10,4,6,22,19,11,15]

   * n=28 k=3 (SAT: 101.348s)
     [10,24,13,17,4,6,28,26,20,4,16,10,6,9,4,15,13,22,19,6,25,17,10,9,27,23,24,16,3,20,13,15,3,9,26,28,3,21,19,17,22,18,2,11,16,2,25,15,2,23,20,24,27,14,7,11,12,8,19,21,18,26,7,22,28,5,8,11,14,12,7,5,25,23,1,8,1,5,1,18,27,21,12,14]

   * n=35 k=3 (SAT:354.236s)
     [9,16,10,19,22,23,26,14,27,35,9,29,6,10,15,28,17,21,16,6,9,33,14,19,10,32,6,22,30,23,15,31,34,26,17,16,27,14,1,21,1,29,1,19,28,35,15,8,13,18,22,25,17,23,24,33,8,20,32,30,26,21,13,31,27,8,2,34,18,2,12,29,2,28,11,4,13,25,20,24,4,35,5,12,7,4,11,18,5,33,30,32,7,3,5,31,12,3,11,20,7,3,34,25,24]

   * n=36 k=3 (SAT: 284.544s)
     [9,3,27,18,16,3,33,17,30,3,9,32,1,19,1,21,1,13,4,35,9,16,18,4,36,17,2,29,4,2,27,13,2,19,34,28,31,21,16,30,33,18,22,17,32,13,7,25,23,6,15,24,26,19,7,35,6,29,27,21,20,36,7,6,28,22,15,10,31,34,30,12,23,25,33,14,24,32,10,26,5,20,15,11,12,8,5,29,22,10,14,35,5,28,8,11,23,12,36,25,31,24,20,8,34,14,26,11]

  * n=37 k=3 (SAT: 335.774s)
    [2,17,11,2,37,22,2,23,18,7,5,29,19,10,11,31,5,7,34,17,28,26,5,33,10,7,11,18,22,36,32,23,19,35,1,10,1,17,1,30,24,29,37,20,27,15,18,31,26,28,3,22,19,34,3,23,25,33,3,13,6,15,21,32,20,24,36,6,14,35,30,29,27,13,6,26,16,15,28,31,37,12,25,14,21,20,8,13,34,9,24,33,4,16,12,8,32,4,14,9,27,30,4,36,8,35,21,12,25,9,16]

  * n=44 k=3 (SAT: 901.753s)
    [12,44,4,29,14,19,24,4,11,6,28,42,4,12,3,25,6,20,3,14,11,2,3,6,2,19,12,2,41,43,34,24,11,29,14,38,13,31,20,28,10,25,35,27,36,19,44,39,40,26,13,10,33,30,42,37,24,32,23,20,16,21,10,29,13,34,18,25,28,31,41,27,7,43,38,22,26,16,35,15,7,36,23,21,30,18,33,39,7,40,32,44,17,37,16,15,5,42,22,27,34,31,5,26,18,21,23,8,5,9,17,15,41,38,35,30,8,43,36,9,33,22,1,32,1,8,1,39,17,9,40,37]

  * n=45 k=3 (SAT: 3159.34s)
    [14,15,21,41,36,3,29,19,5,3,37,45,6,3,5,14,38,15,4,6,5,28,20,4,21,44,6,19,4,39,14,26,27,15,16,18,29,11,32,42,43,36,40,20,31,41,21,19,37,11,28,16,10,13,18,38,34,45,26,30,27,11,35,10,20,33,29,13,16,39,44,32,23,18,10,25,31,22,36,28,24,13,42,40,43,26,37,41,27,2,30,34,2,17,38,2,23,9,35,33,22,25,7,45,32,24,12,9,31,39,7,17,1,8,1,44,1,9,7,12,23,30,8,22,40,42,34,25,43,17,24,8,12,33,35]

  * n=46 K=3 (SAT: 3025.75s)
    [3,13,10,14,3,42,18,35,3,22,1,24,1,10,1,13,34,44,14,30,43,27,37,46,10,18,15,17,5,13,45,41,22,14,5,2,24,16,2,28,5,2,15,35,18,17,36,39,42,27,30,34,25,40,16,22,38,26,15,32,37,24,44,17,43,19,23,31,28,33,46,16,29,41,21,6,45,27,25,35,12,30,6,36,26,19,34,39,20,6,23,42,32,12,40,38,21,28,37,31,11,8,29,33,25,19,12,44,43,20,8,26,11,7,23,41,9,46,21,8,36,7,45,4,11,32,9,39,4,7,20,31,29,4,38,40,9,33]

  * n=53 k=3 (SAT: 8378.72s)
    [50,37,10,14,26,9,7,35,23,40,53,8,34,10,7,9,36,48,14,52,8,41,7,20,10,9,43,46,31,8,49,26,23,14,1,4,1,47,1,37,4,42,25,35,20,4,24,34,6,45,40,50,16,36,51,6,23,29,26,44,31,38,6,41,53,20,48,15,25,16,43,24,52,39,46,27,33,37,28,35,49,30,34,15,42,47,16,29,19,32,36,40,31,17,25,45,24,18,21,15,38,22,50,27,44,41,51,28,19,13,33,17,30,39,43,48,18,29,53,12,21,46,32,13,22,52,11,42,19,17,49,27,12,47,5,18,28,13,11,38,5,45,21,30,33,12,5,22,3,44,11,2,3,39,2,32,3,2,51]

  * n=54 k=3 (SAT:10981.8s)
    [2,43,28,2,46,16,2,6,14,9,35,18,11,23,6,50,8,40,48,9,52,6,16,14,11,8,37,31,12,9,18,28,42,53,8,44,11,23,14,16,15,12,49,51,38,43,35,45,54,18,17,46,47,27,12,7,15,30,40,31,28,23,33,7,37,39,50,48,17,4,41,7,15,52,4,42,34,36,29,4,44,27,35,38,19,21,17,53,30,43,24,31,49,45,32,51,33,25,46,40,47,26,37,54,19,39,13,21,29,27,20,34,41,22,36,24,48,50,42,30,13,10,38,25,19,44,52,32,26,21,33,20,10,1,13,1,22,1,29,45,24,53,49,10,5,39,34,51,47,25,5,36,20,3,41,26,5,3,54,22,32,3]

  * n=55 k=3 (SAT: 29052.6s)
    [7,27,28,3,14,45,6,3,7,11,15,3,2,6,49,2,7,50,2,14,6,11,55,37,46,4,15,9,47,27,4,28,8,11,14,4,18,9,53,13,40,8,15,39,51,20,42,9,44,54,8,45,26,13,43,18,52,27,21,41,28,37,48,24,49,29,20,13,50,30,36,46,17,38,18,34,47,25,55,26,21,40,22,39,32,35,33,20,24,42,17,23,53,44,31,29,51,45,43,37,30,41,21,25,54,22,26,36,17,52,34,48,38,24,49,23,19,32,46,50,33,35,40,39,47,29,31,12,22,25,16,30,42,1,55,1,19,1,44,23,12,10,43,41,36,34,53,16,51,5,32,38,10,12,33,5,19,35,31,54,48,5,52,10,16]

  * n=62 k=3 (SAT: 31845.8s)
    [50,47,41,38,1,46,1,48,1,31,54,25,40,43,2,62,44,2,49,9,2,16,8,35,29,32,52,20,60,9,45,8,55,51,61,36,37,25,16,9,8,31,38,39,41,34,53,27,20,47,42,50,46,40,29,16,48,43,32,35,26,44,58,25,59,54,15,57,49,20,33,56,36,31,37,27,45,14,62,52,34,38,15,39,29,51,41,26,55,60,17,32,14,42,40,35,61,47,15,46,53,43,50,27,33,48,44,14,17,36,24,19,37,28,26,34,30,22,49,23,54,58,45,39,59,57,17,18,56,4,21,19,52,11,4,24,42,51,33,4,22,62,28,23,55,11,18,30,13,5,60,19,21,12,53,5,7,11,61,10,24,5,13,22,7,18,12,23,6,3,10,28,7,3,21,6,13,3,30,12,58,10,6,57,59,56]

  * n=63 k=3 (SAT: 19022.0s)
    [45,5,40,52,53,63,20,5,56,47,49,18,34,5,46,25,23,36,59,50,15,7,22,26,1,57,1,20,1,7,18,61,30,62,27,8,15,7,33,48,23,25,58,40,8,22,45,34,20,18,26,3,15,8,36,3,52,47,53,3,49,46,27,30,23,56,60,25,22,63,50,54,33,55,41,42,12,26,59,44,51,31,34,57,40,39,16,29,48,12,27,36,45,61,30,43,62,38,24,28,6,58,12,16,37,47,33,6,46,52,49,32,53,31,6,35,41,29,42,11,16,50,56,24,44,39,54,60,28,55,9,11,51,63,21,17,38,48,59,43,9,57,37,11,32,31,19,29,24,14,9,35,10,17,13,61,21,28,41,62,58,42,4,10,14,39,19,4,13,44,2,17,4,2,10,38,2,32,21,14,37,54,13,43,51,55,19,35,60]

  * n=64 k=3 (SAT: 8439.43s)
    [26,10,61,24,42,4,48,30,28,46,4,62,10,58,36,4,7,53,38,9,64,22,39,10,7,35,56,26,24,9,18,63,7,47,41,14,23,28,30,9,34,37,27,50,22,59,45,42,33,18,14,36,54,24,26,48,46,38,60,55,23,35,39,57,61,14,28,22,18,30,27,53,58,12,62,34,41,52,49,37,51,47,33,56,23,64,12,25,36,16,42,17,45,20,50,63,38,35,27,12,43,44,39,46,48,59,16,54,40,17,34,31,21,25,20,55,33,37,41,60,32,57,29,16,11,53,61,17,49,47,52,58,51,8,21,20,11,62,45,25,56,13,8,31,43,50,44,19,11,40,64,8,29,32,6,13,21,15,5,63,2,6,54,2,5,59,2,19,6,13,5,55,1,15,1,31,1,3,49,57,60,3,29,52,51,3,32,19,43,15,40,44]


  K = 4

  * n=24 k=4 (SAT: 63730.3s (17h42min10.3s))
    [10,12,13,19,16,14,1,18,1,24,1,10,1,17,12,20,13,23,6,8,14,16,10,19,22,6,18,12,8,21,13,17,6,10,24,14,20,8,16,6,12,23,15,19,13,18,8,22,5,17,14,21,9,7,5,16,11,20,15,24,5,7,9,19,18,23,5,17,11,7,22,4,9,21,15,3,4,7,20,3,11,4,9,3,24,2,4,3,2,23,15,2,11,22,2,21]



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

*/

import util.
% import cp. % Faster for counting solutions
import sat. % Faster for generating one solution

main => go.

go ?=>
  nolog,
  N = 24,
  K = 4,
  printf("N: %d K: %d\n", N,K),
  langford(N, K, Solution),
  printf("Solution: %w\n", Solution),
  % fail,
  nl.

go => true.

%
% Get the first (if any) solutions for
% N in 2..40
%
go2 =>
  nolog,
  Found = [],
  foreach(N in 3..40, K in 4..4, N > K) 
    printf("N: %d K: %d\n", N,K),
    if time2(langford(N,K, Solution)) then
      flush(stdout),
      if nonvar(Solution) then 
         printf("Solution: %w\n", Solution),
         Found := Found ++ [[k=K,n=N]],
         println(found=Found)
      else 
         printf("No solution\n")
      end,
      nl,
      flush(stdout)
    end
  end,
  println(found=Found).


% Count the number of solutions
go3 => 
  Map = get_global_map(),
  foreach(N in 2..40) 
    foreach(K in 3..4, N > K)
      % println([n=N,k=K]),
      Map.put(count,0),
      ((langford(N,K, Solution), Map.put(count, Map.get(count)+1), fail) ; true),
      printf("N: %d K: %d = %d solutions\n", N, K, Map.get(count)),
      flush(stdout)
    end,
    nl
  end.


 
langford(N, K, Solution) =>

  if K = 2, not ((N mod 4 == 0; N mod 4 == 3)) then
     printf("There is no solution for N and K=2 unless N mod 4 == 0 or N mod 4 == 3"),
     fail
  end,
  if K = 3, not ((N mod 9 == 0; N mod 9 == 1 ; N mod 9 == 8)) then
     printf("There is no solution for N and K=3 unless N mod 9 == (0,1,8)"),
     fail
  end,

  NK = N*K,
  Solution = new_list(NK),
  Solution :: 1..N,

  Positions = new_list(NK),
  Positions :: 1..NK,

  all_distinct(Positions),

  Js = [], % temporary variables
  foreach(I in 1..N)
     J :: 1..K*N - ((K-1)*I),
     Js := Js ++ [J],
     foreach(C in 0..K-1)
       J2 #= J+(I*C)+C,
       Js := Js ++ [J2],
       element(J2, Solution, I),
       Positions[(I-1)*K+C+1] #= J2
     end
  end,
  
  % ensure that there are N occurrences of each number
  GCC = $[I-K : I in 1..N],
  global_cardinality(Solution, GCC),

  % symmetry breaking
  Solution[1] #< Solution[NK],

  Vars = Positions ++ Js ++ Solution,
  solve([ffc,split], Vars).