In [12]:
# Congratulations! You have found a MEDIUM FLASHLIGHT and LARGE FLASHLIGHT!
# Each of the 36 forest tiles is home to some animals (possibly zero).
# But there cannot be multiple of a single type of animal in a tile.
# For example, a tile may contain a caterpillar and an ant, but a tile
# may not contain two ants.
import Numberjack
import functools

class Animal(Numberjack.Matrix):
  def __init__(self, name):
    super(Animal, self).__init__(6, 6, name)
    self.animal = name

  def __hash__(self):
    return hash(self.name())

m = Numberjack.Model()
a = Animal('a')  # Ant
b = Animal('b')  # Butterfly
c = Animal('c')  # Catterpillar
d = Animal('d')  # Deer
e = Animal('e')  # Earthworm

@functools.lru_cache(maxsize=9999)
def box(src, row, col, size=2):
  if size == 3:
    edge = ((2, 0), (2, 1), (2, 2), (1, 2), (0, 2))
    cells = [src[row+y][col+x] for (x, y) in edge]
    cells.append(box(src, row, col, size=2))
    return Numberjack.Sum(cells)
  return Numberjack.Sum(
    src[y][x] for y in range(row, row+size)
              for x in range(col, col+size))

def cell_box_total(row, col, size=2):
  return Numberjack.Sum(x[row][col] for x in [a, b, c, d, e])

def animal_box_total(row, col, size=2):
  pass

@functools.lru_cache(maxsize=9999)
def total(row, col, size=2):
  return Numberjack.Sum(box(x, row, col, size) for x in [a, b, c, d, e])


# 0, 0
m.add(total(0, 0) == 12)
m.add(box(a, 0, 0) == 3)
m.add(box(b, 0, 0) > box(d, 0, 0))
# 0, 1
m.add(total(0, 1) == 9)
m.add(box(b, 0, 1) == 2)
m.add(box(e, 0, 1) == 1)
# 0, 2
m.add(total(0, 2) == 8)
m.add(box(d, 0, 2) == 2)
# TODO: Even number of each animal.
# 0, 3
m.add(total(0, 3) == 8)
m.add(box(c, 0, 3) == 2)
# TODO: Even number of each animal.
# 0, 4
m.add(total(0, 4) == 9)
m.add(box(e, 0, 4) == 2)
# TODO: Earthworms are in same column.

# 1, 0
m.add(total(1, 0) == 10)
m.add(box(c, 1, 0) == 2)
# 1, 1
m.add(total(1, 1) == 4)
m.add(box(d, 1, 1) == 0)
# 1, 2
m.add(total(1, 2) == 3)
m.add(box(a, 1, 2) == 0)
# 1, 3
m.add(total(1, 3) == 4)
m.add(box(e, 1, 3) > 0)
m.add(box(a, 1, 3) > 0)
# 1, 4
m.add(total(1, 4) == 9)
m.add(box(b, 1, 4) == 2)
# TODO: Butterflies are in the same row.
# 2, 0
m.add(total(2, 0) == 9)
m.add(box(b, 2, 0) == 3)
# 2, 1
m.add(total(2, 1) == 3)
m.add(box(b, 2, 1) == 2)
m.add(box(e, 2, 1) == 1)
m.add(box(a, 2, 1) == 0)
m.add(box(c, 2, 1) == 0)
m.add(box(d, 2, 1) == 0)
# m.add(box(b, 2, 1) > box(e, 2, 1))
# m.add(box(e, 2, 1) > box(c, 2, 1))
# 2, 2
m.add(total(2, 2) == 4)
m.add(box(d, 2, 2) == 0)
# 2, 3
m.add(total(2, 3) == 4)
m.add(box(a, 2, 3) == 0)
m.add(box(b, 2, 3) == box(e, 2, 3))
# 2, 4
m.add(total(2, 4) == 7)
m.add(box(c, 2, 4) == 0)

# 3, 0
m.add(total(3, 0) == 8)
m.add(box(a, 3, 0) == 2)
m.add(box(e, 3, 0) == 0)
# 3, 1
m.add(total(3, 1) == 1)
m.add(box(b, 3, 1) == 0)
# 3, 2
m.add(total(3, 2) == 2)
m.add(box(c, 3, 2) == 0)
# 3, 3
m.add(total(3, 3) == 2)
m.add(box(e, 3, 3) == 1)
# 3, 4
m.add(total(3, 4) == 5)
m.add(box(d, 3, 4) == 2)
m.add(box(c, 3, 4) == 1)

# 4, 0
m.add(total(4, 0) == 12)
m.add(box(c, 4, 0) == 2)
m.add(box(e, 4, 0) == 2)
# 4, 1
m.add(total(4, 1) == 10)
m.add(box(e, 4, 1) == 2)
# 4, 2
m.add(total(4, 2) == 9)
m.add(box(d, 4, 2) == 2)
# 4, 3
m.add(total(4, 3) == 8)
m.add(box(b, 4, 3) == 2)
# 4, 4
m.add(total(4, 4) == 7)
m.add(box(b, 4, 4) >= (box(a, 4, 4) * 2))
m.add(box(a, 4, 4) >= (box(e, 4, 4) * 2))


#######
# BIG #
#######
# 0, 0
m.add(total(0, 0, size=3) == 23)
# TODO: Every tile with a caterpillar has a deer, vice versa.
# 0, 1
m.add(total(0, 1, size=3) == 17)
m.add(box(e, 0, 1, size=3) == 2)
# TODO: 2 earthworms share a corner, not edge.
# 0, 2
m.add(total(0, 2, size=3) == 17)
# 0, 3
m.add(total(0, 3, size=3) == 19)
m.add(box(b, 0, 3, size=3) > 0)
# TODO: Even number of butterflies.

# 1, 0
m.add(total(1, 0, size=3) == 16)
# 1, 1
m.add(total(1, 1, size=3) == 6)
# TODO: 6, 3 the same + 3 the same
# 1, 2
m.add(total(1, 2, size=3) == 7)
m.add(box(c, 1, 2, size=3) < 2)
# 1, 3
m.add(total(1, 3, size=3) == 13)
# TODO: Odd number of every type of animal.

# 2, 0
m.add(total(2, 0, size=3) == 16)
m.add(box(a, 2, 0, size=3) == 3)
# 2, 1
m.add(total(2, 1, size=3) == 6)
m.add(box(e, 2, 1, size=3) == 3)
# TODO: 1 earthworm per row
# 2, 2
m.add(total(2, 2, size=3) == 8)
m.add(box(b, 2, 2, size=3) == 3)
# TODO: 3 butterflies = 111 in row or col
# 2, 3
m.add(total(2, 3, size=3) == 12)
m.add(box(a, 2, 3, size=3) == 3)
# TODO: The 3 ants are not all in the same col
# 3, 0
m.add(total(3, 0, size=3) == 21)
# TODO: 3/4 corner tiles have ant AND butterfly
# 3, 1
m.add(total(3, 1, size=3) == 15)
m.add(box(a, 3, 1, size=3) == 3)
m.add(box(c, 3, 1, size=3) == 3)
m.add(box(d, 3, 1, size=3) == 3)
# TODO: All 9 acd are in same row or col
# 3, 2
m.add(total(3, 2, size=3) == 14)
# 3, 3
m.add(total(3, 3, size=3) == 14)
# TODO: Even number of deer
# TODO: Odd number of a, b, c, e

s = m.load('Mistral')
#print(str(m))
s.solve()

_ART = [' ', '#']
if s.is_unsat():
  print('Impossible')
else:
  print('solution:')
  for x in [a, b, c, d, e]:
    print(x.animal)
    for row in range(6):
      print(''.join(_ART[bool(c.get_value())] for c in x[row]))


solution:
a
##### 
#   # 
#    #
#    #
#   # 
 ###  
b
####  
      
######
#     
#     
######
c
 #####
##   #
      
#     
#    #
 #### 
d
  ### 
#    #
#    #
#    #
#    #
##### 
e
##   #
#    #
# # # 
   #  
  #   
##    

In [ ]: