/* 

  Inner circle in Picat.

  From Niyaz KC: "Reasoning with Constraints: A Puzzle in Logic, Sets, and Automated Proof"
  https://medium.com/puzzle-sphere/reasoning-with-constraints-a-puzzle-in-logic-sets-and-automated-proof-a5df3983f1ea
  """
  The Scenario

  There are five people in this example: Alice, Bob, Clara, Dan, and Eva. There are three sets:

  Set A: Those who enjoy algebra
  Set B: Those who own a cat
  Set C: Those who always tell the truth

  There is an exclusive club called the "Inner Circle" . Membership to the club is allowed 
  if and only if they are in all three sets (i.e., in A ∩ B ∩ C).

  We know the following facts about all the five people. They are:

  - If Alice is in Set A, then Bob is in Set C.
  - Clara is not in Set B.
  - If Bob is in Set B, then Clara is in Set A.
  - Either Alice is in Set B or Clara is in Set C (or both).
  - Dan is in Set A if and only if Eva is in Set B.
  - Eva is in Set C.
  - If Clara is in Set A, then Alice is in Set C.

  The Goal

  We have to find out who among the five qualifies for the Inner Circle. That is, who is 
  eligible to be all three sets A, B and C; without contradicting the known statements.

  ...

  Running this code in Python, we get the output of:

  Inner Circle members (possibly):
   Alice
   Bob
   Dan
   Eva
  """


  Hmm, there is a lot (1152) of solutions for this, and what I can see is that
  there's no person(s) that are inside the Inner Circle in all solutions . 

  OK, one interpretation of this is that a person is in the InnerCircle
  is they are in the InnerCircle in _any_ of the 1152 solutions. 
  With this interpretation then the solution is the same as in the post:

  num_solutions = 1152

  Inner Circle members (possibly):
  Alice
  Bob
  Dan
  Eva

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

*/

import util.
import cp.

main => go.

go ?=>
  N = 5,
  People = [Alice, Bob, Clara, Dan, Eva],
  People = [1,2,3,4,5],
  PeopleS = ["Alice", "Bob", "Clara", "Dan", "Eva"],
  
  [A,B,C] = [1,2,3],
  
  Sets = new_array(N,3),
  Sets :: 0..1,
  
  % There is an exclusive club called the "Inner Circle" . Membership to the club is allowed 
  % if and only if they are in all three sets (i.e., in A ∩ B ∩ C).

  % We know the following facts about all the five people. They are:

  % - If Alice is in Set A, then Bob is in Set C.
  Sets[Alice,A] #= 1 #=> Sets[Bob,C] #= 1,  

  % - Clara is not in Set B.
  Sets[Clara,B] #= 0,

  % - If Bob is in Set B, then Clara is in Set A.
  Sets[Bob,B] #= 1 #=> Sets[Clara,A] #= 1,
  
  % - Either Alice is in Set B or Clara is in Set C (or both).
  (Sets[Alice,B] #= 1 #\/ Sets[Clara,C] #= 1),

  % - Dan is in Set A if and only if Eva is in Set B.
  Sets[Dan,A] #= 1 #<=> Sets[Eva,B] #= 1,
    
  % - Eva is in Set C.
  Sets[Eva,C] #= 1,
  
  % - If Clara is in Set A, then Alice is in Set C.
  Sets[Clara,A] #= 1 #=> Sets[Alice,C] #= 1,

  % Who is the Inner Circle?
  InnerCircle = new_list(N),
  InnerCircle :: 0..1,
  foreach(P in 1..N)
    InnerCircle[P] #= 1 #= (sum([Sets[P,S] : S in 1..3]) #= 3)
  end,

  % We have to find out who among the five qualifies for the Inner Circle. That is, who is 
  % eligible to be all three sets A, B and C; without contradicting the known statements.

  Vars = Sets.array_matrix_to_list_matrix.flatten ++ InnerCircle,
  All = solve_all(Vars),
  println(num_solutions=All.len),
  nl,
  
  % Check if a person is in the Inner Cicle in any of the 1152 solutions:
  Sol = new_list(N),
  bind_vars(Sol,0),
  foreach(L in All)
    T = L.drop(3*5),
    foreach(I in 1..N, T[I] == 1)
      Sol[I] := Sol[I] + 1
    end
  end,
  println("Inner Circle members (possibly):"),
  foreach(I in 1..N,Sol[I] > 0)
    println(PeopleS[I])
  end,
  nl,
  
  fail, % Check for alternative solutions.

  nl.
go => true.