[MaxSAT][Python] Packing students into dorm

Given, say, 15 students. And they all have various interests/hobbies in their life, like hiking, clubbing, dancing, swimming, maybe hanging out with girls, etc.

The dormitory has 5 rooms. Three students can be accommodated in each room.

The problem to pack them all in such a way, so that all roommates would share as many interests/hobbies with each other, as possible. To make them happy and tight-knit.

This is what I will do using Open-WBO MaxSAT solver ( 1, 2 ) this time, and my small Python library.

import SAT_lib

s=SAT_lib.SAT_lib(maxsat=True)

STUDENTS=15
CEILING_LOG2_STUDENTS=4 # 4 bits to hold a number in 0..14 range

POSSIBLE_INTERESTS=8

# interests/hobbies for each student. 8 are possible:
interests=[
0b10000100,
0b01000001,
0b00000010,
0b01000001,
0b00001001,
0b00101000,
0b00000100,
0b00000011,
0b01000000,
0b00000100,
0b10000001,
0b00001000,
0b00000010,
0b01000001,
0b01000010,
0] # dummy variable, to pad the list to 16 elements

# each variable is "grounded" to the bitmask from interests[]:
interests_vars=[s.alloc_BV(POSSIBLE_INTERESTS) for i in range(2**CEILING_LOG2_STUDENTS)]
for st in range(2**CEILING_LOG2_STUDENTS):
    s.fix_BV(interests_vars[st], SAT_lib.n_to_BV(interests[st], POSSIBLE_INTERESTS))

# where each student is located after permutation:
students_positions=[s.alloc_BV(CEILING_LOG2_STUDENTS) for i in range(2**CEILING_LOG2_STUDENTS)]

# permutation. all positions are distinct, of course:
s.make_distinct_BVs (students_positions)

# connect interests of each student to permuted version
# use multiplexer...
interests_of_student_in_position={}
for st in range(2**CEILING_LOG2_STUDENTS):
    interests_of_student_in_position[st]=s.create_wide_MUX (interests_vars, students_positions[st])

# divide result of permutation by triplets
# we want as many similar bits in interests[] between all 3 students, as possible:
for group in range(STUDENTS/3):
    i1=interests_of_student_in_position[group*3]
    i2=interests_of_student_in_position[group*3+1]
    i3=interests_of_student_in_position[group*3+2]
    s.fix_soft_always_true_all_bits_in_BV(s.BV_AND(i1, i2), weight=1)
    s.fix_soft_always_true_all_bits_in_BV(s.BV_AND(i1, i3), weight=1)
    s.fix_soft_always_true_all_bits_in_BV(s.BV_AND(i2, i3), weight=1)

assert s.solve()

def POPCNT(v):
    rt=0
    for i in range(POSSIBLE_INTERESTS):
        if ((v>>i)&1)==1:
            rt=rt+1
    return rt

total_in_all_groups=0

# print solution:
for group in range(STUDENTS/3):
    print "* group", group
    st1=SAT_lib.BV_to_number(s.get_BV_from_solution(students_positions[group*3]))
    st2=SAT_lib.BV_to_number(s.get_BV_from_solution(students_positions[group*3+1]))
    st3=SAT_lib.BV_to_number(s.get_BV_from_solution(students_positions[group*3+2]))

    print "students:", st1, st2, st3

    c12=POPCNT(interests[st1]&interests[st2])
    c13=POPCNT(interests[st1]&interests[st3])
    c23=POPCNT(interests[st2]&interests[st3])

    print "common interests between 1 and 2:", c12
    print "common interests between 1 and 3:", c13
    print "common interests between 2 and 3:", c23

    total=c12+c13+c23
    print "total=", total
    total_in_all_groups=total_in_all_groups+total

print "* total in all groups=", total_in_all_groups


Most significant parts from the library used, are:

    # bitvectors must be different.
    def fix_BV_NEQ(self, l1, l2):
        #print len(l1), len(l2)
        assert len(l1)==len(l2)
        self.add_comment("fix_BV_NEQ")
        t=[self.XOR(l1[i], l2[i]) for i in range(len(l1))]
        self.add_clause(t)

    def make_distinct_BVs (self, lst):
        assert type(lst)==list
        assert type(lst[0])==list
        for pair in itertools.combinations(lst, r=2):
            self.fix_BV_NEQ(pair[0], pair[1])

...

    def create_MUX(self, ins, sels):
        assert 2**len(sels)==len(ins)
        x=self.create_var()
        for sel in range(len(ins)): # for example, 32 for 5-bit selector
            tmp=[self.neg_if((sel>>i)&1==1, sels[i]) for i in range(len(sels))] # 5 for 5-bit selector
   
            self.add_clause([self.neg(ins[sel])] + tmp + [x])
            self.add_clause([ins[sel]] + tmp + [self.neg(x)])
        return x
    
    # for 1-bit sel
    # ins=[[outputs for sel==0], [outputs for sel==1]]
    def create_wide_MUX (self, ins, sels):
        out=[]
        for i in range(len(ins[0])):
            inputs=[x[i] for x in ins]
            out.append(self.create_MUX(inputs, sels))
        return out

( https://github.com/DennisYurichev/SAT_SMT_by_example/blob/master/libs/SAT_lib.py )

... and then Open-WBO MaxSAT searches such a solution, for which as many soft clauses as possible would be satisfied, i.e., as many hobbies shared, as possible.

And the result:

* group 0
students: 7 12 1
common interests between 1 and 2: 1
common interests between 1 and 3: 1
common interests between 2 and 3: 0
total= 2
* group 1
students: 13 2 10
common interests between 1 and 2: 0
common interests between 1 and 3: 1
common interests between 2 and 3: 0
total= 1
* group 2
students: 3 4 14
common interests between 1 and 2: 1
common interests between 1 and 3: 1
common interests between 2 and 3: 0
total= 2
* group 3
students: 8 5 11
common interests between 1 and 2: 0
common interests between 1 and 3: 0
common interests between 2 and 3: 1
total= 1
* group 4
students: 9 0 6
common interests between 1 and 2: 1
common interests between 1 and 3: 1
common interests between 2 and 3: 1
total= 3
* total between all groups= 9

Surely, you can group any other objects with each other based on multiple preferences.


→ [list of blog posts]

Please drop me email about any bug(s) and suggestion(s): dennis(@)yurichev.com.