Friday, October 6, 2017

von Koch and MiniZinc

image

A MiniZinc [1] version of the graceful labeling model in [3] was sent to me [4]. This looks actually quite nice, so therefore I reproduce it here:

include "globals.mzn";
 
%
% Definition of data
%
 
% Number of nodes in the graph
int: nodes;
set of int: Nodes = 1..nodes;
 
% Connections
int: connections;
set of int: Connections = 1..connections;
array[Connections,1..2] of int: ConnectionEdges;
 
%
% Instance from http://yetanothermathprogrammingconsultant.blogspot.se/2017/09/von-koch-and-z3.html
% The following data could be located in a minizinc data file instead.
%
nodes = 7;
connections = 6;
ConnectionEdges =
         [|  1,  2,
          |  1,  4,
          |  1,  7,
          |  2,  3,
          |  2,  5,
          |  5,  6,
          |];
 
%
% Model proper
%
 
array[Nodes] of var 1..nodes: NodeLabel;
array[Connections] of var 1..connections: ConnectionLabel;
 
constraint alldifferent(NodeLabel) :: domain;
 
constraint alldifferent(ConnectionLabel) :: domain;
 
constraint forall(connection in Connections) (
    ConnectionLabel[connection] = abs(NodeLabel[ConnectionEdges[connection, 1]] - NodeLabel[ConnectionEdges[connection, 2]])
);

 
solve satisfy;
 
output [
  "NodeLabels: " ++ show(NodeLabel) ++
  " ConnectionLabels: " ++ show(ConnectionLabel) ++
  "\n"
  ];

MiniZinc comes with an IDE so that makes it easy to edit and run the model:

image

This is solved with the Gecode [2] Constraint Programming solver.

Generating all solutions is just a question of changing a setting:  

image

Indeed we get all solutions:

image

References
  1. http://www.minizinc.org/
  2. http://www.gecode.org/
  3. von Koch and Z3, http://yetanothermathprogrammingconsultant.blogspot.com/2017/09/von-koch-and-z3.html
  4. Mikael Zayenz Lagerkvist, private communication