Abstract
Given a classroom containing a fixed number of students and a fixed number of tables that can be of different sizes, as well as a list of preferred classmates to sit with for each student, the team composition problem in a classroom (TCPC) is the problem of finding an assignment of students to tables in such a way that the preferences of students are maximally-satisfied. In this paper, we first formally define the TCPC, prove that it is NP-hard and define two different MaxSAT models of the problem, called maximizing and minimizing encoding. Then, we report on the results of an empirical investigation that show that solving the TCPC with MaxSAT solvers is a promising approach and provide evidence that the minimizing encoding outperforms the maximizing encoding. Finally, we illustrate how the proposed MaxSAT-based modeling approach is also well-suited for modeling other more complex team formation problems.