# Blogofbrew

home

## Covid-19 Minimization with Z3

04 Sep 2020

There is controversy in Iowa and elsewhere on how to effectively keep classrooms as in person as possible. I decided to model the problem in z3py. The model is simple, it minimizes outside contact edges between students in different classrooms.

I hosted it here. Feedback is welcome.

For simplicity (dataset from Yurichev’s book) I used a school of international students, one from every country in Europe. Where borders touch it is assumes students might be exposed to each other. See Network theory and SARS: predicting outbreak diversity if you want to generate your own social networks.

I also wrote a second model that assumes classrooms are a clique and minimizes total edges. It uses the formula for edges within a clique of a given size instead of counting them.

There was a 3x speedup by using fixed length BitVec() values instead of constrained size Int() values to encode the four classroom assignments.

if(BIT_COLORS):
student_color=[BitVec('student%d_color' % c,2) for c in range(students_total)]
else:
student_color=[Int('student%d_color' % c) for c in range(students_total)]
for i in range(PERSONS):