part2_sat.pi

import sat.

main =>
  Grid = read_file_lines(),
  {W,H} = {Grid[1].len, Grid.len},
  {Vs,Es} = to_graph(Grid,W,H),
  Cost = search(Vs.keys,Es.keys,{2,1},{W-1,H}),
  println(Cost).

search(Vs,Es,Src,Dest) = Cost =>
  path_d(Vs,Es,Src,Dest),
  Counts = new_array(Es.len),
  Counts :: 0..1,
  foreach (I in 1..Es.len)
    {From,To,B} = Es[I],
    member({To,From,B2}, Es),
    B #= 1 #=> B2 #= 0,
    Counts[I] #= B
  end,
  S #= sum(Counts),
  S :: 0..len(Es),
  solve([seq,$max(S),$report(printf("Best so far: %d\n",S))],[S,Vs,Es]),
  Cost = S.

to_graph(Grid,W,H) = Graph =>
  Actions = [north,east,south,west],

  Vs = new_set(),
  Es = new_set(),

  foreach (J in 1..H)
    foreach (I in 1..W)
      Cell = Grid[J,I],
      if Cell != '#' then
        Vs.put({{I,J}, _}),

        foreach (Action in Actions)
          {I2, J2} = inc(I,J,Action),
          if (I2 >= 1, I2 <= W, J2 >= 1, J2 <= H) then
            Target = Grid[J2,I2],
            if (Target != '#') then
              Es.put({{I,J},{I2,J2},_}),
            end
          end
        end
      end
    end
  end,
  println(sizes={Vs.size,Es.size}),
  Graph = {Vs,Es}.

inc(X,Y,north) = {X,Y-1}.
inc(X,Y,east)  = {X+1,Y}.
inc(X,Y,south) = {X,Y+1}.
inc(X,Y,west)  = {X-1,Y}.