2.4. Option Types

Option types are a powerful abstraction that allows for concise modelling. An option type decision variable represents a decision that has another possibility \(\top\), represented in MiniZinc as <> indicating the variable is absent. Option type decisions are useful for modelling problems where a decision is not meaningful unless other decisions are made first.

2.4.1. Declaring and Using Option Types

Option type Variables

An option type variable is declared as:

var opt <type> : <var-name>:

where <type> is one of int, float or bool or a fixed range expression. Option type variables can be parameters.

An option type variable can take the additional value <> indicating absent.

An option type variable behaves like a normal, non-optional variable, as long as it is not absent, i.e., as long as it is not equal to <>. An absent option type variable should behave as if the object it represents does not exist. This means different things for different functions and relations.

For example, when adding <> to another variable x, the result is just x. Similarly, all_different([x,y,z]) should behave exactly like all_different([x,y]) in case z=<>, i.e., z is absent.

Option type variables can be used like their non-optional versions with most operators on Booleans, integers and floats. Many functions and predicates in the MiniZinc library are also defined for option type variables. Here are a few examples of how different functions and operators treat option types:

% Expression:               Equivalent to:          Simplified:
<> + a                  =   0 + a                =  a
a * <>                  =   a * 1                =  a
sum([x1,<>,x2])         =   sum([x1,x2])
sum([<>,<>])            =   sum([])              = 0
product([x1,x2,<>])     =   product([x1,x2])
product([<>,<>,<>])     =   product([])          = 1
exists([b1,<>])         =   exists([b1])         = b1
exists([<>,<>])         =   exists([])           = false
forall([<>,b1,b2])      =   forall([b1,b2])
forall([<>,<>])         =   forall([])           = true
all_different([x,<>,y]) =   all_different([x,y])

Comparison operators return true if any of their arguments is absent. For instance, 3 <= <> is true, as is <> <= 3. However, note that equality between option type expressions is only true if both expressions have the same optionality: <> = <> is true, but 3 = <> is false. If you need the “weaker” version of equality, MiniZinc provides the ~= operator: 3 ~= <> is true. The ~!= operator is the weak version of disequality, it is true is either side is absent or they are not equal. Note that a ~!= b is different from not (a ~= b), because <> ~!= <> is true, while not (<> ~= <>) is false.

Similarly, it can sometimes be useful to have “weak” versions of the arithmetic operators that return <> if any of their arguments is absent. MiniZinc provides the ~+, ~-, ~*, ~/ and ~div operators for this purpose (e.g., 3 + <> =3, but 3 ~+ <> = <>).

Operations on option type variables

Two builtin functions and a binary operator are provided for option type variables: absent(v) returns true iff option type variable v takes the value <>, occurs(v) returns true iff option type variable v does not take the value <>, and x default y returns x if x occurs, and y otherwise.

In addition, the function deopt(v) returns the normal value of v or fails if it takes the value <>. This function should not be used in normal models, but is required to implement predicates over option type variables.

2.4.2. Option Types in Scheduling Problems

A common use of option types is for optional tasks in scheduling. In the flexible job shop scheduling problem we have n tasks to perform on k machines, and the time to complete each task on each machine may be different. The aim is to minimize the completion time of all tasks. A model using option types to encode the problem is given in Listing 2.4.1. We model the problem using \(n \times k\) optional tasks representing the possibility of each task run on each machine. We require that start time of the task and its duration spans the optional tasks that make it up, and require only one actually runs using the alternative global constraint. We require that at most one task runs on any machine using the disjunctive global constraint extended to optional tasks. Finally we constrain that at most k tasks run at any time, a redundant constraint that holds on the actual (not optional) tasks.

Listing 2.4.1 Model for flexible job shop scheduling using option types (flexible-js.mzn).
include "globals.mzn";

int: horizon;                  % time horizon
set of int: Time = 0..horizon;
enum Task;
enum Machine; 

array[Task,Machine] of int: d; % duration on each machine
int: maxd = max([ d[t,m] | t in Task, m in Machine ]);
int: mind = min([ d[t,m] | t in Task, m in Machine ]);

array[Task] of var Time: S;             % start time
array[Task] of var mind..maxd: D;       % duration
array[Task,Machine] of var opt Time: O; % optional task start

constraint forall(t in Task)(alternative(S[t],D[t],
                 [O[t,m]|m in Machine],[d[t,m]|m in Machine]));
constraint forall(m in Machine)
                 (disjunctive([O[t,m]|t in Task],[d[t,m]|t in Task]));
constraint cumulative(S,D,[1|i in Task],card(Machine));

solve minimize max(t in Task)(S[t] + D[t]);

2.4.3. Hidden Option Types

Option type variable arise implicitly when list comprehensions are constructed with iteration over variable sets, or where the expressions in where clauses are not fixed.

For example the model fragment

var set of 1..n: x;
constraint sum(i in x)(i) <= limit;

is syntactic sugar for

var set of 1..n: x;
constraint sum(i in 1..n)(if i in x then i else <> endif) <= limit;

The sum builtin function actually operates on a list of type-inst var opt int. Since the <> acts as the identity 0 for + this gives the expected results.

Similarly the model fragment

array[1..n] of var int: x;
constraint forall(i in 1..n where x[i] >= 0)(x[i] <= limit);

is syntactic sugar for

array[1..n] of var int: x;
constraint forall(i in 1..n)(if x[i] >= 0 then x[i] <= limit else <> endif);

Again the forall function actually operates on a list of type-inst var opt bool. Since <> acts as identity true for /\ this gives the expected results.

The hidden uses can lead to unexpected behaviour though so care is warranted. Consider

var set of 1..9: x;
constraint card(x) <= 4;
constraint length([ i | i in x]) > 5;
solve satisfy;

which would appear to be unsatisfiable. It returns x = {1,2,3,4} as example answer. This is correct since the second constraint is equivalent to

constraint length([ if i in x then i else <> endif | i in 1..9 ]) > 5;

and the length of the list of optional integers is always 9 so the constraint always holds!

One can avoid hidden option types by not constructing iteration over variables sets or using unfixed where clauses. For example the above two examples could be rewritten without option types as

var set of 1..n: x;
constraint sum(i in 1..n)(bool2int(i in x)*i) <= limit;

and

array[1..n] of var int: x;
constraint forall(i in 1..n)(x[i] >= 0 -> x[i] <= limit);

2.4.4. Option Type Parameters

Option type variables of fixed parameter type can be used to define optional model parameters. For example, a variable defined like this:

opt bool: enable_feature;

could be used to enable or disable a certain optional feature of a model. In contrast to other parameter variables, these optional parameters do not have to be assigned a value (e.g., the data file may omit an assignment to enable_feature). In that case, the variable is automatically assigned the value <>. In the model, such an optional parameter could be used like this:

bool: enable_feature_enabled = enable_feature default false;

constraint if enable_feature_enabled then ... endif;