In [72]:
import forge
from puzzle.puzzlepedia import puzzlepedia

puzzle = puzzlepedia.parse("""
with init:
  ALL_Q = list(range(1, 16+1))
  A = {i: variable('%02dA' % i) for i in ALL_Q}
  B = {i: variable('%02dB' % i) for i in ALL_Q}
  C = {i: variable('%02dC' % i) for i in ALL_Q}
  ALL_A = [A[i] for i in ALL_Q]
  ALL_B = [B[i] for i in ALL_Q]
  ALL_C = [C[i] for i in ALL_Q]
for i in ALL_Q:
  A[i] | B[i] | C[i]

def n_correct(i):
  return A[i] + B[i] + C[i]

def vector(i):
  return A[i] * 4 + B[i] * 2 + C[i]

def superset(big, small):
  return (
      A[big] >= A[small] and
      B[big] >= B[small] and
      C[big] >= C[small])

#1
if A[1]: B[1] and not C[1]
if B[1]: A[1] and B[1]
if C[1]: A[1] and C[1]

#2
sum_a = sum(ALL_A)
if A[2]: sum_a == 10
if B[2]: sum_a == 12
if C[2]: sum_a == 14

#3
not A[3]
B[3]
not C[3]

#4
A[4]
not B[4]
not C[4]

#5
n_multiple_answers = sum(n_correct(i) > 1 for i in ALL_Q)
A[5] == (n_multiple_answers >= 5)
B[5] == (n_multiple_answers == 5)
C[5] == (n_multiple_answers == 3)

#6
A[6] == (n_correct(5) == 1)
B[6] == (n_correct(10) == 1)
C[6] == (n_correct(15) == 1)

#7
q11_superset_of_q12 = superset(11, 12)
A[7] == q11_superset_of_q12
B[7] != q11_superset_of_q12
not C[7]

#8
q12_same_as_q13 = vector(12) == vector(13)
A[8] == q12_same_as_q13
B[8] != q12_same_as_q13
not C[8]

#9
not A[9]
B[9]
not C[9]

#10
A[10] == (A[1] and A[4])
B[10] == (A[1] and A[4] and C[1] and C[4])
C[10] == (B[1] and B[4] and C[1] and C[4])

#11
A[11]: vector(2) == vector(4)
B[11]: vector(4) == vector(8)
C[11]: vector(8) == vector(16)

#12
# !!!! CHANGES FROM A to B !!!
not A[12]
B[12]
not C[12]

#13
# FIXME: This didn't work. (Well, one solution was correct but two others were not.)
sum_c = sum(ALL_C)
A[13] == (sum_c == 1)
B[13] == (sum_c >= 2)
C[13] == (sum_c >= 8)

#14
A[14] == (C[14] + C[15] + C[16] == 1)
B[14] == (A[14] + A[15] + A[16] == 1)
C[14] == (B[14] + B[15] + B[16] == 1)

#15
#A[15] == any(A[i] and B[i] and (not C[i]) for i in [14, 15, 16])
A[15] == (
    (A[14] and B[14] and not C[14]) |
    (A[15] and B[15] and not C[15]) |
    (A[16] and B[16] and not C[16]))

B[15] == any(A[i] and B[i] and C[i] for i in [14, 15, 16])
#C[15] == any((not A[i]) * B[i] * C[i] for i in [14, 15, 16])
c15_14 = (1 - A[14]) and B[14] and C[14]
c15_15 = (1 - A[15]) and B[15] and C[15]
c15_16 = (1 - A[16]) and B[16] and C[16]
C[15] == (c15_14 | c15_15 | c15_16)
#C[15] == (
#    ((not A[14]) and B[14] and C[14]) |
#    ((not A[15]) and B[15] and C[15]) |
#    ((not A[16]) and B[16] and C[16])) > 0

#16
A[16] == any(C[i] for i in [14, 15, 16])
B[16] == any(A[i] for i in [14, 15, 16])
C[16] == any(B[i] for i in [14, 15, 16])
""")

In [ ]: