Constraint solvers, SAT solvers, what am I looking for?

help
1

Let's say I have N players that I want to divide into teams of size m, but I also have constraints on which players can be paired together e.g. "don't put player A with player B", "do put player C with player D", etc.

What I want to know is given these constraints:

  • Is it possible to divide the players into teams like this?
  • If so, what is one (of possibly many) such assignment?

The thing is, I don't know what general category of computer science problem I'm looking at (I'm self taught), so I don't really know which kind of libraries to look for and I don't know if they exist in Rust. I could always bind to a library written in another language, but that's not ideal.

2 Likes
2

It’s an NP-complete problem.

(overview/sketch of a mathematical proof as to why it’s NP-complete)

For NP-hardness, 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 Nv for each vertex v in the graph
  • a lot of dummy players, specifically k*(n-k) 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*(n-k) = (k+1)*(n-k+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 Nv cannot be in a team with Nv'

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

1 Like
3

This is called graph coloring.

Any time you have two players that should be on the same team, just treat both as a single player.

Once you only have "not same team" constraints left, what you have is a graph coloring problem. The colors correspond to teams, and you must use different colors for pairs of people with a conflict. The hardness of the problem depends on the number of teams.

  • If you want to find the smallest possible number of teams, or if the number of teams is part of the input, then it is NP-complete like @steffahn mentioned.
  • However if the number of teams is larger than the largest number of conflicts that any single person has, then you can solve the problem in linear time by going through the players in order and assigning the player any team that doesn't cause a conflict with a player that has already been assigned. You never fail to assign a team because there are too few conflicts for that.

However, since you mentioned a specific number of teams m, you are in the first case.

5 Likes
4

As for how this is solved in practice for games:

  • If the teams are small enough, just brute-force it. 2N is no big deal if N is only 10.

  • Otherwise, change it from "do"/"don't" to "bonus/penalize such a team", and run Simulated annealing - Wikipedia for a bit until you get pretty good teams, and don't worry about it too much when they're not perfect.

5

My experience working on CG:SHOP 2022 taught me that simulated annealing was not a very good heuristic for solving graph coloring problems. Our experience was that SAT solvers are much better than every other heuristic at this particular problem, even for finding non-optimal solutions.

6

That makes sense for hard constraints.

The "make teams" situations where I've seen it used are where it's much less "you cannot do this" and more "we have a bunch of things we'd rather did/didn't happen" -- like we'd like you to be on the same team with your friends, but not if it makes other things bad -- where phrasing teams as more of an optimization problem rather than a constraint satisfaction one works well.

If that's not what the OP's doing, then they should definitely ignore my advice :slight_smile:

7

How are SAT solvers used for finding non-optimal solutions? Are the constraints relaxed, or is there a mode where not every clause needs to become true or what’s the idea? If not every clause needs to become true, is there a way to specify which ones are absolutely necessary and for which ones “as many as possible” (in a heuristic sense, not a strict optimization problem sense) should become true?

8

If you have a solution with k colors, then you might ask the SAT solver to find a solution using k-1 colors. You can repeat this in a loop. The solution you get from the SAT solver is only optimal if the number of colors you ask the SAT solver to use is least possible.

9

This topic was automatically closed 90 days after the last reply. We invite you to open a new topic if you have further questions or comments.