Previously: https://yurichev.com/blog/kirkman/.

I've found this in the Dennis E. Shasha -- "Puzzles for Programmers and Pros" book:

Scheduling Tradition There are 12 school teams, unimaginatively named A, B, C, D, E, F, G, H, I, J, K, and L. They must play one another on 11 consecutive days on six fields. Every team must play every other team exactly once. Each team plays one game per day. Warm-Up Suppose there were four teams A, B, C, D and each team has to play every other in three days on two fields. How can you do it? Solution to Warm-Up We’ll represent the solution in two columns corresponding to the two playing fields. Thus, in the first day, A plays B on field 1 and C plays D on field 2. AB CD AC DB AD BC Not only does the real problem involve 12 teams instead of merely four, but there are certain constraints due to traditional team rivalries: A must play B on day 1, G on day 3, and H on day 6. F must play I on day 2 and J on day 5. K must play H on day 9 and E on day 11. L must play E on day 8 and B on day 9. H must play I on day 10 and L on day 11. There are no constraints on C or D because these are new teams. 1. Can you form an 11-day schedule for these teams that satisfies the constraints? It may seem difficult, but look again at the warm-up. Look in particular at the non-A columns. They are related to one another. If you understand how, you can solve the harder problem.

This is like Kirkman's Schoolgirl Problem I have solved using Z3 before, but this time I've rewritten it as a SAT problem. Also, I added additional constraints relating to "team rivalries". This code also uses my SAT-related Xu Python library.

import Xu import itertools, math PERSONS, DAYS, GROUPS = 12, 11, 6 s=Xu.Xu(False) # each element - group for each person and each day: tbl=[[s.alloc_BV(GROUPS) for day in range(DAYS)] for person in range(PERSONS)] def chr_to_n (c): return ord(c)-ord('A') # A must play B on day 1, G on day 3, and H on day 6. # A/B, day 1: s.fix_BV_EQ(tbl[chr_to_n('A')][0], tbl[chr_to_n('B')][0]) # A/G, day 3: s.fix_BV_EQ(tbl[chr_to_n('A')][2], tbl[chr_to_n('G')][2]) # A/H, day 5: s.fix_BV_EQ(tbl[chr_to_n('A')][4], tbl[chr_to_n('H')][4]) # F must play I on day 2 and J on day 5. s.fix_BV_EQ(tbl[chr_to_n('F')][1], tbl[chr_to_n('I')][1]) s.fix_BV_EQ(tbl[chr_to_n('F')][4], tbl[chr_to_n('J')][4]) # K must play H on day 9 and E on day 11. s.fix_BV_EQ(tbl[chr_to_n('K')][8], tbl[chr_to_n('H')][8]) s.fix_BV_EQ(tbl[chr_to_n('K')][10], tbl[chr_to_n('E')][10]) # L must play E on day 8 and B on day 9. s.fix_BV_EQ(tbl[chr_to_n('L')][7], tbl[chr_to_n('E')][7]) s.fix_BV_EQ(tbl[chr_to_n('L')][8], tbl[chr_to_n('B')][8]) # H must play I on day 10 and L on day 11. s.fix_BV_EQ(tbl[chr_to_n('H')][9], tbl[chr_to_n('I')][9]) s.fix_BV_EQ(tbl[chr_to_n('H')][10], tbl[chr_to_n('L')][10]) for person in range(PERSONS): for day in range(DAYS): s.make_one_hot(tbl[person][day]) # enumerate all variables # we add Or(pair1!=0, pair2!=0) constraint, so two non-zero variables couldn't be present, # but both zero variables in pair is OK, one non-zero and one zero variable is also OK: def only_one_must_be_zero(lst): for pair in itertools.combinations(lst, r=2): s.OR_always([s.BV_not_zero(pair[0]), s.BV_not_zero(pair[1])]) # at least one variable must be zero: s.OR_always([s.BV_zero(l) for l in lst]) # get two arrays of variables XORed. one element of this new array must be zero: def only_one_in_pair_can_be_equal(l1, l2): assert len(l1)==len(l2) only_one_must_be_zero([s.BV_XOR(l1[i], l2[i]) for i in range(len(l1))]) # enumerate all possible pairs: for pair in itertools.combinations(range(PERSONS), r=2): only_one_in_pair_can_be_equal (tbl[pair[0]], tbl[pair[1]]) assert s.solve() print "group for each person:" print "person: "+"".join([chr(ord('A')+i)+" " for i in range(PERSONS)]) for day in range(DAYS): print "day=%2d:" % day, for person in range(PERSONS): print int(math.log(s.get_val_from_solution(tbl[person][day]),2)), print "" def persons_in_group(day, group): rt="" for person in range(PERSONS): if int(math.log(s.get_val_from_solution(tbl[person][day]),2))==group: rt=rt+chr(ord('A')+person) return rt print "" print "persons grouped:" for day in range(DAYS): print "day=%2d:" % day, for group in range(GROUPS): print persons_in_group(day, group)+" ", print ""

The solution:

group for each person: person: A B C D E F G H I J K L day= 0: 4 4 1 3 5 0 2 0 5 3 2 1 day= 1: 5 0 3 3 2 4 1 2 4 1 0 5 day= 2: 4 5 1 0 1 2 4 5 3 3 2 0 day= 3: 3 5 4 1 1 4 2 2 0 5 3 0 day= 4: 3 0 4 5 0 2 5 3 4 2 1 1 day= 5: 3 5 4 5 3 0 0 4 1 2 1 2 day= 6: 5 3 5 4 1 0 1 4 3 2 2 0 day= 7: 5 2 0 1 3 1 2 4 5 4 0 3 day= 8: 4 2 5 4 1 1 3 0 3 5 0 2 day= 9: 4 2 2 1 5 4 0 3 3 5 1 0 day=10: 2 5 0 4 3 5 0 1 4 2 3 1 persons grouped: day= 0: FH CL GK DJ AB EI day= 1: BK GJ EH CD FI AL day= 2: DL CE FK IJ AG BH day= 3: IL DE GH AK CF BJ day= 4: BE KL FJ AH CI DG day= 5: FG IK JL AE CH BD day= 6: FL EG JK BI DH AC day= 7: CK DF BG EL HJ AI day= 8: HK EF BL GI AD CJ day= 9: GL DK BC HI AF EJ day=10: CG HL AJ EK DI BF

("Person" and "team" terms are interchangeable in my code.)

Thanks to parallel lingeling SAT solver I've used this time, it takes couple of minutes on a decent 4-core CPU.

The source code: https://github.com/DennisYurichev/yurichev.com/tree/master/blog/kirkman_SAT.

Please drop me email about any bug(s) and suggestion(s):