3.3. Visualising solutions in the MiniZinc IDE

The MiniZinc IDE provides a web-browser based system for visualising solutions generated by MiniZinc.

3.3.1. Visualisation library

In order to use these features, the library file ide/vis.mzn must be included:

include "ide/vis.mzn";

Running a model with a visualisation will automatically launch a web browser page containing the visualisation. If this page is closed, it can be reopened by clicking the hyperlink on the right side of the run’s output.

3.3.2. Pre-defined visualisations

There are a number of pre-defined visualisations to suit common use cases, such as line graphs, scatter plots, bar charts, graph visualisation, and 2D packing visualisation. Multiple visualisations can be shown concurrently.

These come in the form of functions which used as the value of an output item.

Documentation for these is available in MiniZincIDE solution visualisation tools.

An example model with a visualisation for a graph along with a time series line graph of the objective value is shown in Listing 3.3.1.

Listing 3.3.1 Minimum spanning tree data visualisation (vis_mst.mzn).
include "globals.mzn";
include "ide/vis.mzn";

% Graph definition
enum NODE = {A, B, C, D, E, F, G, H, I, J};
array [int] of NODE: from = [A, A, A, B, B, B, B, C, C, D, D, E,  E, F, F, F, G,  G, H, H, I];
array [int] of NODE:   to = [B, C, E, C, D, E, G, D, F, F, G, G,  J, G, H, I, I,  J, I, J, J];
array [int] of int:     w = [3, 6, 9, 4, 2, 9, 9, 2, 9, 9, 8, 8, 18, 7, 4, 5, 9, 10, 1, 4, 3];

% Find the minimum spanning tree of the graph
var 0..sum(w): total_weight;
array [index_set(from)] of var bool: es;
constraint weighted_spanning_tree(
  card(NODE),   % Number of nodes
  length(from), % Number of edges
  from,         % Edge from node
  to,           % Edge to node
  w,            % Weight of edge
  es,           % Whether edge is in spanningtree
  total_weight  % Total weight of spanning tree
);
solve minimize total_weight;

% Graph visualisation
array [int] of string: edge_labels = [i: show(w[i]) | i in index_set(w)];
output vis_graph_highlight(
  from,                  % Edge from node
  to,                    % Edge to node
  edge_labels,           % Edges are labelled with their weights
  [i: true | i in NODE], % All nodes are present in a spanning tree
  es                     % Whether edge is in spanningtree
);

% Objective visualisation
output vis_line(total_weight, "Spanning tree weight");
images/mst.png

Fig. 3.3.1 Minimum spanning tree visualisation result

3.3.3. Custom visualisations

A user-defined visualisation can be created by making use of the visualisation JavaScript API from an HTML page.

The visualisation is setup using an output item annotated with vis_server:

The call to vis_server takes a path to an HTML file to load (relative to the model), and can optionally be given some initialisation user data (init_data) that is sent upon loading the page. Then, on each solution, the output expression (solution_data) is sent to the page.

Note that the initial user data and the solution data are sent as JSON objects, so it is generally convenient to use records (see Tuple and record types), and you may wish to do some processing either in

Multiple such output items can be used to start concurrent visualisations.

The HTML page is loaded in an embedded web server and has access to the MiniZincIDE JavaScript API, served at /minizinc-ide.js. The HTML page can use this API to subscribe to events from the IDE and update its visualisation accordingly.

3.3.3.1. Example visualisation

In this example, we will create a visualisation for a version of the colouring problem introduced in MiniZinc基本模型.

images/aust1.svg

Fig. 3.3.2 Australia colouring visualisation result

All files should be placed in the same directory so that they are properly served by the IDE’s embedded web server.

Listing 3.3.2 Australia colouring data visualisation model (vis_aust.mzn).
include "ide/vis.mzn";

int: n_colors;

enum PALETTE = { red, lime, blue, cyan, magenta, yellow, orange };
set of PALETTE: COLOR = to_enum(PALETTE, 1..n_colors);

% Color for each region
var COLOR: wa;
var COLOR: nt;
var COLOR: sa;
var COLOR: q;
var COLOR: nsw;
var COLOR: v;
var COLOR: t;

% Neighboring regions have different colours
constraint wa != nt;
constraint wa != sa;
constraint nt != sa;
constraint nt != q;
constraint sa != q;
constraint sa != nsw;
constraint sa != v;
constraint q != nsw;
constraint nsw != v;

% Data to send during initialisation of the visualisation
any: initial_data = (n: n_colors);

% Data to send on each solution
% Note the use of :: output_only
any: solution_data :: output_only = (
  wa: show(wa), % Get colors as strings
  nt: show(nt),
  sa: show(sa),
  q: show(q),
  nsw: show(nsw),
  v: show(v),
  t: show(t)
);
% Launch the visualisation
output :: vis_server("vis_aust.html", initial_data) solution_data;

The MiniZinc model contains an output item annotated with vis_server. This initialises the visualisation, telling the IDE what page to load, and the user data to pass to it. In this case, we are passing the input number of colours so it can be shown on the visualisation.

The solution data is given as a record mapping regions to their string color names. If we didn’t convert these to strings, we would have to extract their names from the JSON enum output format in the visualisation script.

Passing JSON data to the visualisation

It should be noted that showJSON() is used on the user/solution data to convert them into JSON for the visualisation script. While this supports all MiniZinc values including sets and enums, the format used may need special handling in the visualisation script.

In many cases, it may be easier to convert sets into arrays and enums into strings to make them easier to deal with. For more information about the JSON format generated, see JSON support.

Another important thing to note is that when you place the solution data in its own declaration, you will likely need annotate it with :: output_only to ensure that does not get evaluated during compilation.

Listing 3.3.3 Australia colouring data visualisation HTML page (vis_aust.html).
<!DOCTYPE html>
<html>
  <head>
    <meta charset="utf-8">
    <title>Australia Visualisation</title>
    <script src="/minizinc-ide.js"></script>
    <style>
      html, body {
        margin: 0;
        padding: 0;
        overflow: hidden;
        font-family: Helvetica, sans-serif;
      }
      * {
        box-sizing: border-box;
      }
      main {
        width: 100vw;
        height: 100vh;
        padding: 50px;
      }
      svg {
        width: 100%;
        height: 100%;
      }
      .shapes {
        fill: none;
        stroke: #000;
        stroke-linejoin: round;
        stroke-linecap: round;
        stroke-width: 1;
      }
      .labels {
        font-family: sans-serif;
        font-size: 16px;
        text-anchor: middle;
        fill: #000;
      }
    </style>
  </head>
  <body>
    <main>
      <h3>Map coloring with <span id="count">n</span> colors</h3>
      <svg viewBox="0 0 412 357.33">
        <g class="shapes">
          <path id="wa" d="m152 67.333v-6l-18-18-24 6-24 30-78 36-6 12v18l12 24 12 60-12 18 24 12h24l30-18h30l29.68-8.72z" />
          <path id="nt" d="m152 67.333 6-12 18-24h66l-6 24 12 30 6 2.72v81.28h-102v-102" />
          <path id="q" d="m254 88.053 24 9.28h12l6-48 12-48 36 78 42 42 18 24 6 42-3.6 10.8h-1.2l-3.6-1.2-3.6-2.4-3.6 1.2-8.4-2.4h-108v-24h-24v-81.28" />
          <path id="nsw" d="m406.4 198.13-8.4 31.2-12 6-18 48-20.4-4.8-9.6-8.4-6 2.4-14.4-3.6-8.4-6-14.4-3.6-16.8-8.4v-57.6h108l8.4 2.4 3.6-1.2 3.6 2.4 3.6 1.2z" />
          <path id="v" d="m368 283.33-20.4-4.8-9.6-8.4-6 2.4-14.4-3.6-8.4-6-14.4-3.6-16.8-8.4v40.8l24 9.6 12-6 18 6 18-12z" />
          <path id="sa" d="m278 169.33h-126l-0.32 63.28 12.32-3.28h36l24 30 18-24v13.2l-6 22.8h24l12 18 6 2.4v-122.4" />
          <path id="t" d="m320 319.33 12 6h6l9.6-6.32 8.4 6-2.08 18.64-15.92 11.68-18-12-6-12 6-12" />
        </g>
        <g class="labels">
          <text x="83.533119" y="170.0192">WA</text>
          <text x="201.66409" y="123.36276">NT</text>
          <text x="328.74969" y="147.87715">Q</text>
          <text x="334.34839" y="237.23608">NSW</text>
          <text x="314.19815" y="289.03265">V</text>
          <text x="336.71103" y="344.3877">T</text>
          <text x="213.65285" y="209.55853">SA</text>
        </g>
      </svg>
    </main>
    <script src="vis_aust.js"></script>
  </body>
</html>

The visualisation page includes the script /minizinc-ide.js, which is provided by the embedded web server. This allows access to the MiniZinc IDE JavaScript API using the global MiniZincIDE object. The page contains an SVG element containing the basic parts of the visualisation, ready to be coloured when a solution is produced. Another script, vis_aust.js is loaded with the visualisation logic.

Listing 3.3.4 Australia colouring data visualisation script (vis_aust.js).
const HTML_COLORS = ['red', 'yellow', 'blue', 'lime', 'magenta', 'cyan', 'orange'];

(async function() {
  // getUserData can be used to retrieve the JSON data passed to vis_server()
  const userData = await MiniZincIDE.getUserData();
  document.getElementById('count').textContent = userData.n;
  
  // Handler to set the colors for the solution
  function setSolution(data) {
    for (const r in data) {
      document.getElementById(r).setAttribute('fill', data[r]);
    }
  }

  // Visualise last solution on startup
  const numSols = await MiniZincIDE.getNumSolutions();
  if (numSols > 0) {
    const solution = await MiniZincIDE.getSolution(numSols - 1);
    setSolution(solution.data);
  }

  // Show new solutions if we're following the latest solution
  let followLatest = true;
  MiniZincIDE.on('solution', (solution) => {
    if (followLatest) {
      setSolution(solution.data);
    }
  });

  MiniZincIDE.on('goToSolution', async (index) => {
    // Requesting index -1 turns on following latest solution
    // Otherwise, we stop showing the latest solution and show the requested one
    followLatest = index === -1;
    const solution = await MiniZincIDE.getSolution(index);
    setSolution(solution.data);
  })
})();

The script uses an asynchronous immediately invoked function expression, allowing us to easily use the asynchronous functions in the MiniZincIDE JavaScript API. MiniZincIDE.getUserData() allows us to retrieve the data we passed to vis_server. The function setSolution(data) is defined to handle the solution data and update the visualisation. We load the latest solution using MiniZincIDE.getSolution(idx) if one exists on startup, in case the visualisation page is refreshed or open after solving has begun. The solution and goToSolution events are subscribed to, so we know when to update the visualisation.

3.3.3.2. MiniZincIDE JavaScript API

The MiniZincIDE JavaScript API provides an asynchronous interface between the IDE and visualisations.

MiniZincIDE.on(event, callback)

Subscribes to the event event and call callback whenever it occurs. The valid events are:

  • solution: triggered when a new solution is produced. The callback function is passed an object containing the time of the solution in milliseconds and the data from the associated vis_json output statement.

    MiniZincIDE.on('solution', function(solution) {
      console.log(solution.time);
      console.log(solution.data);
    });
    
  • goToSolution: triggered when the user has selected a particular solution to visualise. The callback function is passed the solution index to display, or -1 if the user has enabled following the latest solution. Visualisations which support showing a particular solution should subscribe to this event.

    MiniZincIDE.on('goToSolution', async function(index) {
      const solution = await MiniZincIDE.getSolution(index);
      visualiseSolution(solution);
    });
    
  • status: triggered when a final status line is received (such as ==========). The callback function is passed an object containing the status and time in milliseconds. The status value can be one of

    • ALL_SOLUTIONS

    • OPTIMAL_SOLUTION

    • UNSATISFIABLE

    • UNSAT_OR_UNBOUNDED

    • UNBOUNDED

    • UNKNOWN

    • ERROR

  • finish: triggered when solving finishes (or is stopped). The callback function is passed the time when solving finished in milliseconds.

MiniZincIDE.off(event, callback)

Unsubscribes from an event given the event name and callback function.

MiniZincIDE.getUserData()

Returns a Promise which resolves to the user data passed to ide_launch_server().

MiniZincIDE.goToSolution(idx)

Requests that the solution with the given index idx is shown. This causes the goToSolution event to be triggered for all visualisations being shown. Visualisations which allow multiple solutions to displayed simultaneously can call this function when the user interacts on a particular solution. This allows other visualisations to then also show the solution of interest.

The index -1 is used to request that the latest solution be tracked by the visualisations.

MiniZincIDE.solve(modelFile, dataFiles, options)

Requests that the IDE stop solving the current instance and start solving with the given modelFile, dataFiles, and parameter configuration options modelFile and dataFiles may be set to null to re-solve using the current model and data files. Otherwise, modelFile is the path to the .mzn file to solve and dataFiles is an array of paths to the .dzn or .json files. These must be in the same directory or a child directory of the current model. options is an optional object in the parameter configuration file format (see Command-line Parameter Files) to be passed to MiniZinc (in addition to the current solver configuration).

MiniZincIDE.getNumSolutions()

Returns a Promise which resolves to the number of solutions which have been found.

MiniZincIDE.getSolution(index)

Returns a Promise which resolves to the solution object (containing time and data) for the given index. Negative indexes refer to indexes from the end (e.g. -1 refers to the latest solution).

MiniZincIDE.getAllSolutions()

Returns a Promise which resolves to an array of all solution objects (each containing time and data).

MiniZincIDE.getStatus()

Returns a Promise which resolves to an object containing the time and final status, or null if there is no final status.

MiniZincIDE.getFinishTime()

Returns a Promise which resolves to the finishing time, or null if it has not finished.