In [47]:

    

import functools
import Numberjack

import forge
from data.logic import _util


Beth = 0
Charles = 1
David = 2
Frank = 3
Jessica = 4
Karen = 5
Taylor = 6

Weight = 0
Leight = 1
Whockey = 2
Lhockey = 3
asteroids = 4
baffle = 5
defender = 6
pacman = 7
qix = 8
invaders = 9

model = Numberjack.Model()

names = ['Beth', 'Charles', 'David', 'Frank', 'Jessica', 'Karen', 'Taylor']
n_names = list(range(len(names)))
activity_names = [
  'W 8ball', 'L 8ball',
  'W hockey', 'L hockey',
  'Asteroids', 'Baffle Ball', 'Defender', 'Pac-Man', 'Qix', 'Space Invaders',
]
people = list(range(len(names)))
rounds = list(range(6))
grid = []
for x in names:
  row = []
  grid.append(row)
  for y in rounds:
    row.append(Numberjack.Variable(0, len(activity_names) - 1, '%s_%s' % (x, y+1)))

units = {
  ' ': 0,
  'L': 1,
  'W': 2,
}
def parse_outcomes(s):
  result = {}
  for line in s.split('\n'):
    line = line.strip()
    if not line:
      continue
    lower, upper, spec = int(line[0]), int(line[1]), line[3:]
    acc = 0
    for i, c in enumerate(spec):
      acc += units[c] * (3 ** i)
    result[acc] = (lower, upper)
  return result

@functools.lru_cache()
def game_vector(n, g):
  return Numberjack.Sum(
    [grid[n][r] == g for r in rounds],
    coefs=[1, 2, 4, 8, 16, 32],
  )

@functools.lru_cache()
def game_count(n, g):
  return Numberjack.Cardinality(grid[n], g)

@functools.lru_cache()
def game_win_and_loss_vector(n, w, l):
  return Numberjack.Sum(
    [(grid[n][r] == w) for r in rounds] + [(grid[n][r] == l) for r in rounds],
    coefs=[2 * (3 ** r) for r in rounds] + [1 * (3 ** r) for r in rounds],
  )

# Setup.
# Eight-ball and hockey are always occupied. Other things are optional, limit 1.
for r in rounds:
  model.add(Numberjack.Gcc(
    [grid[n][r] for n in range(len(names))],
    {
      Weight: (1, 1),
      Leight: (1, 1),
      Whockey: (1, 1),
      Lhockey: (1, 1),
      asteroids: (0, 1),
      baffle: (0, 1),
      defender: (0, 1),
      pacman: (0, 1),
      qix: (0, 1),
      invaders: (0, 1),
    }
  ))
# No one played the same machine twice (or won more than 3 games).
for n in range(len(names)):
  model.add(Numberjack.Gcc(
    grid[n],
    {
      Weight: (0, 3),
      Leight: (0, 1),
      Whockey: (0, 3),
      Lhockey: (0, 1),
      asteroids: (0, 1),
      baffle: (0, 1),
      defender: (0, 1),
      pacman: (0, 1),
      qix: (0, 1),
      invaders: (0, 1),
    }
  ))
# The tournament is single elimination. That means:
# 1. Every round has (win + loss)*2. Implemented with first GCC.
# 2. There are 12 total plays over 6 matches. Implemented above.
# 3. "In the first 3 periods 3 different pairs of people played..."
#    Implies each player can only play 1 <game> in first 3 rounds.
#for n in range(len(names)):
#  model.add(Numberjack.Sum([
#    [(grid[n][r] == Weight) | (grid[n][r] == Leight) for r in rounds[:3]]
#  ]) == 1)

#    123456
# 11 L
# 01 W  L
# 01 W  W L
# 01 W  W W
# 01    L
# 01    W L
# 01    W W
# 11  L
# 01  W  L
# 01  W  WL
# 01  W  WW
# 11   L
# 01   W L
# 01   W WL
# 01   W WW
# 4. First loss is last game.
outcomes = parse_outcomes("""
  11 L
  01 W  L
  01 W  W L
  01 W  W W
  01    L
  01    W L
  01    W W
  11  L
  01  W  L
  01  W  WL
  01  W  WW
  11   L
  01   W L
  01   W WL
  01   W WW
""")
if False:
  model.add(Numberjack.Gcc(
    [game_win_and_loss_vector(n, Weight, Leight) for n in range(len(names))],
    outcomes,
  ))
  model.add(Numberjack.Gcc(
    [game_win_and_loss_vector(n, Whockey, Lhockey) for n in range(len(names))],
    outcomes,
  ))

#for n in range(len(names)):
  #model.add((
  #  Numberjack.Conjunction([grid[n][r] != Leight for r in rounds]) |
  #  (game_vector(n, Leight) > game_vector(n, Weight))
  #))
  #model.add((
  #  Numberjack.Conjunction([grid[n][r] != Lhockey for r in rounds]) |
  #  (game_vector(n, Lhockey) > game_vector(n, Whockey))
  #))

#1a: One person only played Qix.
Numberjack.Sum(
  [game_count(n, qix) == 1]
)


solver = model.load('MiniSat')
print(str(model))
solver.solve()

if solver.is_unsat():
  print('Impossible')
else:
  for i, n in enumerate(names):
    print(n, _util.numberjack_solution(game_win_and_loss_vector(i, Weight, Leight)))
  print('\t'.join(['name', '1', '2', '3', '4', '5', '6']))
  for y, row in enumerate(grid):
    result = [names[y]]
    for x, variable in enumerate(row):
      value = variable.get_value()
      result.append(activity_names[value][:7])
    print('\t'.join(result))


    

    




assign:
  Beth_1 in {0..9}
  Charles_1 in {0..9}
  David_1 in {0..9}
  Frank_1 in {0..9}
  Jessica_1 in {0..9}
  Karen_1 in {0..9}
  Taylor_1 in {0..9}
  Beth_2 in {0..9}
  Charles_2 in {0..9}
  David_2 in {0..9}
  Frank_2 in {0..9}
  Jessica_2 in {0..9}
  Karen_2 in {0..9}
  Taylor_2 in {0..9}
  Beth_3 in {0..9}
  Charles_3 in {0..9}
  David_3 in {0..9}
  Frank_3 in {0..9}
  Jessica_3 in {0..9}
  Karen_3 in {0..9}
  Taylor_3 in {0..9}
  Beth_4 in {0..9}
  Charles_4 in {0..9}
  David_4 in {0..9}
  Frank_4 in {0..9}
  Jessica_4 in {0..9}
  Karen_4 in {0..9}
  Taylor_4 in {0..9}
  Beth_5 in {0..9}
  Charles_5 in {0..9}
  David_5 in {0..9}
  Frank_5 in {0..9}
  Jessica_5 in {0..9}
  Karen_5 in {0..9}
  Taylor_5 in {0..9}
  Beth_6 in {0..9}
  Charles_6 in {0..9}
  David_6 in {0..9}
  Frank_6 in {0..9}
  Jessica_6 in {0..9}
  Karen_6 in {0..9}
  Taylor_6 in {0..9}
  
subject to:
   Gcc(Beth_1 Charles_1 David_1 Frank_1 Jessica_1 Karen_1 Taylor_1 | 0 in [1,1] 1 in [1,1] 2 in [1,1] 3 in [1,1] 4 in [0,1] 5 in [0,1] 6 in [0,1] 7 in [0,1] 8 in [0,1] 9 in [0,1] )
   Gcc(Beth_2 Charles_2 David_2 Frank_2 Jessica_2 Karen_2 Taylor_2 | 0 in [1,1] 1 in [1,1] 2 in [1,1] 3 in [1,1] 4 in [0,1] 5 in [0,1] 6 in [0,1] 7 in [0,1] 8 in [0,1] 9 in [0,1] )
   Gcc(Beth_3 Charles_3 David_3 Frank_3 Jessica_3 Karen_3 Taylor_3 | 0 in [1,1] 1 in [1,1] 2 in [1,1] 3 in [1,1] 4 in [0,1] 5 in [0,1] 6 in [0,1] 7 in [0,1] 8 in [0,1] 9 in [0,1] )
   Gcc(Beth_4 Charles_4 David_4 Frank_4 Jessica_4 Karen_4 Taylor_4 | 0 in [1,1] 1 in [1,1] 2 in [1,1] 3 in [1,1] 4 in [0,1] 5 in [0,1] 6 in [0,1] 7 in [0,1] 8 in [0,1] 9 in [0,1] )
   Gcc(Beth_5 Charles_5 David_5 Frank_5 Jessica_5 Karen_5 Taylor_5 | 0 in [1,1] 1 in [1,1] 2 in [1,1] 3 in [1,1] 4 in [0,1] 5 in [0,1] 6 in [0,1] 7 in [0,1] 8 in [0,1] 9 in [0,1] )
   Gcc(Beth_6 Charles_6 David_6 Frank_6 Jessica_6 Karen_6 Taylor_6 | 0 in [1,1] 1 in [1,1] 2 in [1,1] 3 in [1,1] 4 in [0,1] 5 in [0,1] 6 in [0,1] 7 in [0,1] 8 in [0,1] 9 in [0,1] )
   Gcc(Beth_1 Beth_2 Beth_3 Beth_4 Beth_5 Beth_6 | 0 in [0,3] 1 in [0,1] 2 in [0,3] 3 in [0,1] 4 in [0,1] 5 in [0,1] 6 in [0,1] 7 in [0,1] 8 in [0,1] 9 in [0,1] )
   Gcc(Charles_1 Charles_2 Charles_3 Charles_4 Charles_5 Charles_6 | 0 in [0,3] 1 in [0,1] 2 in [0,3] 3 in [0,1] 4 in [0,1] 5 in [0,1] 6 in [0,1] 7 in [0,1] 8 in [0,1] 9 in [0,1] )
   Gcc(David_1 David_2 David_3 David_4 David_5 David_6 | 0 in [0,3] 1 in [0,1] 2 in [0,3] 3 in [0,1] 4 in [0,1] 5 in [0,1] 6 in [0,1] 7 in [0,1] 8 in [0,1] 9 in [0,1] )
   Gcc(Frank_1 Frank_2 Frank_3 Frank_4 Frank_5 Frank_6 | 0 in [0,3] 1 in [0,1] 2 in [0,3] 3 in [0,1] 4 in [0,1] 5 in [0,1] 6 in [0,1] 7 in [0,1] 8 in [0,1] 9 in [0,1] )
   Gcc(Jessica_1 Jessica_2 Jessica_3 Jessica_4 Jessica_5 Jessica_6 | 0 in [0,3] 1 in [0,1] 2 in [0,3] 3 in [0,1] 4 in [0,1] 5 in [0,1] 6 in [0,1] 7 in [0,1] 8 in [0,1] 9 in [0,1] )
   Gcc(Karen_1 Karen_2 Karen_3 Karen_4 Karen_5 Karen_6 | 0 in [0,3] 1 in [0,1] 2 in [0,3] 3 in [0,1] 4 in [0,1] 5 in [0,1] 6 in [0,1] 7 in [0,1] 8 in [0,1] 9 in [0,1] )
   Gcc(Taylor_1 Taylor_2 Taylor_3 Taylor_4 Taylor_5 Taylor_6 | 0 in [0,3] 1 in [0,1] 2 in [0,3] 3 in [0,1] 4 in [0,1] 5 in [0,1] 6 in [0,1] 7 in [0,1] 8 in [0,1] 9 in [0,1] )
   Gcc((2*(Beth_1 == 0) + 6*(Beth_2 == 0) + 18*(Beth_3 == 0) + 54*(Beth_4 == 0) + 162*(Beth_5 == 0) + 486*(Beth_6 == 0) + (Beth_1 == 1) + 3*(Beth_2 == 1) + 9*(Beth_3 == 1) + 27*(Beth_4 == 1) + 81*(Beth_5 == 1) + 243*(Beth_6 == 1)) (2*(Charles_1 == 0) + 6*(Charles_2 == 0) + 18*(Charles_3 == 0) + 54*(Charles_4 == 0) + 162*(Charles_5 == 0) + 486*(Charles_6 == 0) + (Charles_1 == 1) + 3*(Charles_2 == 1) + 9*(Charles_3 == 1) + 27*(Charles_4 == 1) + 81*(Charles_5 == 1) + 243*(Charles_6 == 1)) (2*(David_1 == 0) + 6*(David_2 == 0) + 18*(David_3 == 0) + 54*(David_4 == 0) + 162*(David_5 == 0) + 486*(David_6 == 0) + (David_1 == 1) + 3*(David_2 == 1) + 9*(David_3 == 1) + 27*(David_4 == 1) + 81*(David_5 == 1) + 243*(David_6 == 1)) (2*(Frank_1 == 0) + 6*(Frank_2 == 0) + 18*(Frank_3 == 0) + 54*(Frank_4 == 0) + 162*(Frank_5 == 0) + 486*(Frank_6 == 0) + (Frank_1 == 1) + 3*(Frank_2 == 1) + 9*(Frank_3 == 1) + 27*(Frank_4 == 1) + 81*(Frank_5 == 1) + 243*(Frank_6 == 1)) (2*(Jessica_1 == 0) + 6*(Jessica_2 == 0) + 18*(Jessica_3 == 0) + 54*(Jessica_4 == 0) + 162*(Jessica_5 == 0) + 486*(Jessica_6 == 0) + (Jessica_1 == 1) + 3*(Jessica_2 == 1) + 9*(Jessica_3 == 1) + 27*(Jessica_4 == 1) + 81*(Jessica_5 == 1) + 243*(Jessica_6 == 1)) (2*(Karen_1 == 0) + 6*(Karen_2 == 0) + 18*(Karen_3 == 0) + 54*(Karen_4 == 0) + 162*(Karen_5 == 0) + 486*(Karen_6 == 0) + (Karen_1 == 1) + 3*(Karen_2 == 1) + 9*(Karen_3 == 1) + 27*(Karen_4 == 1) + 81*(Karen_5 == 1) + 243*(Karen_6 == 1)) (2*(Taylor_1 == 0) + 6*(Taylor_2 == 0) + 18*(Taylor_3 == 0) + 54*(Taylor_4 == 0) + 162*(Taylor_5 == 0) + 486*(Taylor_6 == 0) + (Taylor_1 == 1) + 3*(Taylor_2 == 1) + 9*(Taylor_3 == 1) + 27*(Taylor_4 == 1) + 81*(Taylor_5 == 1) + 243*(Taylor_6 == 1)) | 1 in [1,1] 3 in [1,1] 9 in [1,1] 27 in [0,1] 29 in [0,1] 87 in [0,1] 99 in [0,1] 297 in [0,1] 299 in [0,1] 411 in [0,1] 423 in [0,1] 540 in [0,1] 542 in [0,1] 654 in [0,1] 666 in [0,1] )
   Gcc((2*(Beth_1 == 2) + 6*(Beth_2 == 2) + 18*(Beth_3 == 2) + 54*(Beth_4 == 2) + 162*(Beth_5 == 2) + 486*(Beth_6 == 2) + (Beth_1 == 3) + 3*(Beth_2 == 3) + 9*(Beth_3 == 3) + 27*(Beth_4 == 3) + 81*(Beth_5 == 3) + 243*(Beth_6 == 3)) (2*(Charles_1 == 2) + 6*(Charles_2 == 2) + 18*(Charles_3 == 2) + 54*(Charles_4 == 2) + 162*(Charles_5 == 2) + 486*(Charles_6 == 2) + (Charles_1 == 3) + 3*(Charles_2 == 3) + 9*(Charles_3 == 3) + 27*(Charles_4 == 3) + 81*(Charles_5 == 3) + 243*(Charles_6 == 3)) (2*(David_1 == 2) + 6*(David_2 == 2) + 18*(David_3 == 2) + 54*(David_4 == 2) + 162*(David_5 == 2) + 486*(David_6 == 2) + (David_1 == 3) + 3*(David_2 == 3) + 9*(David_3 == 3) + 27*(David_4 == 3) + 81*(David_5 == 3) + 243*(David_6 == 3)) (2*(Frank_1 == 2) + 6*(Frank_2 == 2) + 18*(Frank_3 == 2) + 54*(Frank_4 == 2) + 162*(Frank_5 == 2) + 486*(Frank_6 == 2) + (Frank_1 == 3) + 3*(Frank_2 == 3) + 9*(Frank_3 == 3) + 27*(Frank_4 == 3) + 81*(Frank_5 == 3) + 243*(Frank_6 == 3)) (2*(Jessica_1 == 2) + 6*(Jessica_2 == 2) + 18*(Jessica_3 == 2) + 54*(Jessica_4 == 2) + 162*(Jessica_5 == 2) + 486*(Jessica_6 == 2) + (Jessica_1 == 3) + 3*(Jessica_2 == 3) + 9*(Jessica_3 == 3) + 27*(Jessica_4 == 3) + 81*(Jessica_5 == 3) + 243*(Jessica_6 == 3)) (2*(Karen_1 == 2) + 6*(Karen_2 == 2) + 18*(Karen_3 == 2) + 54*(Karen_4 == 2) + 162*(Karen_5 == 2) + 486*(Karen_6 == 2) + (Karen_1 == 3) + 3*(Karen_2 == 3) + 9*(Karen_3 == 3) + 27*(Karen_4 == 3) + 81*(Karen_5 == 3) + 243*(Karen_6 == 3)) (2*(Taylor_1 == 2) + 6*(Taylor_2 == 2) + 18*(Taylor_3 == 2) + 54*(Taylor_4 == 2) + 162*(Taylor_5 == 2) + 486*(Taylor_6 == 2) + (Taylor_1 == 3) + 3*(Taylor_2 == 3) + 9*(Taylor_3 == 3) + 27*(Taylor_4 == 3) + 81*(Taylor_5 == 3) + 243*(Taylor_6 == 3)) | 1 in [1,1] 3 in [1,1] 9 in [1,1] 27 in [0,1] 29 in [0,1] 87 in [0,1] 99 in [0,1] 297 in [0,1] 299 in [0,1] 411 in [0,1] 423 in [0,1] 540 in [0,1] 542 in [0,1] 654 in [0,1] 666 in [0,1] )
  
Impossible

In [39]:

    

units = {
  ' ': 0,
  'L': 1,
  'W': 2,
}
def parse_outcomes(s):
  result = {}
  for line in s.split('\n'):
    line = line.strip()
    if not line:
      continue
    lower, upper, spec = int(line[0]), int(line[1]), line[3:]
    acc = 0
    for i, c in enumerate(spec):
      acc += units[c] * (3 ** i)
    result[acc] = (lower, upper)
  return result

parse_outcomes("""
  11 L
  01 W  L
  01 W  W L
  01 W  W W
  01    L
  01    W L
  01    W W
  11  L
  01  W  L
  01  W  WL
  01  W  WW
  11   L
  01   W L
  01   W WL
  01   W WW
""")


    

    
Out[39]:





{1: (1, 1),
 3: (1, 1),
 9: (1, 1),
 27: (0, 1),
 29: (0, 1),
 87: (0, 1),
 99: (0, 1),
 297: (0, 1),
 299: (0, 1),
 411: (0, 1),
 423: (0, 1),
 540: (0, 1),
 542: (0, 1),
 654: (0, 1),
 666: (0, 1)}

In [ ]: