2.3. Predicates and Functions

Predicates in MiniZinc allow us to capture complex constraints of our model in a succinct way. Predicates in MiniZinc are used to model with both predefined global constraints, and to capture and define new complex constraints by the modeller. Functions are used in MiniZinc to capture common structures of models. Indeed a predicate is just a function with output type var bool.

2.3.1. Global Constraints

There are many global constraints defined in MiniZinc for use in modelling. The definitive list is to be found in the documentation for the release, as the list is slowly growing. Below we discuss some of the most important global constraints.

2.3.1.1. Alldifferent

The alldifferent constraint takes an array of variables and constrains them to take different values. A use of the alldifferent has the form

alldifferent(array[int] of var int: x)

The argument is an array of integer variables.

The alldifferent constraint is one of the most studied and used global constraints in constraint programming. It is used to define assignment subproblems, and efficient global propagators for alldifferent exist. The models send-more-money.mzn (Listing 2.2.4) and sudoku.mzn (Listing 2.2.5) are examples of models using alldifferent.

2.3.1.2. Cumulative

The cumulative constraint is used for describing cumulative resource usage.

cumulative(array[int] of var int: s, array[int] of var int: d,
           array[int] of var int: r, var int: b)

It requires that a set of tasks given by start times s, durations d, and resource requirements r, never require more than a global resource bound b at any one time.

Listing 2.3.1 Model for moving furniture using cumulative (moving.mzn).
include "cumulative.mzn";

enum OBJECTS;
array[OBJECTS] of int: duration; % duration to move
array[OBJECTS] of int: handlers; % number of handlers required
array[OBJECTS] of int: trolleys; % number of trolleys required

int: available_handlers;
int: available_trolleys;
int: available_time;

array[OBJECTS] of var 0..available_time: start;
var 0..available_time: end;

constraint cumulative(start, duration, handlers, available_handlers);
constraint cumulative(start, duration, trolleys, available_trolleys);
 
constraint forall(o in OBJECTS)(start[o] +duration[o] <= end);

solve minimize end;

output [ "start = \(start)\nend = \(end)\n"];
Listing 2.3.2 Data for moving furniture using cumulative (moving.dzn).
OBJECTS = { piano, fridge, doublebed, singlebed, 
            wardrobe, chair1, chair2, table };

duration = [60, 45, 30, 30, 20, 15, 15, 15];
handlers = [3, 2, 2, 1, 2, 1, 1, 2];
trolleys = [2, 1, 2, 2, 2, 0, 0, 1];

available_time = 180;
available_handlers = 4;
available_trolleys = 3;

The model in Listing 2.3.1 finds a schedule for moving furniture so that each piece of furniture has enough handlers (people) and enough trolleys available during the move. The available time, handlers and trolleys are given, and the data gives for each object the move duration, the number of handlers and the number of trolleys required. Using the data shown in ex-movingd, the command

$ minizinc moving.mzn moving.dzn

may result in the output

start = [0, 60, 60, 90, 120, 0, 15, 105]
end = 140
----------
==========

Fig. 2.3.1 and Fig. 2.3.2 show the requirements for handlers and trolleys at each time in the move for this solution.

images/handlers.svg

Fig. 2.3.1 Histogram of usage of handlers in the move.

images/trolleys.svg

Fig. 2.3.2 Histogram of usage of trolleys in the move.

2.3.1.3. Table

The table constraint enforces that a tuple of variables takes a value from a set of tuples. Since there are no tuples in MiniZinc this is encoded using arrays. The usage of table has one of the forms

table(array[int] of var bool: x, array[int, int] of bool: t)
table(array[int] of var int:  x, array[int, int] of int:  t)

depending on whether the tuples are Boolean or integer. The constraint enforces \(x \in t\) where we consider \(x\) and each row in \(t\) to be a tuple, and \(t\) to be a set of tuples.

Listing 2.3.3 Model for meal planning using table constraint (meal.mzn).
% Planning a balanced meal
include "table.mzn";
int: min_energy;
int: min_protein;
int: max_salt;
int: max_fat;
set of FOOD: desserts;
set of FOOD: mains;
set of FOOD: sides;
enum FEATURE = { name, energy, protein, salt, fat, cost}; 
enum FOOD; 
array[FOOD,FEATURE] of int: dd; % food database

array[FEATURE] of var int: main;
array[FEATURE] of var int: side;
array[FEATURE] of var int: dessert;
var int: budget;

constraint main[name] in mains;
constraint side[name] in sides;
constraint dessert[name] in desserts;
constraint table(main, dd);
constraint table(side, dd);
constraint table(dessert, dd);
constraint main[energy] + side[energy] + dessert[energy] >=min_energy;
constraint main[protein]+side[protein]+dessert[protein] >=min_protein;
constraint main[salt] + side[salt] + dessert[salt] <= max_salt;
constraint main[fat] + side[fat] + dessert[fat] <= max_fat;
constraint budget = main[cost] + side[cost] + dessert[cost];

solve minimize budget; 

output ["main = ",show(to_enum(FOOD,main[name])), 
        ", side = ",show(to_enum(FOOD,side[name])),
        ", dessert = ",show(to_enum(FOOD,dessert[name])),
        ", cost = ",show(budget), "\n"];
Listing 2.3.4 Data for meal planning defining the table used (meal.dzn).
FOOD = { icecream, banana, chocolatecake, lasagna, 
          steak, rice, chips, brocolli, beans} ;

dd = [| icecream,      1200,  50,  10, 120,  400     % icecream
      | banana,         800, 120,   5,  20,  120     % banana
      | chocolatecake, 2500, 400,  20, 100,  600     % chocolate cake
      | lasagna,       3000, 200, 100, 250,  450     % lasagna
      | steak,         1800, 800,  50, 100, 1200     % steak
      | rice,          1200,  50,   5,  20,  100     % rice
      | chips,         2000,  50, 200, 200,  250     % chips
      | brocolli,       700, 100,  10,  10,  125     % brocolli
      | beans,         1900, 250,  60,  90,  150 |]; % beans

min_energy = 3300;
min_protein = 500;
max_salt = 180;
max_fat = 320;
desserts = { icecream, banana, chocolatecake };
mains = { lasagna, steak, rice };
sides = { chips, brocolli, beans };

The model in Listing 2.3.3 searches for balanced meals. Each meal item has a name (encoded as an integer), a kilojoule count, protein in grams, salt in milligrams, and fat in grams, as well as cost in cents. The relationship between these items is encoded using a table constraint. The model searches for a minimal cost meal which has a minimum kilojoule count min_energy, a minimum amount of protein min_protein, maximum amount of salt max_salt and fat max_fat.

2.3.1.4. Regular

The regular constraint is used to enforce that a sequence of variables takes a value defined by a deterministic finite automaton (DFA). The usage of regular has the form

regular(array[int] of var $$Val: x,
        array[$$State,$$Val] of opt $$State: d,
        $$State: q0, set of $$State: F)

We use the $$ prefix (here, $$Val and $$State) to indicate that these arguments can be of any enumerated type (including simple integers).

The regular constraint ensures that the sequence of values in array x is accepted by the DFA with transition function d, initial state q0 and accepting states F. The transition function maps a state and a value to another state. Let’s illustrate how to define the transition function using an example.

images/dfa.svg

Fig. 2.3.3 A DFA determining correct rosters.

Consider a nurse rostering problem. Each nurse is scheduled for each day as either: (d) on day shift, (n) on night shift, or (o) off. In each four day period a nurse must have at least one day off, and no nurse can be scheduled for 3 night shifts in a row. This can be encoded using the incomplete DFA shown in Fig. 2.3.3.

We can encode this DFA by introducing an enumerated type for the states

enum State = {S1, S2, S3, S4, S5, S6};

The start state is S1, all states are final states, and the transition function is given by the matrix

d

n

o

S1

S2

S3

S1

S2

S4

S4

S1

S3

S4

S5

S1

S4

S6

S6

S1

S5

S6

<>

S1

S6

<>

<>

S1

Note that value <> in the table indicates an error state, i.e., an illegal transition. This is an example of an option type, which will be discussed in more detail in Section 2.4.

The model shown in Listing 2.3.5 finds a schedule for the nurses defined by enum NURSE over the days defined by enum DAYS, where we require req_day nurses on day shift each day, and req_night nurses on night shift, and that each nurse takes at least min_night night shifts.

Listing 2.3.5 Model for nurse rostering using regular constraint (nurse.mzn)
% Simple nurse rostering
include "regular.mzn";
enum NURSE;
enum DAY;
int: req_day;
int: req_night;
int: min_night;

enum SHIFT = { d, n, o };

enum STATE = { S1, S2, S3, S4, S5, S6 };

array[STATE,SHIFT] of opt STATE: t =
     [|      d:  n:  o:
      | S1:  S2, S3, S1
      | S2:  S4, S4, S1
      | S3:  S4, S5, S1
      | S4:  S6, S6, S1
      | S5:  S6, <>, S1
      | S6:  <>, <>, S1|];

array[NURSE,DAY] of var SHIFT: roster;

constraint forall(j in DAY)(
             sum(i in NURSE)(roster[i,j] == d) == req_day /\
             sum(i in NURSE)(roster[i,j] == n) == req_night
           );
constraint forall(i in NURSE)(
             regular([roster[i,j] | j in DAY], t, S1, STATE) /\
             sum(j in DAY)(roster[i,j] == n) >= min_night
           );

solve satisfy;
Listing 2.3.6 Example data for nurse rostering using regular constraint (nurse.dzn)
NURSE = Nurse(1..7);
DAY = D(1..10);

req_day = 3;
req_night = 2;
min_night = 2;

Running the command

$ minizinc nurse.mzn nurse.dzn

finds a 10 day schedule for 7 nurses, requiring 3 on each day shift and 2 on each night shift, with a minimum 2 night shifts per nurse. A possible output is

roster =
[|           D(1): D(2): D(3): D(4): D(5): D(6): D(7): D(8): D(9): D(10):
 | Nurse(1):    d,    o,    n,    o,    n,    o,    n,    n,    o,     o
 | Nurse(2):    d,    o,    d,    n,    n,    o,    d,    d,    n,     o
 | Nurse(3):    o,    d,    d,    n,    o,    n,    d,    n,    o,     n
 | Nurse(4):    d,    d,    d,    o,    d,    n,    d,    o,    n,     n
 | Nurse(5):    o,    d,    n,    d,    o,    d,    n,    o,    d,     d
 | Nurse(6):    n,    n,    o,    d,    d,    d,    o,    d,    d,     d
 | Nurse(7):    n,    n,    o,    d,    d,    d,    o,    d,    d,     d
 |];
----------

There is an alternate form of the regular constraint regular_nfa which specifies the regular expression using an NFA (without \(\epsilon\) arcs). This constraint has the form

regular_nfa(array[int] of var $$Val: x,
        array[$$State,$$Val] of set of $$State: d, $$State: q0, set of $$State: F)

It constrains that the sequence of values in array x is accepted by the NFA with transition function d, initial state q0 and accepting states F. There is no need for option types in this case, since an impossible transition can be represented using the empty set.

2.3.2. Defining Predicates

One of the most powerful modelling features of MiniZinc is the ability for the modeller to define their own high-level constraints. This allows them to abstract and modularise their model. It also allows re-use of constraints in different models and allows the development of application specific libraries defining the standard constraints and types.

Listing 2.3.7 Model for job shop scheduling using predicates (jobshop2.mzn)
int: jobs;                                    % no of jobs
set of int: JOB = 1..jobs;
int: tasks;                                   % no of tasks per job
set of int: TASK = 1..tasks;
array [JOB,TASK] of int: d;                   % task durations
int: total = sum(i in JOB, j in TASK)(d[i,j]);% total duration
int: digs = ceil(log(10.0,total));            % digits for output
array [JOB,TASK] of var 0..total: s;          % start times
var 0..total: end;                            % total end time

% nooverlap
predicate no_overlap(var int:s1, int:d1, var int:s2, int:d2) =
    s1 + d1 <= s2 \/ s2 + d2 <= s1;

constraint %% ensure the tasks occur in sequence
    forall(i in JOB) (
        forall(j in 1..tasks-1) 
            (s[i,j] + d[i,j] <= s[i,j+1]) /\
        s[i,tasks] + d[i,tasks] <= end
    );

constraint %% ensure no overlap of tasks
    forall(j in TASK) (
        forall(i,k in JOB where i < k) (
            no_overlap(s[i,j], d[i,j], s[k,j], d[k,j])
        )
    );

solve minimize end;

output ["end = \(end)\n"] ++
       [ show_int(digs,s[i,j]) ++ " " ++ 
         if j == tasks then "\n" else "" endif |
         i in JOB, j in TASK ];

We start with a simple example, revisiting the job shop scheduling problem from the previous section. The model is shown in Listing 2.3.7. The item of interest is the predicate item:

predicate no_overlap(var int:s1, int:d1, var int:s2, int:d2) =
    s1 + d1 <= s2 \/ s2 + d2 <= s1;

This defines a new constraint that enforces that a task with start time s1 and duration d1 does not overlap with a task with start time s2 and duration d2. This can now be used inside the model anywhere any other Boolean expression (involving decision variables) can be used.

As well as predicates the modeller can define new constraints that only involve parameters. These are useful to write fixed tests for a conditional expression. These are defined using the keyword test. For example

test even(int:x) = x mod 2 = 0;

Predicate definitions

Predicates are defined by a statement of the form

predicate <pred-name> ( <arg-def>, ..., <arg-def> ) = <bool-exp>

The <pred-name> must be a valid MiniZinc identifier, and each <arg-def> is a valid MiniZinc type declaration.

One relaxation of argument definitions is that the index types for arrays can be unbounded, written int.

test <pred-name> ( <arg-def>, ..., <arg-def> ) = <bool-exp>

The <bool-exp> of the body must be fixed.

We also introduce a new form of the assert command for use in predicates.

assert ( <bool-exp>, <string-exp>, <exp> )

The type of the assert expression is the same as the type of the last argument. The assert expression checks whether the first argument is false, and if so prints the second argument string. If the first argument is true it returns the third argument.

Note that assert expressions are lazy in the third argument, that is if the first argument is false they will not be evaluated. Hence, they can be used for checking:

predicate lookup(array[int] of var int:x, int: i, var int: y) =
    assert(i in index_set(x), "index out of range in lookup",
           y = x[i]
    );

This code will not evaluate x[i] if i is out of the range of the array x.

2.3.3. Defining Functions

Functions are defined in MiniZinc similarly to predicates, but with a more general return type.

The function below defines the index in a Sudoku matrix of the \(a1^{th}\) row (or column) of the \(a^{th}\) subsquare.

function int: posn(int: a, int: a1) = (a-1) * S + a1;

With this definition we can replace the last constraint in the Sudoku problem shown in Listing 2.2.5 by

constraint forall(a, o in SubSquareRange)(
                  alldifferent([ puzzle [ posn(a,a1), posn(o,o1) ] |
                                         a1, o1 in SubSquareRange ] ) );

Functions are useful for encoding complex expressions that are used frequently in the model. For example, imagine placing the numbers 1 to \(n\) in different positions in an \(n \times n\) grid such that the Manhattan distance between any two numbers \(i\) and \(j\) is greater than the maximum of the two numbers minus 1. The aim is to minimize the total of the Manhattan distances between the pairs. The Manhattan distance function can be expressed as:

function var int: manhattan(var int: x1, var int: y1,
                            var int: x2, var int: y2) =
         abs(x1 - x2) + abs(y1 - y2);

The complete model is shown in Listing 2.3.8.

Listing 2.3.8 Model for a number placement problem illustrating the use of functions (manhattan.mzn).
int: n;
set of int: NUM = 1..n;

array[NUM] of var NUM: x;
array[NUM] of var NUM: y;
array[NUM,NUM] of var 0..2*n-2: dist = 
     array2d(NUM,NUM,[ 
     if i < j then manhattan(x[i],y[i],x[j],y[j]) else 0 endif
                     | i,j in NUM ]);

% manf
function var int: manhattan(var int: x1, var int: y1,
                            var int: x2, var int: y2) =
         abs(x1 - x2) + abs(y1 - y2);

constraint forall(i,j in NUM where i < j)
                 (dist[i,j] >= max(i,j)-1);

var int: obj = sum(i,j in NUM where i < j)(dist[i,j]);
solve minimize obj; 

% simply to display result
include "alldifferent_except_0.mzn";
array[NUM,NUM] of var 0..n: grid;
constraint forall(i in NUM)(grid[x[i],y[i]] = i);
constraint alldifferent_except_0([grid[i,j] | i,j in NUM]);

output ["obj = \(obj);\n"] ++
       [ if fix(grid[i,j]) > 0 then show(grid[i,j]) else "." endif
         ++ if j = n  then "\n" else "" endif 
       | i,j in NUM ]; 

Function definitions

Functions are defined by a statement of the form

function <ret-type> : <func-name> ( <arg-def>, ..., <arg-def> ) = <exp>

The <func-name> must be a valid MiniZinc identifier, and each <arg-def> is a valid MiniZinc type declaration. The <ret-type> is the return type of the function which must be the type of <exp>. Arguments have the same restrictions as in predicate definitions.

Functions in MiniZinc can have any return type, not just fixed return types. Functions are useful for defining and documenting complex expressions that are used multiple times in a model.

2.3.4. Reflection Functions

To help write generic tests and predicates, various reflection functions return information about array index sets, var set domains and decision variable ranges. Those for index sets are index_set(<1-D array>), index_set_1of2(<2-D array>), index_set_2of2(<2-D array>), and so on for higher dimensional arrays.

A better model of the job shop conjoins all the non-overlap constraints for a single machine into a single disjunctive constraint. An advantage of this approach is that while we may initially model this simply as a conjunction of non-overlap constraints, if the underlying solver has a better approach to solving disjunctive constraints we can use that instead, with minimal changes to our model. The model is shown in Listing 2.3.9.

Listing 2.3.9 Model for job shop scheduling using disjunctive predicate (jobshop3.mzn).
include "disjunctive.mzn";

int: jobs;                                    % no of jobs
set of int: JOB = 1..jobs;
int: tasks;                                   % no of tasks per job
set of int: TASK = 1..tasks;
array [JOB,TASK] of int: d;                   % task durations
int: total = sum(i in JOB, j in TASK)(d[i,j]);% total duration
int: digs = ceil(log(10.0,total));            % digits for output
array [JOB,TASK] of var 0..total: s;          % start times
var 0..total: end;                            % total end time

constraint %% ensure the tasks occur in sequence
    forall(i in JOB) (
        forall(j in 1..tasks-1) 
            (s[i,j] + d[i,j] <= s[i,j+1]) /\
        s[i,tasks] + d[i,tasks] <= end
    );

constraint %% ensure no overlap of tasks
    forall(j in TASK) (
        disjunctive([s[i,j] | i in JOB], [d[i,j] | i in JOB])
    );

solve minimize end;

output ["end = \(end)\n"] ++
       [ show_int(digs,s[i,j]) ++ " " ++ 
         if j == tasks then "\n" else "" endif |
         i in JOB, j in TASK ];

The disjunctive constraint takes an array of start times for each task and an array of their durations and makes sure that only one task is active at any one time. We define the disjunctive constraint as a predicate with signature

predicate disjunctive(array[int] of var int:s, array[int] of int:d);

We can use the disjunctive constraint to define the non-overlap of tasks as shown in Listing 2.3.9. We assume a definition for the disjunctive predicate is given by the file disjunctive.mzn which is included in the model. If the underlying system supports disjunctive directly, it will include a file disjunctive.mzn in its globals directory (with contents just the signature definition above). If the system we are using does not support disjunctive directly we can give our own definition by creating the file disjunctive.mzn. The simplest implementation simply makes use of the no_overlap predicate defined above. A better implementation is to make use of a global cumulative constraint assuming it is supported by the underlying solver. Listing 2.3.10 shows an implementation of disjunctive. Note how we use the index_set reflection function to (a) check that the arguments to disjunctive make sense, and (b) construct the array of resource utilisations of the appropriate size for cumulative. Note also that we use a ternary version of assert here.

Listing 2.3.10 Defining a disjunctive predicate using cumulative (disjunctive.mzn).
include "cumulative.mzn";

predicate disjunctive(array[int] of var int:s, array[int] of int:d) =
          assert(index_set(s) == index_set(d), "disjunctive: " ++
          "first and second arguments must have the same index set",
            cumulative(s, d, [ 1 | i in index_set(s) ], 1)
          );

2.3.5. Local Variables

It is often useful to introduce local variables in a predicate, function or test. The let expression allows you to do so. It can be used to introduce both decision variables and parameters, but parameters must be initialised. For example:

var s..e: x;
let {int: l = s div 2; int: u = e div 2; var l .. u: y;} in x = 2*y

introduces parameters l and u and variable y. While most useful in predicate, function and test definitions, let expressions can also be used in other expressions, for example for eliminating common subexpressions:

constraint let { var int: s = x1 + x2 + x3 + x4 } in
           l <= s /\ s <= u;

Local variables can be used anywhere and can be quite useful for simplifying complex expressions. Listing 2.3.11 gives a revised version of the wedding model, using local variables to define the objective function, rather than adding lots of variables to the model explicitly.

Listing 2.3.11 Using local variables to define a complex objective function (wedding2.mzn).
enum Guests = { bride, groom, bestman, bridesmaid, bob, carol, 
  ted, alice, ron, rona, ed, clara}; 
set of int: Seats = 1..12;
set of int: Hatreds = 1..5;
array[Hatreds] of Guests: h1 = [groom, carol, ed, bride, ted];
array[Hatreds] of Guests: h2 = [clara, bestman, ted, alice, ron];
set of Guests: Males = {groom, bestman, bob, ted, ron,ed};
set of Guests: Females = {bride,bridesmaid,carol,alice,rona,clara}; 

array[Guests] of var Seats: pos; % seat of guest

include "alldifferent.mzn";
constraint alldifferent(pos);

constraint forall(g in Males)( pos[g] mod 2 == 1 );
constraint forall(g in Females)( pos[g] mod 2 == 0 );

constraint not (pos[ed] in {1,6,7,12});
constraint abs(pos[bride] - pos[groom]) <= 1 /\ 
           (pos[bride] <= 6 <-> pos[groom] <= 6);

solve maximize sum(h in Hatreds)(
          let {  var Seats: p1 = pos[h1[h]];
                 var Seats: p2 = pos[h2[h]];
                 var 0..1: same = bool2int(p1 <= 6 <-> p2 <= 6); } in   
          same * abs(p1 - p2) + (1-same) * (abs(13 - p1 - p2) + 1));

output [ show(g)++" " | s in Seats,g in Guests where fix(pos[g]) == s]
       ++ ["\n"]; 

Using let expressions, it is possible to define a function whose result is not well-defined. For example, we could write the following:

function var int: x_or_x_plus_1(var int: x) = let {
  var 0..1: y;
} in x+y; % result is not well-defined!

The result, x+y, is indeed not functionally defined by the argument of the function, x. The MiniZinc compiler does not detect this, and the behaviour of the resulting model is undefined. In particular, calling this function twice with the same argument may or may not return the same result. It is therefore important to make sure that any function you define is indeed a function! If you need non-deterministic behaviour, use a predicate:

predicate x_or_x_plus_1(var int: x, var int: z) = let {
  var 0..1: y;
} in z=x+y;

2.3.6. Context

One limitation is that predicates and functions containing decision variables that are not initialised in the declaration cannot be used inside a negative context. The following is illegal:

predicate even(var int:x) =
          let { var int: y } in x = 2 * y;

constraint not even(z);

The reason for this is that solvers only solve existentially constrained problems, and if we introduce a local variable in a negative context, then the variable is universally quantified and hence out of scope of the underlying solvers. For example the \(\neg \mathit{even}(z)\) is equivalent to \(\neg \exists y. z = 2y\) which is equivalent to \(\forall y. z \neq 2y\).

If local variables are given values, then they can be used in negative contexts. The following is legal

predicate even(var int:x) =
          let { var int: y = x div 2; } in x = 2 * y;

constraint not even(z);

Note that the meaning of even is correct, since if x is even then \(x = 2 * (x ~\mbox{div}~ 2)\). Note that for this definition \(\neg \mathit{even}(z)\) is equivalent to \(\neg \exists y. y = z ~\mbox{div}~ 2 \wedge z = 2y\) which is equivalent to \(\exists y. y = z ~\mbox{div}~ 2 \wedge \neg z \neq 2y\), because \(y\) is functionally defined by \(z\).

Every expression in MiniZinc appears in one of the four contexts: root, positive, negative, or mixed. The context of a non-Boolean expression is simply the context of its nearest enclosing Boolean expression. The one exception is that the objective expression appears in a root context (since it has no enclosing Boolean expression).

For the purposes of defining contexts we assume implication expressions e1 -> e2 are rewritten equivalently as not e1 \/ e2, and similarly e1 <- e2 is rewritten as e1 \/ not e2.

The context for a Boolean expression is given by:

root

root context is the context for any expression e appearing as the argument of constraint or as an assignment item, or appearing as a sub expression e1 or e2 in an expression e1 /\ e2 occurring in a root context.

Root context Boolean expressions must hold in any model of the problem.

positive

positive context is the context for any expression appearing as a sub expression e1 or e2 in an expression e1 \/ e2 occurring in a root or positive context, appearing as a sub expression e1 or e2 in an expression e1 /\ e2 occurring in a positive context, or appearing as a sub expression e in an expression not e appearing in a negative context.

Positive context Boolean expressions need not hold in a model, but making them hold will only increase the possibility that the enclosing constraint holds. A positive context expression has an even number of negations in the path from the enclosing root context to the expression.

negative

negative context is the context for any expression appearing as a sub expression e1 or e2 in an expression e1 \/ e2 or e1 /\ e2 occurring in a negative context, or appearing as a sub expression e in an expression not e appearing in a positive context.

Negative context Boolean expressions need not hold in a model, but making them false will increase the possibility that the enclosing constraint holds. A negative context expression has an odd number of negations in the path from the enclosing root context to the expression.

mixed

mixed context is the context for any Boolean expression appearing as a subexpression e1 or e2 in e1 <-> e2, e1 = e2, or bool2int(e).

Mixed context expression are effectively both positive and negative. This can be seen from the fact that e1 <-> e2 is equivalent to (e1 /\ e2) \/ (not e1 /\ not e2) and x = bool2int(e) is equivalent to (e /\ x=1) \/ (not e /\ x=0).

Consider the code fragment

constraint x > 0 /\ (i <= 4 -> x + bool2int(x > i) = 5);

then x > 0 is in the root context, i <= 4} is in a negative context, x + bool2int(x > i) = 5 is in a positive context, and x > i is in a mixed context.

2.3.7. Local Constraints and Partiality

Let expressions can also be used to include local constraints, usually to constrain the behaviour of local variables. For example, consider defining an integer square root function making use of only multiplication:

function var int: mysqrt(var int:x) =
         let { var 0..infinity: y;
               constraint x = y * y; } in y;

The local constraints ensure y takes the correct value; which is then returned by the function.

Local constraints can be used in any let expression, though the most common usage is in defining functions. A function with local constraints is often partial, which means that it is not defined for all possible inputs. For example, the mysqrt function above constrains its argument x to take a value that is in fact the square of an integer. The MiniZinc compiler handles these cases according to the relational semantics, which means that the result of applying a partial function may become false in its enclosing Boolean context. For example, consider the following model:

var 1..9: x;
var 0..9: y;
constraint (x=3 /\ y=0) \/ y = mysqrt(x);

Clearly, the intention of the modeller is that x=3, y=0 should be a solution. This requires the compiler to take care not to “lift” the constraint x=y*y out of the context of the function, because that would prevent it from finding any solution with x=3. You can verify that the set of solutions contains x=3, y=0 as well as the expected x=1, y=1, x=4, y=2 and x=9, y=3.

If you define a total function using local constraints, you can give the compiler a hint that allows it to produce more efficient code. For example, you could write the square function (not square root, note the subtle difference) as follows:

function var int: mysqr(var int:x) ::promise_total =
         let { var 0..infinity: y;
               constraint y = x * x; } in y;

This function is indeed defined for any input value x. The ::promise_total annotation tells the compiler that it can safely lift all local constraints out of the context of the function call.

Let expressions

Local variables can be introduced in any expression with a let expression of the form:

let { <dec>; ... <dec> ; } in <exp>

The declarations <dec> can be declarations of decision variables and parameters (which must be initialised) or constraint items. No declaration can make use of a newly declared variable before it is introduced.

Note that local variables and constraints cannot occur in tests. Local variables cannot occur in predicates or functions that appear in a negative or mixed context, unless the variable is defined by an expression.

2.3.8. Domain Reflection Functions

Other important reflection functions are those that allow us to access the domains of variables. The expression lb(x) returns a value that is lower than or equal to any value that x may take in a solution of the problem. Usually it will just be the declared lower bound of x. If x is declared as a non-finite type, e.g. simply var int then it is an error. Similarly the expression dom(x) returns a (non-strict) superset of the possible values of x in any solution of the problem. Again it is usually the declared values, and again if it is not declared as finite then there is an error.

Listing 2.3.12 Using reflection predicates (reflection.mzn).
var -10..10: x;
constraint x in 0..4;
int: y = lb(x);
set of int: D = dom(x);
solve satisfy;
output ["y = ", show(y), "\nD = ", show(D), "\n"];

For example, the model show in Listing 2.3.12 may output

y = -10
D = -10..10
----------

or

y = 0
D = {0, 1, 2, 3, 4}
----------

or any answer with \(-10 \leq y \leq 0\) and \(\{0, \ldots, 4\} \subseteq D \subseteq \{-10, \ldots, 10\}\).

Variable domain reflection expressions should be used in a manner where they are correct for any safe approximations, but note this is not checked! For example the additional code

var -10..10: z;
constraint z <= y;

is not a safe usage of the domain information. Since using the tighter (correct) approximation leads to more solutions than the weaker initial approximation.

Domain reflection

There are reflection functions to interrogate the possible values of expressions containing variables:

  • dom(<exp>) returns a safe approximation to the possible values of the expression.

  • lb(<exp>) returns a safe approximation to the lower bound value of the expression.

  • ub(<exp>) returns a safe approximation to the upper bound value of the expression.

The expressions for lb and ub can only be of types int, bool, float or set of int. For dom the type cannot be float. If one of the variables appearing in <exp> has a non-finite declared type (e.g. var int or var float) then an error can occur.

There are also versions that work directly on arrays of expressions (with similar restrictions):

  • dom_array(<array-exp>): returns a safe approximation to the union of all possible values of the expressions appearing in the array.

  • lb_array(<array-exp>) returns a safe approximation to the lower bound of all expressions appearing in the array.

  • ub_array(<array-exp>) returns a safe approximation to the upper bound of all expressions appearing in the array.

The combinations of predicates, local variables and domain reflection allows the definition of complex global constraints by decomposition. We can define the time based decomposition of the cumulative constraint using the code shown in Listing 2.3.13.

Listing 2.3.13 Defining a cumulative predicate by decomposition (cumulative.mzn).
%--------------------------------------------------------------------%
% Requires that a set of tasks given by start times 's', 
% durations 'd', and resource requirements 'r', 
% never require more than a global 
% resource bound 'b' at any one time.
% Assumptions:
% - forall i, d[i] >= 0 and r[i] >= 0
%--------------------------------------------------------------------%
predicate cumulative(array[int] of var int: s,
                     array[int] of var int: d,
                     array[int] of var int: r, var int: b) =
   assert(index_set(s) == index_set(d) /\ 
          index_set(s) == index_set(r),
     "cumulative: the array arguments must have identical index sets",
   assert(lb_array(d) >= 0 /\ lb_array(r) >= 0,
     "cumulative: durations and resource usages must be non-negative",
           let { 
               set of int: times =
                 lb_array(s) ..
                 max([ ub(s[i]) + ub(d[i]) | i in index_set(s) ]) 
               } 
           in
              forall( t in times ) (
                 b >= sum( i in index_set(s) ) (
                    bool2int( s[i] <= t /\ t < s[i] + d[i] ) * r[i]
                 )
              )
       )
   );

The decomposition uses lb and ub to determine the set of times times over which tasks could range. It then asserts for each time t in times that the sum of resources for the active tasks at time t is less than the bound b.

2.3.9. Scope

It is worth briefly mentioning the scope of declarations in MiniZinc. MiniZinc has a single namespace, so all variables appearing in declarations are visible in every expression in the model. MiniZinc introduces locally scoped variables in a number of ways:

  • as iterator variables in comprehension expressions

  • using let expressions

  • as predicate and function arguments

Any local scoped variable overshadows the outer scoped variables of the same name.

Listing 2.3.14 A model for illustrating scopes of variables (scope.mzn).
int: x = 3;
int: y = 4;
predicate smallx(var int:y) = -x <= y /\ y <= x;
predicate p(int: u, var bool: y) = 
      exists(x in 1..u)(y \/ smallx(x));
constraint p(x,false);
solve satisfy;

For example, in the model shown in Listing 2.3.14 the x in -x <= y is the global x, the x in smallx(x) is the iterator x in 1..u, while the y in the disjunction is the second argument of the predicate.