Itâ€™s an NPcomplete problem.
(overview/sketch of a mathematical proof as to why itâ€™s NPcomplete)
For NPhardness, itâ€™s possible to reduce from the clique problem as follows.
Given a graph and a number k
, construct a problem instance of players and constraints as follows.
 one special player X
 one player N_{v} for each vertex v in the graph

a lot of dummy players, specifically k*(nk) many, where n is the number of vertices in the graph
We look for teams of size k+1, and have a total of 1+n+k*(nk) = (k+1)*(nk+1) players (so it is divisible by k+1), where n is the number of vertices in the graph.
The â€śdo put player â€¦ with â€¦â€ť constraints are unused.
Thereâ€™s a â€śdon't put player â€¦ with â€¦â€ť constraint for the following pairs
 X canâ€™t be in a team with any dummy player
 for vertices v and v' that aren't connected by an edge N_{v} cannot be in a team with N_{v'}
This has the effect that the team of size k+1 with player X will also contain k more players, all of which are players of type N_{v} for some vertices v, and those vertices form a clique.
On the other hand, if there exists a clique, then it can be put with player X, and all remaining nodes N_{v} for vertices v not in that clique can be put into their own teams, each together with k dummy players.
As for being solvable in NP, thatâ€™s rather trivial, so I wonâ€™t go into it.
(end of the proof)
It is possible to model the problem using a SAT solver. For example, one can model it by introducing a variable for each pair of player and team encoding whether the player in question is part of the team in question. This encoding would need N*(N/m) variables, and encoding the constraints should be possible with some polynomial (in N) amount of clauses (as well as probably some helper variables for intermediate results), too, though I havenâ€™t fully thought through the details, and how large exactly that would become, nor whether there might be a better way to encode the problem.