Solution for the ping pong problem using Z3Py

ping_pong.py

# Solution for the following problem:
# 3 friends (A, B and C) play ping-pong all day.
# The winner always keeps playing. A plays 10 games, B 15, C 17. Who lost the 2nd game?
# Problem by @eldracote https://twitter.com/eldracote/status/939614390571200514

from z3 import *

# Keep track of the players results (2 means win, 1 means loss, 0 is DNP)
A = IntVector('a', 21)
B = IntVector('b', 21)
C = IntVector('c', 21)

# Keep track whether each player played or not
playedA = IntVector('playedA', 21)
playedB = IntVector('playedB', 21)
playedC = IntVector('playedC', 21)

s = Solver()

for i in range(21):
	s.add(playedA[i] >= 0, playedB[i] >=0, playedC[i] >= 0)
	s.add(playedA[i] <= 1, playedB[i] <=1, playedC[i] <= 1)
	s.add(A[i] + B[i] + C[i] == 3) 
	s.add(A[i] <= 2, A[i] >= 0)
	s.add(B[i] <= 2, B[i] >= 0)
	s.add(C[i] <= 2, C[i] >= 0)
	if i < 20:
		s.add(If(A[i] == 1, A[i+1] == 0, True))
		s.add(If(B[i] == 1, B[i+1] == 0, True))
		s.add(If(C[i] == 1, C[i+1] == 0, True))
	s.add(If(Or(A[i] == 1, A[i] == 2), playedA[i] == 1, True))
	s.add(If(Or(B[i] == 1, B[i] == 2), playedB[i] == 1, True))
	s.add(If(Or(C[i] == 1, C[i] == 2), playedC[i] == 1, True))

s.add(sum(playedA) == 10, sum(playedB) == 15, sum(playedC) == 17)

if s.check() == sat:
	m = s.model()

	for i in range(21):
		print("Game {} A:{}, B:{}, C:{}".format(i+1, m[A[i]], m[B[i]], m[C[i]]))

# Solution (2 means win, 1 means loss, 0 is DNP)
# Game 1 A:0, B:2, C:1
# Game 2 A:1, B:2, C:0
# Game 3 A:0, B:1, C:2
# Game 4 A:1, B:0, C:2
# Game 5 A:0, B:1, C:2
# Game 6 A:1, B:0, C:2
# Game 7 A:0, B:1, C:2
# Game 8 A:1, B:0, C:2
# Game 9 A:0, B:1, C:2
# Game 10 A:1, B:0, C:2
# Game 11 A:0, B:1, C:2
# Game 12 A:1, B:0, C:2
# Game 13 A:0, B:1, C:2
# Game 14 A:1, B:0, C:2
# Game 15 A:0, B:2, C:1
# Game 16 A:1, B:2, C:0
# Game 17 A:0, B:2, C:1
# Game 18 A:1, B:2, C:0
# Game 19 A:0, B:2, C:1
# Game 20 A:1, B:2, C:0
# Game 21 A:0, B:2, C:1