In [18]:

    

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

Aida = 0
Carmen = 1
Die = 2
Il = 3
Le = 4
Les = 5
Rig = 6
Tosca = 7

model = Numberjack.Model()

names = ['Beth', 'Charles', 'David', 'Frank', 'Jessica', 'Karen', 'Taylor']
movie_names = [
  'Aida', 'Carmen', 'Die Walkure', 'Il trovatore', 'Le nozze di Figaro',
  'Les contes d\'Hoffman', 'Rigoletto', 'Tosca']
people = list(range(7))
movies = list(range(8))
grid = []
for x in range(len(names)):
  row = []
  grid.append(row)
  for y in range(len(movies)):
    row.append(Numberjack.Variable(0, 8, '%s_%s' % (x, y)))
  model.add(Numberjack.Sum(row) == 8)

@functools.lru_cache()
def count_p_score_n(p, n):
  #return Numberjack.Sum(grid[p][i] == n for i in movies)
  return Numberjack.Cardinality([grid[p][i] for i in movies], n)

@functools.lru_cache()
def movie_n(m):
  return Numberjack.Sum(grid[p][m] for p in people)

@functools.lru_cache()
def top_score(p):
  return Numberjack.Max([grid[p][m] for m in movies])

#1: In setup.

#2: Count the number of zeros for all 7 people.
model.add(Numberjack.Gcc(
  [count_p_score_n(p, 0) for p in people],
  {
    # One 8 score (implies 7 zeros).
    7: (1, 1),
    # Voted for 2 operas.
    6: (0, 5),
    # Voted for 3 operas.
    5: (0, 5),
    # Voted for 4 operas.
    4: (0, 0),
    # Voted for 5 operas.
    3: (0, 0),
    # Voted for 6 operas.
    2: (1, 1),
    # Voted for 7 operas.
    1: (0, 0),
    # Voted for all operas.
    0: (0, 0),
  }
))

#3
model.add(top_score(Beth) == top_score(David))

#4
model.add(Numberjack.AllDiff([
  top_score(Beth),
  top_score(Charles),
  top_score(Frank),
  top_score(Jessica),
  top_score(Karen),
  top_score(Taylor),
]))

#5a
model.add(count_p_score_n(Taylor, 1) > 1)
#5b
for p in people:
  if p != Taylor:
    model.add(Numberjack.AllDiffExcept0(grid[p]))
#5c
model.add(grid[Taylor][Aida] != 0)

#6
for m in movies:
  model.add(Numberjack.AllDiffExcept0([grid[p][m] for p in people]))

#7
model.add(grid[David][Rig] > grid[Jessica][Rig])
model.add(grid[Jessica][Rig] > grid[Charles][Rig])
model.add(grid[Charles][Rig] > grid[Taylor][Rig])
model.add(grid[Taylor][Rig] == 1)

#8
model.add(grid[Beth][Il] == grid[Jessica][Rig])

#9
model.add(movie_n(Aida) == grid[Jessica][Aida] * 2)

#10a
model.add(grid[Karen][Carmen] != 0)
#10b
model.add(Numberjack.Mod([movie_n(Carmen), 2]) == 1)

#11
model.add(grid[David][Aida] == grid[Karen][Il])
model.add(grid[Karen][Il] == grid[Jessica][Les])
model.add(grid[Jessica][Les] != 0)

#12
model.add(movie_n(Tosca) == movie_n(Aida) + 1)
model.add(movie_n(Tosca) == movie_n(Les) + 2)

#13
model.add(movie_n(Die) == movie_n(Il) - 1)

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


if solver.is_unsat():
  print('Impossible')
else:
  for i, m in enumerate(movie_names):
    print(i, m, _util.numberjack_solution(movie_n(i)))
  for y, row in enumerate(grid):
    result = [names[y]]
    for x, variable in enumerate(row):
      result.append(str(variable.get_value()))
    print('\t'.join(result))


    

    




0 Aida 8
1 Carmen 13
2 Die Walkure 3
3 Il trovatore 4
4 Le nozze di Figaro 1
5 Les contes d'Hoffman 7
6 Rigoletto 11
7 Tosca 9
Beth	0	5	0	3	0	0	0	0
Charles	0	0	0	0	0	6	2	0
David	1	0	2	0	0	0	5	0
Frank	0	0	0	0	0	0	0	8
Jessica	4	0	0	0	0	1	3	0
Karen	0	7	0	1	0	0	0	0
Taylor	3	1	1	0	1	0	1	1

In [ ]: