The Limits of Formal Modelling : models meet real-life

We have all been affected by the pandemic and our lives are slowly limping back to some degree of normalcy. As organizations prepare to invite employees back to their office locations (at least for a couple of days a week), we are faced with an interesting problem. Over the last two years, we have hired and on-boarded engineers remotely - many of them have not even seen the office premises; we now have to make sure that their experience coming back to office is a positive one and seating arrangement plays an important role in this experience.

?I had the opportunity recently to be part of a committee tasked with re-allocating and re-organizing seating for engineers. Given the size of the organization, we had to break up the problem hierarchically, and delegate the detailed seat allocation to sub-teams, but at a high-level it is a fairly straightforward problem to state: "given a bunch of blocks of seats of given capacities, and a bunch of groups of given sizes, what is the optimal allocation of blocks to groups?" This is not a new problem to solve, and I have earlier been part of committees that solved this problem manually - using the time-tested method of eye-balling! However, this time around I was determined to put math to use and model this as an optimization problem - and arrive at the optimal solution.

Let us start with a visual representation of the problem in the header of this post. We have 6 blocks of seats organized around a core of conference rooms and cafeteria (typical organization of an office), and 4 top-level groups. All blocks, and groups are of different sizes - the quintessential problem of "fitting a round peg into a rectangular hole" (sic.).

The Model

There are a number of techniques for modelling this problem, from SAT solving to linear programming. I decided to apply the MiniZinc tool for modelling and solving the seat allocation problem. I have recently been playing around with the MiniZinc tool and investigating the algorithms it uses to solve constraint problems in the context of program analysis and formal verification. The MiniZinc language is a nice high-level language to model problems and supports a number of constraint formulations that are well studied in literature. The Global Constraint Catalog is a very nice resource that catalogs many forms of constraints studied in the literature.

The first thought that comes to mind is "this looks like the bin-packing problem" -?and bin-packing is one of the standard constraints that can be directly expressed in MiniZinc. However the seat-assignment does not quite fit into a bin-packing formulation; this is because the items (Groups) can be broken up into smaller pieces to fit into the bins (Blocks). After a bit of exploration, I finally decided to build the MiniZinc model of the problem starting from first-principles.

The MiniZinc model I came up with is fairly small and can be reviewed here. We first introduce two enumerated types Blocks and Groups and maps from these types to integers -- representing capacity of Blocks and size of Groups. Maps are modelled in MiniZinc as arrays indexed by the corresponding domain type. Each of these mappings are additionally constrained so that they map Blocks and Groups to only positive integers - MiniZinc constraints are simple Boolean predicates. One nice feature of the MiniZinc language is the separation in specification of the model and its parameters. Parameters are specific ground values provided to symbols introduced in the model. For example, the enumerated values of a Block or the actual capacity of each Block can be treated as parameters to a model. This allows easy reuse of a model to a number of different problem data-sets.

The most important definition in the model is an assignment of Groups to Blocks - I chose to model this as a two-dimensional mapping from Groups, and Blocks to positive integers - representing the number of seats in a Block assigned to a Group. There are other ways to model this : for example as a mapping to a real number in the range [0,1] - representing the fraction of a Block assigned to a Group, or the fraction of a Group assigned to a Block - however, I found the assignment of integers to be the most direct and simple modelling choice. One sanity condition on assignments is:

• Any assignment of a Group to a Block has to be non-negative, less than the size of the Group, and the less than the capacity of the Block.

The primary constraints on seat assignment can now be stated:

• Every member in each Group has to be assigned to a Block : the sum of all assignments for a Group has to be equal to the size of the Group
• There can be empty seats in a Block - the sum of all assignments to a Block has to be less-than-or-equal-to the capacity of the Block
• There is?a minimum size for every assignment of a Group to a Block - this is typically the smallest size of a cross-functional team. A cross-functional team is very effective when they are seated near each other - maximizing interactions.

And that is it!!?

The search for The Optimal Solution

MiniZinc solver can solve this model given a specification of ground-values for enums and parameters - see here for a sample data-set. As a sanity check, we can obtain a solution for the model, and get MiniZinc to print it - this is quite simple using the GUI interface of MiniZinc. First, we have to configure the solver that MiniZinc uses - for this particular problem the default solver "Gecode" does not seem to be the best option; the "Chuffed" solver seems to perform orders of magnitude better on this problem. Setting up the solver and solving the basic model (seating_model_no_optimization.mzn) with the data-set (seat_data_v1.dzn) gives the following result:

MiniZinc generates a nicely formatted output of the assignment matrix. It is possible to check the number of satisfying solutions by adjusting the configuration options - there is an option to specify the number of solutions to be generated by the solver. There are tens of thousands of solutions for this model and data-set - an impossible amount of noisy data to go through!

We can narrow down the search by providing an optimization objective to the solver - this is a numerical expression, and it is possible to instruct MiniZinc to minimize (or maximize) this numerical expression. There are many optimization objectives to choose from:

• The total number of allocations of sub-groups to Blocks (minimizing this will try to avoid splitting up Groups)
• The maximum distance between two sub-groups of a single Group (minimizing this will try to increase adjacency of sub-groups of a Group)
• The maximum number of Groups assigned to Blocks (minimizing this will try to keep a Block homogenous, and maximizing this will increase chances of non-planned interactions in at least one Block)
• The maximum free-space?in any Block (minimizing this will ensure free-space is spread evenly across all blocks - Note that the total free space is fixed by the data-set; the only variable is how this free-space is distributed across Blocks)

These objective functions need to be carefully evaluated - as they directly relate to the outcome that we would like to design for! For example the first objective of minimizing splits in a Group certainly is important from an administrative perspective - in a hierarchical organization, where each Group or sub-Group is responsible for managing the seats available to it, it reduces complexity of the management task for each Group. However, this would generally increase homogeneity of the assignment, and perhaps reduce un-planned interactions between engineers - which is an important advantage of a work-place over work-from-home. Note that some of these objectives can have subtleties based on their precise formulation - for example, if we maximize on the number of Groups assigned to a Block (see the definition of max_free in seating_model.mzn) , it may result in a single Block becoming a "kitchen-sink". A simple-minded objective here would be to maximize the total number of assignments across all Groups maximizing the heterogenity of the assignment; however this directly contradicts the first objective which tries to reduce the number of Group splits! It is meaningless to both maximize and minimize the same objective! The simplest way to resolve this conflict is to appeal to a status-quo which emphasized on group cohesion in seating, and punting the problem of encouraging un-planned interactions to common-areas like the cafeteria, games-rooms, and activities like book-clubs; and this is the approach I will follow below!

?I decided to optimize on two metrics: minimize the number of assignments for a data-set; and additionally minimize the maximum distance between two sub-Groups of a single Group (seating_model.mzn).?MiniZinc does not natively support minimizing for multiple objectives, so I had to encode a simple lexicographic encoding of two individual numbers into a single number - the file utils.mzn?has the definitions for the lexicographic encoding, and also some other utility functions. MiniZinc now generates the solution:

This solution is one of the optimal assignments for the seat-allocation problem; it is not possible to have an assignment with fewer group splits. Looking at the other metrics displayed just above the assignment matrix, we can also see that this assignment has at least one Block that is completely full (Min Free), and one Block with 4 additional seats (Max Free). From the fact that the total number of seats is 730, and total size of the Groups is 726, this assignment has allocated all free seats to a single Block - all other Blocks are fully allocated.

?So have we obtained "the optimal solution"? We still have to check whether there are other solutions that are optimal. In the MiniZinc model, we can do this by converting the optimization query to a satisfaction query - the metrics in the optimal solution (num_allocations, and max_distance) are converted into constraints, and we ask the solver to generate all satisfying solutions. This needs a couple of modifications in the model which I have indicated as comments in the model. Additionally we need to modify the solver configuration to instruct the tool to display all satisfying solutions (there is a single checkbox in MiniZinc for this setting). It turns out that there are actually 4 different solutions that are optimal. One of the candidate solutions is:

We can notice that the main difference is how free space is spread across the Blocks; in the above solution two Blocks have some free space (BlockC - 3 seats; and BlockD - 1 seat). We can add a minimization objective to avoid this kind of disparity between the Block assignments (seating_model_optimal.mzn). The solution we now obtain is:

Now checking for all solutions that are optimal with this optimization objective, we find that we have finally found the unique optimal seating solution.?

The Real World

Summarizing the situation so far, given the data-set of Block sizes and Group sizes, and a few easily explainable optimization objectives, I have found an optimal solution to the seat-allocation problem - it is in-fact the unique optimal solution given the set of optimization objectives used. Note that the process of arriving at this result was far more tortuous than I have described above, I had to dig my way out of many rabbit-holes of incorrect models, unsatisfiable problems, and tweaking of solver settings. The entire exercise took approximately 6 hours of playing with the tool over a couple of days.

So what actually happened to the seat-allocation exercise of the committee? Well, I took this assignment to the committee, they patiently listened to the way I had modelled it, my optimal solution, along with a few other proposals for seat-allocation from other committee members. As a group, we looked at all the proposals, and something magical happened - the committee members started negotiating and trading off on group sizes and locations, changed the composition of the Groups (remember that this was a top-level grouping, and this grouping had logical sub-group structure), moved around allocations on a white-board, discussed other aspects of team-interactions and dynamics and came to a completely different allocation.

Was this the optimal solution? I am not certain - I am not able to mathematically point out the optimization criteria used. However, I do know that one optimization criteria that I had not used in my mathematical model was consensus built by joint problem-solving - the committee members put their skin in the game and jointly solved the problem and looked each other in the eye to make sure that everyone agreed! The value of the modelling exercise I had undertaken was perhaps the seed solutions it generated and clarity on the principles to be followed in solving the problem (the optimization criteria!).