The Problem
If you have ever been to a wedding in Asia, you would have noticed that some of the family members can be extremely picky on where they sit and who they sit with. Accomodating peoples’ preferences at a rather large wedding can be extremely taxing on the couple that is getting married.
What we did
We framed the problem of seating people at a wedding table as a satisfiability modulo theories (SMT) problem. We tried to identify rules that define how a table should be seated:
- Couples should be seated together
- "Enemies" should not be seated together
- A person can only be seated at one table
- There are different restrictions on how many people can be seated at different tables
- Tables are sometimes restricted by guests' dietary preferences
To find a table arrangement that fulfills as many constraints listed by a couple as possible, we used the Z3 theorem prover and PySMT libraries to develop a solution.
Our solution is on github.