/*

  Langford's number problem L(2,N) in Picat.

  Langford's number problem (CSP lib problem 24)
  http://www.csplib.org/prob/prob024/
  """
  Arrange 2 sets of positive integers 1..k to a sequence,
  such that, following the first occurence of an integer i, 
  each subsequent occurrence of i, appears i+1 indices later
  than the last. 
  For example, for k=4, a solution would be 41312432
  """
  
  * John E. Miller: Langford's Problem
    http://www.lclark.edu/~miller/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


  Note: For k=4 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.

  Note: There are only solutions when K mod 4 == 0 or K mod 4 == 3.

  - For a generalized version L(k,n) where k >= 2, see http://hakank.org/langford_generalized.pi
  - For Nickerson's variant, see http://hakank.org/langford_nickerson.pi

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

*/

import util.
import cp.

main => go.

go =>
    K = 4,
    printf("K: %d\n", K),
    time2($langford(K, Solution, Position)),
    printf("Solution: %w\n", Solution),
    printf("Position: %w\n", Position).

%
% Get the first (if any) solutions for K in 2..40
%
go2 => 
  foreach(K in 2..60) 
     printf("K: %d\n", K),
     if time2(langford(K, Solution, Position)) then
         if nonvar(Solution) then 
           printf("Solution: %w\n", Solution)
           % printf("Position: %w\n", Position)
         else 
           printf("No solution\n")
         end,
        printf("\n"),
        flush(stdout)
     end
  end.

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


 
langford(K, Solution, Position) =>

  if not ((K mod 4 == 0; K mod 4 == 3)) then
     println("There is no solution for K unless K mod 4 == 0 or K mod 4 == 3"),
     fail
  end,

  K2 = 2*K,
  Position = new_list(K2),
  Position :: 1..K2,

  Solution = new_list(K2),
  Solution :: 1..K,

  % all_different(Position),
  all_distinct(Position),

  % symmetry breaking:
  Solution[1] #< Solution[K2],

  foreach(I in 1..K)
      Position[K+I] #= Position[I] + I+1,
      element(Position[I],Solution,I),  
      element(Position[K+I],Solution,I)
  end,

  Vars = Solution ++ Position,
  solve([ffc,updown], Vars).