## [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)
t=[self.XOR(l1[i], l2[i]) for i in range(len(l1))]

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

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


... 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.