A clojure2minizinc Tutorial

MiniZinc is a highly specialised and rather small language. It lacks many features of standard programming languages. clojure2minizinc marries MiniZinc with Clojure and that way many concepts of general purpose languages (in the guise of their Clojure implementation) can be used for a MiniZinc program.

For example, a clojure2minizinc program is defined in a Clojure namespace. The following code block defines a namespace for this tutorial. Note that clojure2minizinc "overwrites" many standard Clojure functions. You may want to use the library with a namespace prefix. The definitions below uses the alias mz (for MiniZinc).

(ns clojure2minizinc.tutorial
  (:require [clojure2minizinc.core :as mz]  ; loading clojure2minizinc.core 
            [clojure.pprint :as pprint]))   ; pprint is needed later...

The library clojure.pprint will be needed later. We already add them here for convenience.

The first example defines a map-colouring of Australia. The MiniZinc tutorial, p. 3ff, motivates and explains this model. This tutorial assumes that you read the MiniZinc tutorial alongside. To help you with that, even the same headlines are used.

Notice that most functions in this example are in the mz namespace, but the decision variables (and an int) of the model are stored with the standard Clojure let form – clojure2minizinc allows to store MiniZinc variables and parameters (constants) in arbitrary Clojure data structures.

(def aust
  (mz/clj2mnz
   (let [nc (mz/int 'nc 3)              ; number of colours
         wa (mz/variable (mz/-- 1 nc))  ; 7 variables for 7 states
         nt (mz/variable (mz/-- 1 nc))
         sa (mz/variable (mz/-- 1 nc))
         q (mz/variable (mz/-- 1 nc))
         nsw (mz/variable (mz/-- 1 nc))
         v (mz/variable (mz/-- 1 nc))
         t (mz/variable (mz/-- 1 nc))]
     (mz/constraint (mz/!= wa nt))
     (mz/constraint (mz/!= wa sa))
     (mz/constraint (mz/!= nt sa))
     (mz/constraint (mz/!= nt q))
     (mz/constraint (mz/!= sa q))
     (mz/constraint (mz/!= sa nsw))
     (mz/constraint (mz/!= sa v))
     (mz/constraint (mz/!= nsw v))
     (mz/solve :satisfy)
     (mz/output-map {:wa wa :nt nt :sa sa :q q :nsw nsw :v v :t t}))))

We can solve this MiniZinc model as follows.

(mz/minizinc aust)

It returns the following result. Different numbers encode different colours on the map for the Australian states.

; => ({:wa 1, :nt 2, :sa 3, :q 1, :nsw 2, :v 1, :t 1})

In this example, a solution is wrapped in a Clojure map. You can ask for multiple solutions, if you like.

(mz/minizinc aust :num-solutions 3)

; => ({:wa 1, :nt 2, :sa 3, :q 1, :nsw 2, :v 1, :t 1} {:wa 2, :nt 1, :sa 3, :q 2, :nsw 2, :v 1, :t 1} {:wa 1, :nt 3, :sa 2, :q 1, :nsw 3, :v 1, :t 1})

In fact, you can specify arbitrary options supported by the minizinc shell command. The next code line specifies to use (the FlatZinc interpreter of) Gecode (which must of could be installed). This solver won many MiniZinc Challenges and is much more efficient than the solver that minizinc uses by default. For this simple model this makes no real difference (most time is spend on the translation of MiniZinc to FlatZinc here), but for more complex problems the difference can be huge.

(mz/minizinc aust :options ["-f fzn-gecode"])

The solution happens to be different, because different solvers may use different search strategies, which can lead to different first solutions. (MiniZinc also allows to specify the search strategy, within certain bounds).

; => ({:wa 3, :nt 2, :sa 1, :q 3, :nsw 3, :v 2, :t 1})

In the next call we ask Gecode to use 8 threads and/or cores for a parallel search. Again, this makes only a real difference for more complex problems.

(mz/minizinc aust :options ["-f fzn-gecode" "-p8"])

For more information on solver options see the help screen of minizinc. Type at a terminal.

$ minizinc --help

The MiniZinc tutorial continues with an optimisation example, that computes the number of banana (b) and chocolate (c) cakes to bake for maximum profit given the recipes for these cakes, the amount of ingredients, and the price at which each cake can be sold.

The corresponding clojure2minizinc code is shown below. Please see the MiniZinc tutorial for an explanation of this model.

(mz/minizinc 
 (mz/clj2mnz
  (let [b (mz/variable (mz/-- 1 100))
        c (mz/variable (mz/-- 1 100))]
    ;; flour
    (mz/constraint (mz/<= (mz/+ (mz/* 250 b)
                                (mz/* 200 c))
                          4000))
    ;; bananas
    (mz/constraint (mz/<= (mz/* 2 b) 6))
    ;; sugar
    (mz/constraint (mz/<= (mz/+ (mz/* 75 b)
                                (mz/* 150 c))
                          2000))
    ;; butter 
    (mz/constraint (mz/<= (mz/+ (mz/* 100 b)
                                (mz/* 150 c))
                          500))
    ;; cocoa
    (mz/constraint (mz/<= (mz/* 75 c) 500))
    ;; maximise profit
    (mz/solve :maximize (mz/+ (mz/* 400 b) (mz/* 450 c)))
    (mz/output-map {:banana-cakes b :chocolate-cakes c}))))

The optimal solution are two cakes of each kind.

; => ({:banana-cakes 2, :chocolate-cakes 2})

In the previous example, the amount of each ingredient was fixed in the model. MiniZinc supports parameterising models, where MiniZinc parameters or variables are declared but not further initialised. Values for this parameters/variables are specified outside of the model to the solver, usually with MiniZinc data files.

The clojure2minizinc version of the parameterised model is shown below. Again, please see the MiniZinc tutorial (p. 8ff) for an explanation of this model.

Note that we must specify explicit names for the parameters of a parameterised model (here flour, banana, sugar, and so forth), so that these names are the same as in the parameter file (i.e., automatically generated names would not work).

(def cakes2
  (mz/clj2mnz
   (let [flour (mz/int 'flour)
         banana (mz/int 'banana)
         sugar (mz/int 'sugar)
         butter (mz/int 'butter)
         cocoa (mz/int 'cocoa)]
     (mz/constraint (mz/assert (mz/>= flour 0) "Amount of flour must not be negative"))
     (mz/constraint (mz/assert (mz/>= banana 0) "Amount of banana must not be negative"))
     (mz/constraint (mz/assert (mz/>= sugar 0) "Amount of sugar must not be negative"))
     (mz/constraint (mz/assert (mz/>= butter 0) "Amount of butter must not be negative"))
     (mz/constraint (mz/assert (mz/>= cocoa 0) "Amount of cocoa must not be negative"))
     (let [b (mz/variable (mz/-- 1 100))
           c (mz/variable (mz/-- 1 100))]
       ;; flour
       (mz/constraint (mz/<= (mz/+ (mz/* 250 b)
                                   (mz/* 200 c))
                             flour))
       ;; bananas
       (mz/constraint (mz/<= (mz/* 2 b) banana))
       ;; sugar
       (mz/constraint (mz/<= (mz/+ (mz/* 75 b)
                                   (mz/* 150 c))
                             sugar))
       ;; butter 
       (mz/constraint (mz/<= (mz/+ (mz/* 100 b)
                                   (mz/* 150 c))
                             butter))
       ;; cocoa
       (mz/constraint (mz/<= (mz/* 75 c) cocoa))
       ;; maximise profit
       (mz/solve :maximize (mz/+ (mz/* 400 b) (mz/* 450 c)))
       (mz/output-map {:banana-cakes b :chocolate-cakes c})))))

In clojure2minizinc, the parameters for a model are given directly to the solver. The code below specifies the same amounts of ingredients for the cakes as the original example, and therefore the result is the same.

(mz/minizinc cakes2
  :data (mz/map2minizinc {:flour 4000 :banana 6 :sugar 2000 :butter 500 :cocoa 500}))

; => ({:banana-cakes 2, :chocolate-cakes 2})

Different amounts have a different optimal result.

(mz/minizinc cakes2
  :data (mz/map2minizinc {:flour 8000 :banana 11 :sugar 3000 :butter 1500 :cocoa 800}))

; => ({:banana-cakes 3, :chocolate-cakes 8})

The next example demonstrates constraint programming on "real numbers" (floating point variables). The example models the repayment of a loan with interest over four quarters.

The model is also parameterised – values for variables r, p and so forth can be specified to the solver. Remember that we must specify explicit names for these variables (they should not be named automatically).

(def loan
  (mz/clj2mnz
   (let [r (mz/variable :float 'r)           ; quarterly repayment
         p (mz/variable :float 'p)           ; principal initially borrowed
         i (mz/variable (mz/-- 0.0 10.0) 'i) ; interest rate
         ;; intermediate variables 
         b1 (mz/variable :float 'b1)         ; balance after one quarter
         b2 (mz/variable :float 'b2)         ; balance after two quarters
         b3 (mz/variable :float 'b3)         ; balance after three quarters
         b4 (mz/variable :float 'b4)]        ; balance owing at end
     (mz/constraint (mz/= b1 (mz/- (mz/* p (mz/+ 1.0 i)) r)))
     (mz/constraint (mz/= b2 (mz/- (mz/* b1 (mz/+ 1.0 i)) r)))
     (mz/constraint (mz/= b3 (mz/- (mz/* b2 (mz/+ 1.0 i)) r)))
     (mz/constraint (mz/= b4 (mz/- (mz/* b3 (mz/+ 1.0 i)) r)))
     (mz/solve :satisfy)
     (mz/output-map {:borrowing p :interest-rate (mz/* i 100.0)
                     :repayment-per-quarter r
                     :owing-at-end b4}))))

The default MiniZinc solver (mzn-g12fd) does not support floating point variables, so we can use Gecode again. A solution is shown below the solver call.

(mz/minizinc loan :options ["-f fzn-gecode"] 
  :data (mz/map2minizinc {:i 0.04 :p 1000.0 :r 260.0}))

; => ({:borrowing 1000.0, :interest-rate 4.00000000000001, :repayment-per-quarter 260.0, :owing-at-end 65.7779200000003})

In constraint programming any variable can be quasi input or output of the algorithm. Instead of setting the values for r, p and i in the solver call, we can set the values for other variables. By setting b4 to 0 we specify that the loan is fully payed back after four quarters.

(mz/minizinc loan :options ["-f fzn-gecode"] 
  :data (mz/map2minizinc {:i 0.04 :p 1000.0 :b4 0.0}))

; => ({:borrowing 1000.0, :interest-rate 4.00000000000001, :repayment-per-quarter 275.490045364803, :owing-at-end 0.0})

Here are again other variables set before the search.

(mz/minizinc loan :options ["-f fzn-gecode"] 
  :data (mz/map2minizinc {:i 0.04 :r 250.0 :b4 0.0}))

; => ({:borrowing 907.473806064214, :interest-rate 4.00000000000001, :repayment-per-quarter 250.0, :owing-at-end 0.0})

If you do not have Gecode installed, you can also use the solver mzn-g12mip, which comes with MiniZinc. The result happens to be slightly different.

(mz/minizinc loan :solver "mzn-g12mip"
  :data (mz/map2minizinc {:i 0.04 :r 250.0 :b4 0.0}))

; => ({:borrowing 907.4738060642132, :interest-rate 4.0, :repayment-per-quarter 250.0, :owing-at-end 0.0})

This example demonstrates the use of a two-dimensional array of float variables. It models temperatures on a rectangular sheet of metal. The MiniZinc tutorial explains the details.

In order to make the result better comprehensible, we will print it in table form instead of just returning the result. We need an auxiliary function that prints a table. Lets use print-table that is shown as an example for get-pretty-writer at http://clojure.github.io (print-table is only slightly edited here). This function is the reason why we require'd clojure.pprint in the name space definition above.

(defn print-table [column-width aseq]
  (binding [*out* (pprint/get-pretty-writer *out*)]
    (doseq [row aseq]
      (doseq [col row]
        (pprint/cl-format true "~6,2F~7,vT" col column-width))
      (prn))))

Now we can present the clojure2minizinc version of the Laplace model from the MiniZinc tutorial.

(let [width 5
      height 5]
  (print-table 2
   (partition (+ 1 height)  ;; add one, because array boundaries are [0, height] etc.
    (first 
     (mz/minizinc 
      (mz/clj2mnz
       (let [w (mz/int 'w width)
             h (mz/int 'h height)
             ;; array decl
             t (mz/array (list (mz/-- 0 w) (mz/-- 0 h)) [:var :float] 't)
             left (mz/variable :float 'left)
             right (mz/variable :float 'right)
             top (mz/variable :float 'top)
             bottom (mz/variable :float 'bottom)]
         ;; Laplace equation
         ;; Each internal temp. is average of its neighbours
         (mz/constraint 
          (mz/forall [i (mz/-- 1 (mz/- w 1))
                      j (mz/-- 1 (mz/- h 1))]
                     (mz/= (mz/* 4.0 (mz/nth t i j))
                           ;; Constraints like + support an arbitray number of arguments 
                           (mz/+ (mz/nth t (mz/- i 1) j)
                                 (mz/nth t i (mz/- j 1))
                                 (mz/nth t (mz/+ i 1) j)
                                 (mz/nth t i (mz/+ j 1))))))
         ;; edge constraints
         (mz/constraint (mz/forall [i (mz/-- 1 (mz/- w 1))]
                                   (mz/= (mz/nth t i 0) left)))
         (mz/constraint (mz/forall [i (mz/-- 1 (mz/- w 1))]
                                   (mz/= (mz/nth t i h) right)))
         (mz/constraint (mz/forall [j (mz/-- 1 (mz/- h 1))]
                                   (mz/= (mz/nth t 0 j) top)))
         (mz/constraint (mz/forall [j (mz/-- 1 (mz/- h 1))]
                                   (mz/= (mz/nth t w j) bottom)))
         ;; corner constraints
         (mz/constraint (mz/= (mz/nth t 0 0) 0.0))
         (mz/constraint (mz/= (mz/nth t 0 h) 0.0))
         (mz/constraint (mz/= (mz/nth t w 0) 0.0))
         (mz/constraint (mz/= (mz/nth t w h) 0.0))
         (mz/constraint (mz/= left 0.0))
         (mz/constraint (mz/= right 0.0))
         (mz/constraint (mz/= top 100.0))
         (mz/constraint (mz/= bottom 0.0))
         (mz/solve :satisfy)
         ;; 2d-array output as flat 1d array -- formatting of result done by Clojure
         (mz/output-var t) 
         ))
      :options ["-f fzn-gecode"]
      ; :solver "mzn-g12mip"
      )))))

In this model, the top-level call is print-table. The model therefore returns only nil, but prints the following result at the REPL.

  0.00 100.00  100.00  100.00  100.00    0.00  
  0.00  45.45   59.47   59.47   45.45    0.00  
  0.00  22.35   32.95   32.95   22.35    0.00  
  0.00  10.98   17.05   17.05   10.98    0.00  
  0.00   4.55    7.20    7.20    4.55    0.00  
  0.00   0.00    0.00    0.00    0.00    0.00

Note that in the actual Laplace equation in the code above, the mz/+ constraint takes four arguments. Unlike MiniZinc, where such arithmetic operators are only binary (infix operators), their clojure2minizinc counterparts support an arbitrary number of arguments, in true Lisp spirit.

However, you can already move on to the next section…

The syntax of MiniZinc and clojure2minizinc differs clearly. The MiniZinc notation is close to an ASCII version of standard math notation, while in clojure2minizinc all code is expressed by standard Lisp S-expressions.

Nevertheless, most MiniZinc operators, functions etc. are called exactly the same in clojure2minizinc. For example the following two code snippets show a MiniZinc code line and the corresponding clojure2minizinc code (without namespace prefixes).

constraint x + y != z;

(constraint (!= (+ x y) z))

Because of this similarity of code, the main documentation of clojure2minizinc is the MiniZinc documentation itself.

There are a few exceptions, where certain MiniZinc operator etc. names cannot be translated into Clojure due to certain restrictions of Clojure. The differences between MiniZinc operators, keywords etc. and the corresponding Clojure functions are listed in the table below.

Several literal Clojure types can be used directly in clojure2minizinc for corresponding literal MiniZinc parameter types. The exception are Clojure strings.

Two-dimensional MiniZinc arrays can be encoded by nested Clojure vectors. The nested vectors

[[1.0 2.0] [3.0 4.0]]

corresponds to the MiniZinc code

[| 1.0, 2.0 | 3.0, 4.0 |]

The Constraint Programming community developed many solvers, and a considerable number of them extends a programming language directly. Such close integration has clear advantages. E.g., custom search strategies can be programmed using the full power of the host language (if the solver supports it).

clojure2minizinc's inherits from MiniZinc the advantage that it is solver-independent: any solver supporting FlatZinc as input can be used.

Constraint programming provides a very high level of abstraction for the programmer. However, this strength comes with a certain price. In particular, software using constraint programming can be hard to debug. Even worse, error messages by MiniZinc currently refer to line numbers of the generated MiniZinc code, not the clojure2minizinc code. However, constraint problem debuggers are not too helpful anyway. Often it is necessary to carefully analyse a model in order to understand why it does not work as intended.

A useful and easy debugging strategy is to disable a set of constraints and to enable them one by one again in order to find the problem. Another useful debugging aid is the search tree visualiser and interactive search tool gist provided by Gecode. It can be enabled with the -mode option. For more information see the Gecode tutorial, p. 157ff.

(mz/minizinc aust :options ["-f fzn-gecode" "--fzn-flags '-mode gist'"])

TODO: get code above working – it works at the shell, but not yet in clojure2minizinc