/* 

  Drinker paradox in Picat.

  From Adrian Groza "Modelling Puzzles in First Order Logic"
  """
  Puzzle 141. Drinker paradox
  
  For any pub, there is always a customer in the pub so that, if he is drinking, every cus-
  tomer in the pub is drinking. (taken from Smullyan (2011)).
  """

  The point of the paradox is that either all is drinking or none is drinking which
  contradicts each other. Perhaps this is not as powerful as the logic proof that 
  Groza's Prover9 encoding yields (page 331)
  """
  Prover9 outputs a three-step proof. By negating the goal, it infers 
  both ¬drinks(f1(x)) [...] and drinks(x) that contradict
  each other.
  """


  There are two solutions:

  [0,0,0,0,0]
  [1,1,1,1,1]

  i.e. either none is drinking or all is drinking.

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

*/

import cp.

main => go.

go =>
  N = 5, % Pick some arbitrary size of the pub's customers

  X = new_list(N),
  X :: 0..1, % 1: X[I] drinks

  foreach(I in 1..N)
    X[I] #= 1 #=> sum(X) #= N
  end,

  solve(X),
  println(X),
  fail,
  
  nl.


% An alternative formulation.
% If there is at least one that drinks then all drinks.
% 
go2 =>
  N = 5,

  X = new_list(N),
  X :: 0..1, % 1: X[I] drinks

  sum(X) #>= 1 #=> sum(X) #= N,

  solve(X),
  println(X),
  fail,
  
  nl.