/* 

  Advent of Code 2024 in Picat.

  Problem 23
  https://adventofcode.com/2024/day/23

  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 aoc_utils.

main => go.


/*
  Part 1
  Hyperfine 

  Benchmark 1: picat -g go 23.pi
    Time (mean ± σ):      84.3 ms ±  10.8 ms    [User: 66.2 ms, System: 16.4 ms]
    Range (min … max):    60.3 ms … 100.5 ms    27 runs

*/
go => 
  File = "23.txt",
  Lines = [Line.split("-"): Line in read_file_lines(File)],
  Graph = new_map(),
  foreach([A,B] in Lines)
    Graph.put(A,Graph.get(A,[])++[B]),
    Graph.put(B,Graph.get(B,[])++[A])
  end,
  Sum = 0,
  foreach(A in Graph.keys, B in Graph.get(A), C in Graph.get(B), membchk(A,Graph.get(C)),         
         [A,B,C] == sort([A,B,C]))
    if (A.first == 't' ; B.first == 't' ; C.first == 't') then
      Sum := Sum + 1
    end
  end,
  println(Sum).


%
% Part 2
% 
% 5.2s
% 
% Note: This uses the maxsat solver.
% Without maxsat, i.e. plain SAT solver, it takes about 16s
%
go2 => 
  File = "23.txt",
  Lines = [Line.split("-"): Line in read_file_lines(File)],
  [M,Rev] = create_adj_matrix(Lines),
  clique(M, Clique,_Card,_), % Find the max clique
  println([Rev.get(C) : C in Clique].sort.join(",")).


% Create a adjacency matrix
create_adj_matrix(Lines) = [M,Rev] =>
  Map = new_map(), % name-> id
  Id = 1,
  foreach([A,B] in Lines)
    if not Map.has_key(A) then
       Map.put(A,Id),
       Id := Id + 1
    end,
    if not Map.has_key(B) then
       Map.put(B,Id),
       Id := Id + 1
    end
  end,
  % Reverse lookup: id -> name
  Rev = new_map([V=K : K=V in Map]),
  N = Rev.keys.len,
  M = new_array(N,N),
  bind_vars(M,0),
  foreach([A,B] in Lines)
    AI = Map.get(A),
    BI = Map.get(B),
    M[AI,BI] := 1,
    M[BI,AI] := 1
  end.


%
% The model below is slightly altered from my
% http://www.hakank.org/picat/clique.pi
% 
%

%
% clique(Graph,Clique,Cardinality,Type)
%
clique(G, Clique, Card, Type) =>
   NumNodes = G.length,

   % The clique found, here represented as a boolean list
   CliqueBool = new_list(NumNodes),
   CliqueBool :: 0..1,
   
   % cardinality of the clique
   Card #= sum(CliqueBool),
   Card #> 0,

   % check the cliques in G
   check_cliques(G,CliqueBool),
   % Either search for all cliques or a clique with 
   % maximum cardinality.
   Vars = CliqueBool ++ Card,
   if Type == all ; ground(Card) then
       solve($[], Vars)
     else
    solve($[maxsat,max(Card),report(printf("card: %d\n",Card))],Vars)
   end,
   % for the result as set representation in Clique
   boolean_to_set(CliqueBool,Clique).
   
%
% convert a list of boolean to a "set"
%
boolean_to_set(List,Clique) =>
   List :: 0..1,
   Clique = [I : {C,I} in zip(List,1..List.length), C==1].

%
% This is kind of backward but it is the whole thing:
% If there is a connection between nodes I and J (I \= J) then
% there should be a node from I to J in G.
%
check_cliques(G, CliqueBool) =>
   Len = length(CliqueBool),
   foreach({C1,I} in zip(CliqueBool,1..Len), {C2,J} in zip(CliqueBool,1..Len))
      if I =\= J, G[I,J] == 0 then      
          #~C1 #\/ #~C2
      end
   end.