/* 

  A special parking lot puzzle in Picat.

  From https://puzzling.stackexchange.com/questions/55853/a-special-parking-lot
  """
  There is a special kind of parking lot that stores special 1x1 cars that only can move to 
  adjacent squares not including diagonals if they are empty (provided no car occupies the square). 
  Every car occupies exactly one square and no more. The exit is beside the top left corner of 
  the parking lot.

  Because everyone is a perfect driver, everyone parks in a way that every car can exit without 
  moving any other cars.

  Currently, there are 24 cars parked in a 7 by 7 parking lot of this kind. Can you fit more cars 
  in a different arrangement?
  """

  Yes, there can be atmost 28 cars for a 7x7 parking lot, e.g. 

  z = 28
  X:
  _ _ c c c c c 
  c _ _ _ _ _ _ 
  c _ c c c c c 
  c _ c c c c c 
  c _ c _ _ _ _ 
  _ _ _ _ c _ c 
  c c c c c _ c 


  "c" is a car and "_" is the free spaces at the parking lot.
  There are 934 optimal solutions.

  Note: This model uses the scc_grid/1 constraint and assumes that the
  free runway (the '_') is connected. There are other solution in
  which there are "islands", i.e. which are not connected
  to the exit (X[1,1]), but these are not shown with the model.


  The number of optimal solutions for some other dimensions (n x n):
  [n = 2,zopt = 2,count = 2]
  [n = 3,zopt = 5,count = 2]
  [n = 4,zopt = 8,count = 26]
  [n = 5,zopt = 14,count = 4]
  [n = 6,zopt = 21,count = 24]
  [n = 7,zopt = 28,count = 934]
  [n = 8,zopt = 38,count = 12]
  [n = 9,zopt = 50,count = 16]



  All 4 solutions for 5x5:
  zopt = 14
  X:
  _ c c _ c 
  _ c c _ c 
  _ c c _ c 
  _ _ _ _ c 
  c c c _ c 

  X:
  _ _ _ _ c 
  c c c _ c 
  c c c _ c 
  _ _ _ _ c 
  c c c _ c 

  X:
  _ _ _ _ c 
  c c c _ c 
  c c c _ c 
  _ _ _ _ _ 
  c c c c c 

  X:
  _ c c _ c 
  _ c c _ c 
  _ c c _ c 
  _ _ _ _ _ 
  c c c c c 


  Here are some solutions for larger sizes:

  8x8 (29.5s)
     z = 38
     X:
     _ _ _ _ c c _ c 
     c c c _ c c _ c 
     c c c _ c c _ c 
     _ _ _ _ _ _ _ c 
     c c c c c c _ c 
     c c c c c c _ c 
     _ _ _ _ _ _ _ c 
     c c c c c c _ c 


  9x9 (17.01s)
    z = 50
    X:
    _ c c c c c c c c 
    _ _ _ _ _ _ _ _ _ 
    c c c c c c c _ c 
    c c c c c c c _ c 
    _ _ _ _ _ _ _ _ c 
    c c c c c c c _ c 
    c c c c c c c _ c 
    _ _ _ _ _ _ _ _ _ 
    c c c c c c c c c 


  Another experiment
  ------------------

  If we restrict that there can be atmost 2 free spaces around each car
  (Ts :: 0..2), then there might be sligly less optimal number of cars, 
  and fewer optimal solutions:

    [n = 2,zopt = 2,count = 2]
    [n = 3,zopt = 5,count = 2]
    [n = 4,zopt = 8,count = 2]
    [n = 5,zopt = 13,count = 10]
    [n = 6,zopt = 21,count = 2]
    [n = 7,zopt = 27,count = 2]
    [n = 8,zopt = 37,count = 2]
    [n = 9,zopt = 49,count = 2]


  For example here are the two optimal (and symmetric) solutions for 7x7. 
  The number of maximum cars is now 27, not 28.

    zopt = 27
    X:
    _ _ c c c c c 
    _ c c _ _ _ _ 
    _ c c _ c c _ 
    _ c c _ c c _ 
    _ c c c c c _ 
    _ _ _ _ _ _ _ 
    c c c c c c c 


    Ts:
    [2,1,1,1,1,1,1]
    [2,2,1,2,2,2,2]
    [2,1,1,2,2,2,2]
    [2,1,1,1,1,1,2]
    [2,2,1,2,1,2,2]
    [2,2,2,2,2,2,2]
    [1,1,1,1,1,1,1]

    X:
    _ _ _ _ _ _ c 
    _ c c c c _ c 
    c c c c c _ c 
    c _ _ _ c _ c 
    c _ c c c _ c 
    c _ c c c _ c 
    c _ _ _ _ _ c 

    Ts:
    [2,2,2,2,2,2,1]
    [1,2,1,1,2,2,1]
    [1,1,1,1,1,2,1]
    [1,2,2,1,2,2,1]
    [1,2,2,1,1,2,1]
    [1,2,2,1,2,2,1]
    [1,2,2,2,2,2,1]


  For 8x8
    zopt = 37
    X:
    _ c c _ _ _ _ c 
    _ c c _ c c _ c 
    _ c c _ c c _ c 
    _ c c _ c c _ c 
    _ c c _ c c _ c 
    _ c c _ c c _ c 
    _ _ _ _ c c _ c 
    c c c c c _ _ c 

    Ts:
    [1,1,1,2,2,2,2,1]
    [2,1,1,2,2,2,2,1]
    [2,1,1,2,1,1,2,1]
    [2,1,1,2,1,1,2,1]
    [2,1,1,2,1,1,2,1]
    [2,2,2,2,1,1,2,1]
    [2,2,2,2,1,2,2,1]
    [1,1,1,1,1,1,2,1]

    X:
    _ _ _ _ _ _ _ c 
    c c c c c c _ c 
    c c c c c c _ c 
    _ _ _ _ _ _ _ c 
    _ c c c c c c c 
    _ c c c c c c _ 
    _ _ _ _ _ _ _ _ 
    c c c c c c c c 

    Ts:
    [1,2,2,2,2,2,2,1]
    [1,1,1,1,1,2,2,1]
    [1,1,1,1,1,2,2,1]
    [2,2,2,2,2,2,2,1]
    [2,2,1,1,1,1,1,1]
    [2,2,1,1,1,1,2,1]
    [2,2,2,2,2,2,2,2]
    [1,1,1,1,1,1,1,1]




  And for 9x9 (and 1..2 free space around each car) with a neat
  symmetric form:

   zopt = 49
   X:
   _ c c c c c c c c 
   _ _ _ _ _ _ _ _ _ 
   c c c c c c c c _ 
   c c c c c c c c _ 
   _ _ _ _ _ _ _ _ _ 
   _ c c c c c c c c 
   _ c c c c c c c c 
   _ _ _ _ _ _ _ _ _ 
   c c c c c c c c c 


   Ts:
   [1,2,1,1,1,1,1,1,1]
   [2,2,2,2,2,2,2,2,2]
   [1,1,1,1,1,1,1,2,2]
   [1,1,1,1,1,1,1,2,2]
   [2,2,2,2,2,2,2,2,2]
   [2,2,1,1,1,1,1,1,1]
   [2,2,1,1,1,1,1,1,1]
   [2,2,2,2,2,2,2,2,1]
   [1,1,1,1,1,1,1,1,1]

   X:
   _ _ c c _ _ _ _ c 
   c _ c c _ c c _ c 
   c _ c c _ c c _ c 
   c _ c c _ c c _ c 
   c _ c c _ c c _ c 
   c _ c c _ c c _ c 
   c _ c c _ c c _ c 
   c _ c c _ c c _ c 
   c _ _ _ _ c c _ c 


  Ts:
  [1,2,1,1,2,2,2,2,1]
  [2,2,1,1,2,2,2,2,1]
  [1,2,1,1,2,1,1,2,1]
  [1,2,1,1,2,1,1,2,1]
  [1,2,1,1,2,1,1,2,1]
  [1,2,1,1,2,1,1,2,1]
  [1,2,1,1,2,1,1,2,1]
  [1,2,2,2,2,1,1,2,1]
  [1,2,2,2,2,1,1,1,1]
  


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

*/

import util.
import sat.
% import cp.

main => go.

%
% Find an optimal solution.
%
go ?=>
  nolog,
  N = 8,
  a_special_parking_lot(N, X,Ts,Z),
  println(z=Z),
  println("X:"),
  foreach(I in 1..N)
    foreach(J in 1..N)
      printf("%w ", cond(X[I,J] == 0,"c","_"))
    end,
    nl
  end,
  nl,
  println("Ts:"),
  foreach(Row in Ts)
    println(Row.to_list)
  end,
  nl,  
  nl.
go => true.

%
% Show all the optimal solutions.
%
go2 ?=>
  nolog,
  N = 8,
  a_special_parking_lot(N, _X,_Ts,ZOpt),
  println(zopt=ZOpt),
  a_special_parking_lot(N, X,Ts,ZOpt),
  println("X:"),
  foreach(I in 1..N)
    foreach(J in 1..N)
      printf("%w ", cond(X[I,J] == 0,"c","_"))
    end,
    nl
  end,
  nl,
  println("Ts:"),
  foreach(Row in Ts)
    println(Row.to_list)
  end,
  nl,
  fail,
  nl.
go2 => true.


%
% Count the number of optimal solutions
% 
go3 ?=>
  nolog,
  foreach(N in 1..9)
    if a_special_parking_lot(N, _,_,ZOpt) then
      Count = count_all(a_special_parking_lot(N,_,_,ZOpt)),
      println([n=N,zopt=ZOpt,count=Count])
    end
  end,
  nl.
go3 => true.


a_special_parking_lot(N, X,Ts,Z) =>

  Car = 0,
  Free = 1,
  
  X = new_array(N,N),
  X :: Car..Free, % 1: the space is free to run, 0: a car is placed, 

  % Number of free spaces around a place
  Ts = new_array(N,N),
  Ts :: 0..4,
  % Ts :: 0..2, % Restrict to atmost two free spaces for each car. 


  X[1,1] #= Free, % the exit (must be empty)
  % The cars are 0s, the 1s are the connected runway
  Z :: 1..N*N,
  Z #= sum([X[I,J] #= Car : I in 1..N, J in 1..N]),

  % All placed cars (the 0s) must have at least one runway connection
  foreach(I in 1..N, J in 1..N)
    Ts[I,J] #= sum([X[I+A,J+B] : A in -1..1, B in -1..N,
                                         abs(A)+abs(B) == 1,
                                         I+A >= 1, I+A <= N,
                                         J+B >= 1, J+B <= N]) #> 0,
    X[I,J] #= Car #=> Ts[I,J] #> 0
  end,

  % Make all the free space connected
  scc_grid(X),

  Vars = X.vars ++ Ts.vars,
  if var(Z) then
    solve($[maxsat,ff,split,max(Z)],Vars)
  else
    solve($[ff,split],Vars)  
  end.