Disjoint rectangles

The following program finds seven non-overlapping rectangles that fill a grid. You can set any of the rectangles’ coordinates or areas and Sentient will figure out the rest.

function main() {
  int gridWidth, gridHeight;

  array7<array4<int>> rectangles;
  array7<int> areas;

  rectangles.eachCombination(2, function (arr) {
    invariant !arr[0].overlap?(arr[1]);
  });

  rectangles.each(function^ (s, index) {
    invariant s.top >= 0, s.left >= 0;
    invariant s.bottom <= gridHeight, s.right <= gridWidth;
    invariant s.top < s.bottom, s.left < s.right;

    width = s.right - s.left;
    height = s.bottom - s.top;

    invariant areas[index] == width * height;
  });

  invariant areas.sum == gridWidth * gridHeight;

  expose gridWidth, gridHeight, rectangles, areas;
};

function overlap? (a, b) {
  return a.left < b.right && a.right > b.left
      && a.top < b.bottom && a.bottom > b.top;
};

function left (r) { return r[0]; };
function top (r) { return r[1]; };
function right (r) { return r[2]; };
function bottom (r) { return r[3]; };

main();

You can touch the example above to cycle through solutions. The areas for the yellow, red, orange, blue and green rectangles have been assigned to [2, 4, 6, 9, 9] respectively.

This program could potentially be useful for generating interesting layouts for photo galleries or web sites that use grid systems. It would be relatively straightforward to incorporate additional constraints to suit the problem.

How does it work?

We declare the width and height of the grid and an array of seven ‘rectangles’. Each is an array that contains four elements corresponding to the left, top, right and bottom edges of the rectangle. We also declare an array to hold the areas for the rectangles. Later on we expose these variables so that we may get/set their values at runtime.

We iterate through all pairs of rectangles with ‘eachCombination’ and specify an invariant that they do not overlap. The ‘overlap?’ function is called using Sentient’s method syntax and is based on this Stack Overflow answer.

We then iterate through each rectangle and check it lies within the bounds of the grid. We check that its top edge is above its bottom edge and that its left edge is left of its right edge. We specify an invariant that the area of this rectangle must equal one of the areas declared earlier. Finally, we insist that the total area of the rectangles equals the grid.

CLI example

Here is an example of running this program with the command-line interface:

sentient --run disjoint-rectangles.json --assign '{ gridWidth: 16, gridHeight: 9 }'

# standard output:
{
  "gridWidth":16,
  "gridHeight":9,
  "rectangles":[
    [0,4,2,6],
    [15,6,16,9],
    [0,0,16,4],
    [2,4,3,6],
    [11,4,16,6],
    [0,6,15,9],
    [3,4,11,6]
  ],
  "areas":[4,3,64,2,10,45,16]
}

You can read the above output in pairs, for example, the first rectangle spans the coordinates (0, 4) to (2, 6). You could optionally assign some of the rectangles:

sentient --run disjoint-rectangles.json \
         --assign '{ rectangles: { 0: [0, 0, 10, 10] } }'