Savile Row Manual

Types and domains play a similar role; they prescribe a set of values that an expression or variable can take. Types denote non-empty sets that contain all elements that have a similar structure, whereas domains denote possibly empty sets drawn from a single type. In this manner, each domain is associated with an underlying type. For example integer is the type underlying the domain comprising integers between 1 and 10. The type contains all integers, and the domain is a finite subset.

Essence Prime is a strongly typed language; every expression has a type, and the types of all expressions can be inferred and checked for correctness. Furthermore, Essence Prime is a finite-domain language; every decision variable is associated with a finite domain of values.

The atomic types of Essence Prime are int (integer) and bool (boolean). There is also a compound type, matrix, that is constructed of atomic types.

There are three different types of domains in Essence Prime: boolean, integer and matrix domains. Boolean and integer domains are both atomic domains; matrix domains are built from atomic domains.

Boolean Domains

bool is the Boolean domain consisting of false and true.

Integer Domains

An integer domain represents a finite subset of the integers, and is specified as a sequence of ranges or individual elements, for example int(1..3,5,7,9..20). Each range includes the endpoints, so the meaning of a range a..b is the set $\{i\in\mathbb{Z}|a\leq i\leq b\}$. A range a..b would normally be in order, i.e. a<=b but this is not strictly required. Out-of-order ranges correspond to the empty set of integers.

The meaning of an integer domain is the union of the ranges and individual elements in the domain. For example, int(10, 1..5, 4..9) is equivalent to int(1..10).

Finally, the elements and endpoints of ranges may be expressions of type int. The only restriction is that they may not contain any CSP decision variables. The integer expression language is described in the following sections.

Matrix Domains

A matrix is defined by the keyword matrix, followed by its dimensions and the base domain. The dimensions are a list, in square brackets, of domains. For instance,

Matrix1 : matrix indexed by [int(1..10),int(1..10)] of int(1..5)

is the domain of a two-dimensional square matrix, indexed by $1..10$ in both dimensions, where each element of the matrix has the domain int(1..5). Elements of this matrix would be accessed by Matrix1[A,B] where A and B are integer expressions.

Matrices may be indexed by any integer domain or the boolean domain. For example,

Matrix2 : matrix indexed by [int(-2..5),int(-10..10,15,17)] of int(1..5)

is a valid matrix domain.

Essence Prime contains a small expression language for boolean and integer domains. This language consists of three binary infix operators intersect, union and -. All three are left-associative and the precedences are given in Appendix B. The language also allows bracketed subexpressions with ( and ).

For example, the first and second lines below are exactly equivalent.

letting dom be domain int(1..5, 3..8)
letting dom be domain int(1..5) union int(3..8)

Each of the three types (integer, boolean and matrix) has a corresponding literal syntax in Essence Prime. Any value of any type may be written as a literal. Sets and real numbers are not (as yet) part of the language. Integer and boolean literals are straightforward:

1 2 3 -5
true false

There are two forms of matrix literals. The simpler form is a comma-separated list of expressions surrounded by square brackets. For example, the following is a matrix literal containing four integer literals.

[ 1, 3, 2, 4 ]

Matrix literals may contain any valid expression in Essence Prime. For example a matrix literal is allowed to contain other matrix literals to build up a matrix with two or more dimensions. The types of the expressions contained in the matrix literal must all be the same.

The second form of matrix literal has an explicit index domain that specifies how the literal is indexed. This is specified after the comma-separated list of contents using a ; as follows.

[ 1, 3, 2, 4 ; int(4..6,8) ]

The index domain must be a domain of type bool or int, and must contain the same number of values as the number of items in the matrix literal. When no index domain is specified, a matrix of size n is indexed by int(1..n).

Finally a multi-dimensional matrix value can be expressed by nesting matrix literals. Suppose we have the following domain:

One value contained in this domain is the following:

[ [ 1,2,3 ; int(1,2,4) ],
  [ 1,3,2 ; int(1,2,4) ],
  [ 3,2,1 ; int(1,2,4) ]
  ; int(-2..0) ]

Variables are identified by a string. Variable names must start with a letter a-z or A-Z, and after the first letter may contain any of the following characters: a-z A-Z 0-9 _. A variable may be of type integer, boolean or matrix.

Scoping of variables depends on how they are declared and is dealt with in the relevant sections below. As well as a type, variables have a category. The category is decision, quantifier or parameter. Decision variables are CSP variables, and the other categories are described below.

Expressions containing decision variables are referred to as decision expressions, and expressions containing no decision variables as non-decision expressions. This distinction is important because expressions in certain contexts are not allowed to contain decision variables.

Expressions can be of any of the three basic types (integer, boolean or matrix). Integer expressions range over an integer domain, for instance x + 3 (where x is an integer variable) is an integer expression ranging from $lb(x)+3$ to $ub(x)+3$. Boolean expressions range over the Boolean domain, for instance the integer comparison x = 3 can either be true or false.

Boolean expressions or literals are automatically converted to integers when used in a context that expects an integer. As is conventional false is converted to 0 and true is converted to 1. For example, the following are valid Essence Prime boolean expressions.

1+2-3+true-(x<y)=5
false < true

Integer expressions are not automatically converted to boolean. Matrix expressions cannot be converted to any other type (or vice versa).

Suppose we have a three-dimensional matrix M with the following domain:

matrix indexed by [int(1..3), int(1..3), bool] of int(1..5)

M would be indexed as follows: M[x,y,z], where x and y may be integer or boolean expressions and z must be boolean. Because the matrix has the base domain int(1..5), M[x,y,z] will be an integer expression. Matrix indexing is a partial function: when one of the indices is out of bounds then the expression is undefined. Essence Prime has the relational semantics, in brief this means that the boolean expression containing the undefined expression is false. So for example, M[1,1,false]=M[2,4,true] is always false because the 4 is out of bounds. The relational semantics are more fully described in Section 3 below.

Parts of matrices can be extracted by slicing. Suppose we have the following two-dimensional matrix named N:

[ [ 1,2,3 ; int(1,2,4) ],
  [ 1,3,2 ; int(1,2,4) ],
  [ 3,2,1 ; int(1,2,4) ]
  ; int(-2..0) ]

We could obtain the first row by writing N[-2,..], which is equal to [ 1,2,3 ; int(1..3)]. Similarly the first column can be obtained by N[..,1] which is [ 1,1,3 ; int(1..3)]. In general, the indices in a matrix slice may be .. or an integer or boolean expression that does not contain any decision variables. Matrix slices are always indexed contiguously from 1 regardless of the original matrix domain.

When a matrix slice has an integer or boolean index that is out of bounds, then the expression is undefined and this is handled as described in Section 3.

Essence Prime has a range of binary infix and unary operators and functions for building up integer and boolean expressions, for example:

• •

  Integer operators: + - * ** / % | min max

• •

  Boolean operators: \/ /\ -> <-> !

• •

  Quantified sum: sum

• •

  Logical quantifiers: forAll exists

• •

  Numerical comparison operators: = != > < >= <=

• •

  Matrix comparison operators: <=lex <lex >=lex >lex

• •

  Set operator: in

• •

  Global constraints: allDiff gcc cumulative

• •

  Table constraint: table

These are described in the following subsections.

Essence Prime has the following binary integer operators: + - * / % **. +, - and * are the standard integer operators.

The operators / and % are integer division and modulo functions. a/b is defined as $\lfloor a/b\rfloor$ (i.e. it always rounds down). This does not match some programming languages, for example C99 which rounds towards 0.

The modulo operator a%b is defined as $a-b\lfloor a/b\rfloor$ to be complementary to /.

3/2 = 1
(-3)/2 = -2
3/(-2) = -2
(-3)/(-2) = 1

3 % 2 = 1
(-3) % 2 = 1
3 % (-2) = -1
(-3) % (-2) = -1

** is the power function: x**y is defined as $x^{y}$. There are two unary functions: absolute value (where |x| is the absolute value of x), and negation (unary -).

Essence Prime has the /\ (and) and \/ (or) operators defined on boolean expressions. There are also -> (implies), <-> (if and only if), and ! (negation). These operators all take boolean expressions and produce a new boolean expression. They can be nested arbitrarily.

The comma , in Essence Prime is also a binary boolean operator, with the same meaning as /\. However it has a different precedence, and is used quite differently. /\ is normally used within a constraint, and , is used to separate constraints (or separate groups of constraints constructed using a forAll). Consider the following example.

forAll i : int(1..n) . x[i]=y[i] /\ x[i]!=y[i+1],
exists i : int(1..n) . x[i]=1 /\ y[i]!=y[i+1]

Here we have two quantifiers, both with an /\ inside. The comma is used to separate the forAll and the exists. The comma has the lowest precedence of all binary operators.

Essence Prime has named functions min(X,Y) and max(X,Y) that both take two integer expressions X and Y. min and max can also be applied to one-dimensional matrices to obtain the minimum or maximum of all elements in the matrix (see Section 2.1.22). factorial(x) returns the factorial of values from 0 to 20 where the result fits in a 64-bit signed integer. It is undefined for other values of x and the expression x is not allowed to contain decision variables. popcount(x) returns the bit count of the 64-bit two’s complement representation of x, and x may not contain decision variables.

The function toInt(x) takes a boolean expression x and converts to an integer 0 or 1. This function is included only for compatibility with Essence: it is not needed in Essence Prime because booleans are automatically cast to integers.

Essence Prime provides the following integer comparisons with their obvious meanings: = != > < >= <=. These operators each take two integer expressions and produce a boolean expression.

Essence Prime provides a way of comparing one-dimensional matrices. These operators compare two matrices using the dictionary order (lexicographical order, or lex for short).

There are four operators. A <lex B ensures that A comes before B in lex order, and A <=lex B which ensures that A <lex B or A=B. >=lex and >lex are identical but with the arguments reversed. For all four operators, A and B may have different lengths and may be indexed differently, but they must be one-dimensional. Multi-dimensional matrices may be flattened to one dimension using the flatten function described in Section 2.1.22 below.

The operator in states that an integer expression takes a value in a set expression. The set espression may not contain decision variables. The set may be a domain expression (Section 2.1.2) or the toSet function that converts a one-dimensional matrix to a set, as in the examples below.

x+y in (int(1,3,5) intersect int(3..10))
x+y in toSet([ i | i : int(1..n), i%2=0])

The sum operator corresponds to the mathematical $\sum$ and has the following syntax:

sum i : D . E

where i is a quantifier variable, D is a domain, and E is the expression contained within the sum. More than one quantifier variable may be created by writing a comma-separated list i,j,k.

For example, if we want to take the sum of all numbers in the range 1 to 10 we write

sum i : int(1..n) . i

which corresponds to $\sum\nolimits_{i=1}^{n}i$. n cannot be a decision variable.

Quantified sum has several similarities to the forAll and exists quantifiers (described below in Section 2.1.16): it introduces new local variables (named quantifier variables) that can be used within E, and the quantifier variables all have the same domain D. However sum has one important difference: a sum is an integer expression.

A quantified sum may be nested inside any other integer operator, including another quantified sum:

sum i,j : int(1..10) .
    sum k : int(i..10) .
        x[i,j] * k

Universal and existential quantification are powerful means to write down a series of constraints in a compact way. Quantifications have the same syntax as sum, but with forAll and exists as keywords:

forAll  i : D . E
exists  i : D . E

For instance, the universal quantification

forAll i : int(1..3) . x[i] = i

corresponds to the conjunction:

x[1] = 1 /\ x[2] = 2 /\ x[3] = 3

An example of existential quantification is

exists i : int(1..3) . x[i] = i

and it corresponds to the following disjunction:

x[1] = 1 \/ x[2] = 2 \/ x[3] = 3

Quantifications can range over several quantified variables and can be arbitrarily nested, as demonstrated with the sum quantifier.

In the running Sudoku example, forAll quantification is used to build the set of constraints. The expression:

forAll row : int(1..9) .
    forAll col1 : int(1..9) .
        forAll col2: int(col1+1..9) . M[row, col1]!=M[row, col2]

is a typical use of universal quantification.

All three quantifiers are defined on matrix domains as well as integer and boolean domains. For example, to quantify over all permutations of size n:

forAll perm : matrix indexed by [int(1..n)] of int(1..n) .
    allDiff(perm) -> exp

The variable perm represents a matrix drawn from the matrix domain, and the allDiff constraint evaluates to true when perm is a permutation of $1\ldots n$. Hence the expression exp is quantified for all permutations of $1\ldots n$.

If n is a constant, the example above could be written as a set of n nested forAll quantifiers. However if n is a parameter of the problem class, it is very difficult to write the example above using other (non-matrix) quantifiers.

Essence Prime provides a small set of global constraints such as allDiff (which is satisfied when a vector of variables each take different values). Global constraints are all boolean expressions in Essence Prime. Typically it is worth using these in models because the solver often performs better with a global constraint compared to a set of simpler constraints.

For example, the following two lines are semantically equivalent (assuming x is a matrix indexed by 1..n).

forAll i,j : int(1..n) . i<j -> x[i]!=x[j]
allDiff(x)

Both lines will ensure that the variables in x take different values. However the allDiff will perform better in most situations.²²2In the current version of Savile Row, with default settings, the x[i]!=x[j] constraints would be aggregated to create allDiff(x) therefore there is no difference in performance between these two statements. There would be a difference in performance when aggregation is switched off (for example by using the -O1 flag). Table 1 summarises the global constraints available in Essence Prime.

To give another example, the cumulative constraint for scheduling applies a bound on the amount of a resource that may be used at each time step in a schedule. It has arguments X, Dur, Res, and Bound (see Table 1) representing the start time of each task, the duration of each task, the resource required for each task while it is running, and the upper limit on the resource usage. Suppose there are three tasks, each task takes 3 time units to execute, each task consumes 2 units of resource when it is running, and the resource limit is 5:

Res=[2,2,2]
Bound=5
Dur=[3,3,3]

If all three tasks are running at any time step, they would exceed the resource bound. X=[0, 1, 2] is not a solution, but X=[0, 1, 3] is (the first task finishes before the third task starts).

Now we have the allDiff global constraint, the Sudoku example can be improved and simplified as shown in Figure 3.

Global constraints are boolean expressions like any other, and are allowed to be used in any context that accepts a boolean expression.

In a table constraint the satisfying tuples of the constraint are specified using a matrix. This allows a table constraint to theoretically implement any relation, although practically it is limited to relations where the set of satisfying tuples is small enough to store in memory and efficiently search.

The first argument specifies the variables in the scope of the constraint, and the second argument is a two-dimensional matrix of satisfying tuples. For example, the constraint a+b=c on boolean variables could be written as a table as follows.

table( [a,b,c], [[0,0,0], [0,1,1], [1,0,1]] )

The first argument of table is a one-dimensional matrix expression. It may contain both decision variables and constants. The second argument is a two-dimensional matrix expression containing no decision variables. The second argument can be stated as a matrix literal, or an identifier, or by slicing a higher-dimension matrix, or by constructing a matrix using matrix comprehensions (see Section 2.1.20).

If the same matrix of tuples is used for many table constraints, a letting statement can be used to state the matrix once and use it many times. Lettings are described in Section 2.2.2 below.

We have seen that matrices may be written explicitly as a matrix literal (Section 2.1.3), and that existing matrices can be indexed and sliced (Section 2.1.7). Matrices can also be constructed using matrix comprehensions. This provides a very flexible way to create matrices of variables or values. A single matrix comprehension creates a one-dimensional matrix, however they can be nested to create multi-dimensional matrices. There are two syntactic forms of matrix comprehension:

[ exp | i : domain1, j : domain2, cond1, cond2 ]
[ exp | i : domain1, j : domain2, cond1, cond2 ; indexdomain ]

where exp is any integer, boolean or matrix expression. This is followed by any number of comprehension variables, each with a domain. After the comprehension variables we have an optional list of conditions: these are boolean expressions that constrain the values of the comprehension variables. Finally there is an optional index domain. This provides an index domain to the constructed matrix.

To expand the comprehension, each assignment to the comprehension variables that satisfies the conditions is enumerated in lexicographic order. For each such assignment, the values of the comprehension variables are substituted into exp. The resulting expression then becomes one element of the constructed matrix.

The simplest matrix comprehensions have only one comprehension variable, as in the example below.

[ num**2 | num : int(1..5) ] = [ 1,4,9,16,25 ; int(1..5) ]

The matrix constructed by a comprehension is one-dimensional and is either indexed from 1 contiguously, or has the given index domain. The given domain must have a lower bound but is allowed to have no upper bound. For example the first line below produces the matrix on the second line.

[ i+j | i: int(1..3), j : int(1..3), i<j ; int(7..) ]
[ 3, 4, 5 ; int(7..9) ]

Matrix comprehensions allow more advanced forms of slicing than the matrix slice syntax in Section 2.1.7. For example it is possible to slice an arbitrary subset of the rows or columns of a two-dimensional matrix. The following two nested comprehensions will slice out the entries of a matrix M where both rows and columns are odd-numbered, and build a new two-dimensional matrix.

[ [ M[i,j] | j : int(1..n), j%2=1 ] | i : int(1..n), i%2=1 ]

Now we have matrix comprehensions, the Sudoku example can be completed by adding the constraints on the $3\times 3$ subsquares (as shown in Figure 4). A comprehension is used to create a matrix of variables and the matrix is used as the parameter of an allDiff constraint.

In this example, the matrix constructed by the comprehension depends on the values of i and j from the forAll quantifier. The comprehension variables k and l each take one of three values, to cover the 9 entries M[k,l] in the subsquare.

Similarly to quantifiers, matrix comprehension variables can have a matrix domain. For example, the following comprehension builds a two-dimensional matrix where the rows are all permutations of 1..n.

[ perm | perm : matrix indexed by [int(1..n)] of int(1..n), allDiff(perm) ]

Table 2 lists the matrix functions available in Essence Prime.

The functions sum, product, and and or were originally intended to be used with matrix comprehensions, but can be used with any matrix. The quantifiers sum, forAll and exists can be replaced with sum, and and or containing matrix comprehensions. For example, consider the forAll expression below (from the Sudoku model). It can be replaced with the second line below.

forAll row : int(1..9) . allDiff(M[row,..])

and([ allDiff(M[row,..]) | row : int(1..9) ])

In fact, matrix functions combined with matrix comprehensions are strictly more powerful than quantifiers. Also, the function product has no corresponding quantifier. Quantifiers are retained in the language because they can be easier to read.

As a more advanced example, given an $n\times n$ matrix M of decision variables, the sum below is the determinant of M using the Leibniz formula. The outermost comprehension constructs all permutations of $1\ldots n$ using a matrix domain and an allDiff. Lines 3 and 4 contain a comprehension that is used to obtain the number of inversions of perm (the number of pairs of values that are not in ascending order). Finally line 5 builds a product of some of the entries of the matrix. Without the product function, it is difficult (perhaps impossible) to write the Leibniz formula in Essence Prime for a matrix of unknown size $n$.

sum([
    $  calculate the sign of perm from the number of inversions.
    ( (-1) ** sum([ perm[idx1]>perm[idx2]
                  | idx1 : int(1..n), idx2 : int(1..n), idx1<idx2 ]) )*
    product([ M[j, perm[j]] | j : int(1..n) ])
| perm : matrix indexed by [int(1..n)] of int(1..n), allDiff(perm)])

The flatten function is typically used to feed the contents of a multi-dimensional matrix expression into a constraint that accepts only one-dimensional matrices. For example, given a three-dimensional matrix M, the following example is a typical use of flatten.

allDiff( flatten(M[1,..,..]) )

When flattening a matrix M to create a new matrix F, the order of elements in F is defined as follows. Suppose M were written as a matrix literal (as in Section 2.1.3) the order elements are written in the matrix literal is the order the elements appear in F. The following example illustrates this for a three-dimensional matrix.

flatten([ [ [1,2], [3,4] ], [ [5,6], [7,8] ] ]) = [1,2,3,4,5,6,7,8]

Parameters are declared with the given keyword followed by a domain the parameter ranges over. Parameters are allowed to range over the infinite domain int, or domains that contain an open range such as int(1..) and int(..10). For example,

given n : int(0..)

given d : int(0..n)

declares two parameters, and the domain of the second depends on the value of the first. Parameters may have integer, boolean or matrix domains.

Now we have parameters we can generalise the Sudoku model of Figure 3 to represent the problem class of all Sudoku puzzles. The generalised model is shown in Figure 5. The parameter is the clues matrix, where blank spaces are represented as 0 and non-zero entries in clues are copied to M.

In most problem models there are re-occurring constant values and it can be useful to define them as constants. The letting statement allows to assign a name with a constant value. The statement

letting NAME = A

introduces a new identifier NAME that is associated with the expression A. Every subsequent occurrence of NAME in the model is replaced by the value of A. Please note that NAME cannot be used in the model before it has been defined. A may be any integer, boolean or matrix expression that does not contain decision variables. Some integer examples are shown below.

given n : int(0..)
letting c = 10
letting d = c*n*2

Here the second integer constant depends on the first. As well as integer and boolean expressions, lettings may contain matrix expressions, as in the example below. When using a matrix literal the domain is optional – the two lettings below are equivalent. The version with the matrix domain may be useful when the matrix is not indexed from 1.

letting cmatrix = [ [2,8,5,1], [3,7,9,4] ]
letting cmatrix2 : matrix indexed by [ int(1..2), int(1..4) ] of int(1..10)
    = [ [2,8,5,1], [3,7,9,4] ]

Finally new matrices may be constructed using a slice or comprehension, as in the example below where the letting is used for the table of a table constraint.

letting xor_table = [ [a,b,c] | a : bool, b : bool, c : bool,
                                (a /\ b) \/ (!a /\ !b) <-> c ]
find x,y,z : bool
such that
table([x,y,z], xor_table)

Constant domains are defined in a similar way using the keywords be domain.

letting c = 10
given n : int(1..)
letting INDEX be domain int(1..c*n)

In this example INDEX is defined to be an integer domain, the upper bound of which depends on a parameter n and another constant c.

Constant domains are convenient when a domain is reused several times. In the Sudoku running example, we could use a letting for the domain int(1..9), as shown in Figure 6.

Decision variables are declared using the find keyword followed by a name and their corresponding domain. The domain must be finite. The example below

find x : int(1..10)

defines a single decision variable with the given domain. It is possible to define several variables in one find by giving multiple names, as follows.

find x,y,z : int(1..10)

Matrices of decision variables are declared using a matrix domain, as in the following example.

find m : matrix indexed by [ int(1..10) ] of bool

This declares m as a 1-dimensional matrix of 10 boolean variables. Simple and matrix domains are described in Section 2.1.1.

In the Sudoku running example, we have been using the following two-dimensional matrix domain.

find M : matrix indexed by [int(1..9), int(1..9)] of int(1..9)

The options -in-eprime and -in-param specify the input files as in the example below.

savilerow -in-eprime sonet.eprime -in-param sonet1.param

These flags may be omitted for any filename that ends with .eprime, .param, or .eprime-param.

The option -params may be used to specify the parameters on the command line. For example, suppose the nurse.eprime model has two parameters. We can specify them on the command line as follows. The format of the parameter string is identical to the format of a parameter file (where, incidentally, the language line is optional and line breaks are not significant).

savilerow nurse.eprime -params "letting n_nurses=4 letting Demand=[[1,0,1,0],[0,2,1,0]]"

Savile Row produces output for various solvers and classes of solver as described in Section 1.2. The output format is specified by using one of the following command-line options.

-minion
-gecode
-chuffed
-or-tools
-flatzinc
-minizinc
-sat
-smt
-maxsat

The output filename may be specified as follows. In each case there is a default filename so the flag is optional. Default filenames are described in Section 4.4. The flag -out-sat also sets the MaxSAT filename.

-out-minion <filename>
-out-flatzinc <filename>
-out-minizinc <filename>
-out-sat <filename>
-out-smt <filename>

The flag -out-flatzinc sets the FlatZinc filename.

In addition, the file names for solution files, solver statistics files and symbol table files (called aux files) may be specified as follows. Once again there are default filenames described in Section 4.4.

-out-solution <filename>
-out-info <filename>
-out-aux <filename>

The following flag sets each of the output files to prefix.extension where extension is the conventional one for the file type (i.e. .minion, .fzn, .dimacs, etc).

-out-prefix <prefix>

The symbol table is not saved by default. To obtain the symbol table file, use the following flag. The symbol table is used in ReadSolution mode, described below.

-save-symbols

The optimisation levels (-O0 to -O3) provide an easy way to control how much optimisation Savile Row does, without having to switch on or off individual optimisations. The default is -O2, which is intended to provide a generally recommended set of optimisations. The rightmost -O flag on the command line is the one that takes precedence.

-O0

The lowest optimisation level, -O0, turns off all optional optimisations. Savile Row will still simplify expressions (including constraints). Any expression containing only constants will be replaced with its value. Some expressions have quite sophisticated simplifiers that will run even at -O0. For example, allDiff([x+y+z, z+y+x, p, q]) would simplify to false because the first two expressions in the allDiff are symbolically equal after normalisation.

-O0 will do no common subexpression elimination, will not unify equal variables, and will not filter the domains of variables.

-O1

-O1 does optimisations that are very efficient in both space and time. Variables that are equal are unified, and a form of common subexpression elimination is applied (Active CSE, described below). -O1 is equivalent to -deletevars and -active-cse.

-O2

In addition to the optimisations performed by -O1, -O2 performs filtering of variable domains (both find and auxiliary variables) and aggregation (both of which are described in the following section). -O2 is the default optimisation level. -O2 adds -reduce-domains-extend and -aggregate compared to -O1.

-O3

In addition to -O2, -O3 enables tabulation (-tabulate) and associative-commutative common subexpression elimination (-ac-cse) (both described below).

The options -S0, -S1 and -S2 control optional optimisations that can change the number of solutions. The default is -S1 which applies only very simple and fast optimisations.

-S0

Preserve the number of solutions, i.e. perform no optimisations that might change the number of solutions.

-S1

Remove variables that appear in no constraints, and allow Savile Row to introduce auxiliary variables that are not functionally defined by the primary (‘find’) variables. At present, non-functional auxiliary variables are only used with the SAT, MaxSAT and SMT backends. Equivalent to -remove-redundant-vars and -aux-non-functional.

-S2

In addition to -S1, apply a graph automorphism solver to find symmetries among the decision variables. The symmetries are then broken using the standard lex-leader method. Equivalent to adding the flag -var-sym-breaking to -S1.

Savile Row currently implements four types of common subexpression elimination (CSE). Identical CSE finds and eliminates syntactically identical expressions. This is the simplest form of CSE, however it can be an effective optimisation. Active CSE performs some reformulations (for example applying De Morgan’s laws) to reveal expressions that are semantically equivalent but not syntactically identical. Active CSE subsumes Identical CSE. Active CSE is enabled by default as part of -O2. Associative-Commutative CSE (AC-CSE) works on the associative and commutative (AC) operators +, *, /\ (and) and \/ (or). It is able to rearrange the AC expressions to reveal common subexpressions among them. AC-CSE is not enabled by default. It would normally be used in conjunction with Identical or Active CSE. Finally, Active AC-CSE combines one active reformulation (integer negation) with AC-CSE, so for example Active AC-CSE is able to extract $y-z$ from the three expressions $x+y-z$, $w-x-y+z$, and $10-y+z$, even though the sub-expression occurs as $y-z$ in one and $-y+z$ in the other two. Active AC-CSE is identical to AC-CSE for And, Or and Product, it differs only on sum.

The following flags control CSE. The first, -no-cse, turns off all CSE. The other flags each turn on one type of CSE.

-no-cse
-identical-cse
-active-cse
-ac-cse
-active-ac-cse

Savile Row can remove a decision variable (either variables declared with find or auxiliary variables introduced during tailoring) when the variable is equal to a constant, or equal to another variable. This is often a useful optimisation. It can be enabled using the following flag.

-deletevars

It can be useful to filter the domains of variables. In Savile Row this is done by running the translation pipeline to completion and producing a Minion file, then running Minion usually with the options -preprocess SACBounds_limit -outputCompressedDomains. With these options Minion performs conventional propagation plus SAC on the lower and upper bound of each variable (SACBounds, also known as shaving) with a limit on the number of iterations. The filtered domains are then read back in to Savile Row. The translation process is started again at the beginning. Thus domain filtering can benefit the entire translation process: variables can be removed (with -deletevars), constraint expressions can be simplified or even removed (if they are entailed), the number of auxiliary variables may be reduced. In some cases domain filtering can enable another optimisation, for example on the BIBD problem it enables associative-commutative CSE to do some very effective reformulation.

Domain filtering can be used with any target solver (but Minion is always used to perform the domain filtering regardless of the target solver). It is switched on using the following flag.

-reduce-domains

Standard domain filtering affects the decision variables defined by find statements. Auxiliary variables created by Savile Row are not filtered by default. To enable filtering of both find variables and auxiliary variables, use the following flag:

-reduce-domains-extend

Aggregation collects sets of constraints together to form global constraints that typically propagate better in the target solver. At present there are two aggregators for allDifferent and GCC. Savile Row constructs allDifferent constraints by collecting not-equal, less-than and other shorter allDifferent constraints. GCC is aggregated by collecting atmost and atleast constraints over the same scope.

-aggregate

Tabulation converts constraint expressions into table constraints to improve propagation. A set of four heuristics are used to identify candidate expressions for tabulation. When tabulating a constraint, the number of tuples is limited to 10,000 to avoid spending excessive time on one constraint. Refer to the CP 2018 paper for more detail [1].

-tabulate

The factor encoding of table constraints [6] may be useful to strengthen propagation when a problem class has overlapping table constraints (or tabulation produces overlapping table constraints). It is enabled with the following flag.

-factor-encoding

When creating Minion output Savile Row will by default use the DISCRETE or BOOL variable type when the variable has fewer than 10,000 values and BOUND otherwise. DISCRETE and BOOL represent the entire domain and BOUND only stores the upper and lower bound, thus propagation may be lost when using BOUND. The following flag prevents Savile Row using BOUND variables.

-no-bound-vars

The following flag causes Savile Row to remove any decision variables that are not mentioned in a constraint or in the objective function. It is enabled by default as part of -S1.

-remove-redundant-vars

The following flag allows Savile Row to to create auxiliary variables that are not functionally defined on the primary variables. May change the number of solutions. Currently only affects the SAT, SMT, MaxSAT backends. Typically a non-functional variable would be $\leq$ or $\geq$ an expression rather than equal to the expression, thus avoiding encoding one side of the equality.

-aux-non-functional

If variable symmetry breaking is enabled, Savile Row will apply a graph automorphism solver based on Ferret to find symmetries among the decision variables. Any symmetries discovered will be broken by the standard lex-leader method. It is disabled by default because it can be expensive. Variable symmetry breaking is part of -S2.

-var-sym-breaking

The SAT backend in general is described in Appendix A. There are several options for encoding constraints into SAT, in particular sums and tables.

Sum constraints are divided into three groups and there are flags to control the encoding of each group. The simplest group is at-most-one (AMO) and exactly-one (EO) constraints containing only Boolean terms (not just Boolean variables but any expression of type Boolean) and where all coefficients are 1. The encoding of these constraints is controlled by -sat-amo flags. Pseudo-Boolean (PB) sums also contain only Boolean terms but can have coefficients other than 1. The encoding of PB constraints is controlled by -sat-pb flags. Finally, the encoding of general sums (containing at least one integer term) is controlled by -sat-sum flags.

Binary table constraints use the support encoding. For non-binary tables, the default encoding introduces a SAT variable for each tuple and was proposed by Bacchus [3]. Another encoding based on MDDs is available for non-binary tables, enabled with the following flag:

-sat-table-mdd

The default encoding for AMO and EO constraints is Chen’s 2-product, it is small and tends to be efficient. Other encodings are available: the Commander encoding of Klieber and Kwon (with group size 3); the ladder encoding; an encoding similar to the totalizer (named Tree); the pairwise encoding (with no auxiliary SAT variables); and the bimander encoding with group size 2. The flags to select the encoding are below:

-sat-amo-product  (default)
-sat-amo-commander
-sat-amo-ladder
-sat-amo-tree
-sat-amo-pairwise
-sat-amo-bimander

There are nine encodings of Pseudo-Boolean constraints. Eight of them are based on Bofill et al [4] (with thanks to Jordi Coll for providing the implementations): Multi-valued Decision Diagrams (MDD); the Global Polynomial Watchdog (GPW); the Local Polynomial Watchdog (LPW); the Sequential Weighted Counter (SWC); the Generalized Generalized Totalizer (GGT); the Reduced Generalized Generalized Totalizer (RGGT); another version of GGT with a tree-construction heuristic (GGTH); and the Generalized n-Level Modulo Totalizer (GMTO). Each of these is implemented exactly as described in [4]. For these eight encodings, any pseudo-Boolean equality constraints are decomposed into $\leq$ and $\geq$. Also these eight encodings support only top-level constraints (i.e. constraints that are not nested inside a logic expression). The flags are as follows:

-sat-pb-mdd
-sat-pb-gpw
-sat-pb-lpw
-sat-pb-swc
-sat-pb-ggt
-sat-pb-rggt
-sat-pb-ggth
-sat-pb-gmto

The final encoding (called Tree) is similar to the Generalized Totalizer. It can directly encode sum-equality, and can also encode non-top-level constraints. It is the default encoding and also the fallback for non-top-level constraints when using one of the other encodings.

-sat-pb-tree  (default)

The first eight encodings (MDD, GPW, LPW, SWC, GGT, RGGT, GGTH, GMTO) are able to take advantage of at-most-one (and exactly-one) relations on the Boolean variables to reduce the size of the encoding. All four of these encodings work with automatic AMO and EO detection as described in the CP 2019 paper [2], which uses Minion to find mutexes between variables then constructs maximal cliques of the mutex graph. The flag below is used to switch on the AMO and EO detection. It is often worthwhile for sufficiently challenging instances with PB constraints.

-amo-detect

The options for encoding general sums (any sum containing at least one integer variable) are the same as for PB constraints. The flags are as follows:

-sat-sum-mdd
-sat-sum-gpw
-sat-sum-lpw
-sat-sum-swc
-sat-sum-ggt
-sat-sum-rggt
-sat-sum-ggth
-sat-sum-gmto
-sat-sum-tree  (default)

The Tree encoding natively handles integer terms. The other eight (MDD, GPW, LPW, SWC, GGT, RGGT, GGTH, GMTO) treat integer terms as a group of Boolean terms (e.g. $1*(x=1)+2*(x=2)+\cdots$) with an exactly-one relation on them. These eight encodings also can benefit from automatically detected AMO and EO relations with the -amo-detect flag.

The SMT backend, enabled with the -smt flag, is able to produce the SMT-LIB 2 language with a choice of four theories: QF_BV (the theory of bit vectors), QF_IDL (integer difference logic), QF_LIA (linear integer arithmetic), and QF_NIA (nonlinear integer arithmetic). The theory is selected using one of the four flags below:

-smt-bv  (default)
-smt-idl
-smt-lia
-smt-nia

For each theory there is a choice of nested or flat encodings, where nested aims to maintain the original nesting of expressions (for example, a product within a sum) as far as possible, whereas flat removes nesting by introducing auxiliary variables. Nested is the default. The encoding may be selected using one of the flags below:

-smt-nested  (default)
-smt-flat

The SMT backend is described and evaluated in a CP 2020 paper [7], including comparison of the four theories and two encodings.

Combined with -run-solver, the SMT backend will run Boolector, Z3, or Yices2. It will select a default solver for the chosen theory, or the solver can be set manually using one of the following flags:

-boolector  (default for QF_BV theory)
-z3         (default for QF_NIA)
-yices2     (default for QF_IDL and QF_LIA)

Choosing a solver does not affect any other setting of the SMT backend. If the solver does not support the chosen theory (at the time of release) Savile Row will output a warning and continue.

The following flag produces a warning when the semantics of a model is affected by undefinedness (see Section 3).

-Wundef

The following flag specifies a time limit in seconds. Savile Row will stop when the time limit is reached, unless it has completed tailoring and is running a backend solver. The time measured is wallclock time not CPU time.

-timelimit <time>

Time limits may also be passed through to solvers, for example when using Minion as the backend solver, the following flag will limit Minion’s run time (specified in seconds).

-solver-options "-cpulimit <time>"

A similar approach can be used to apply a time limit to other solvers.

In some cases the SAT or MaxSAT output can be very large. The following option allows the number of clauses to be limited. If the specified number of clauses is reached, Savile Row will delete the partial SAT file and exit.

-cnflimit <numclauses>

Some reformulations use a pseudorandom number generator with a fixed seed. The following option may be used to set a different seed.

-seed <integer>

The following flag causes Savile Row to run a solver and parse the solutions produced by it. This is currently implemented for Minion, Gecode, Chuffed, Standard FlatZinc, SAT, SMT, and MaxSAT backends.

-run-solver

The following two flags control the number of solutions. The first causes the solver to search for all solutions (and Savile Row to parse all solutions). The second specifies a required number of solutions.

-all-solutions
-num-solutions <n>

When parsing solutions the default behaviour is to create one file for each solution. As an alternative, the following flag will send solutions to standard out, separated by lines of 10 minus signs.

-solutions-to-stdout

To prevent solutions being output at all, use the following flag.

-solutions-to-null

The following flag passes through command-line options to the solver. The string would normally be quoted.

-solver-options <string>

For example when using Minion -solver-options "-cpulimit <time>" may be used to impose a time limit, or when using Gecode -solver-options "-p 8" causes Gecode to parallelise to 8 cores.

The following flag specifies where the Minion executable is. The default value is minion.

-minion-bin <filename>

When Minion is run directly by Savile Row, preprocessing is usually applied before search starts. The following flag allows the level of preprocessing to be specified.

-preprocess LEVEL
    where LEVEL is one of None, GAC, SAC, SAC_limit, SSAC, SSAC_limit,
    SACBounds, SACBounds_limit, SSACBounds, SSACBounds_limit

The default level of preprocessing is SACBounds_limit.

The -preprocess flag affects the behaviour of Minion in two cases: first when Minion is called to filter domains (the -reduce-domains option), and second when Minion is called to search for a solution.

The following flag specifies where the Gecode executable is. The default value is fzn-gecode.

-gecode-bin <filename>

The following flag specifies where the Chuffed executable is. The default value is fzn-chuffed.

-chuffed-bin <filename>

The following flag specifies where the OR Tools executable is. The default value is fzn-ortools.

-or-tools-bin <filename>

By default OR Tools is called without its “free search” option. To enable free search, use the pass-through flag:

-solver-options "-f"

The following flag specifies a FlatZinc solver binary.

-fzn-bin <filename>

Savile Row is able to run and parse the output of MiniSAT, Lingeling, Glucose, CaDiCaL, and kissat solvers as well as two MiniSAT-based solvers for finding all solutions. The following flag specifies which family of solvers is used. Kissat is the default.

-sat-family [ minisat | lingeling | glucose | cadical | kissat |
              nbc_minisat_all | bc_minisat_all ]

The ‘all’ values imply the -all-solutions flag.

The following flag specifies the SAT solver executable. The default value is minisat, lingeling, glucose, cadical, kissat, nbc_minisat_all_release, or bc_minisat_all_release depending on the SAT family.

-satsolver-bin <filename>

The following flag enables interactive usage of the supported solvers when Savile Row is built with this feature. Supported SAT solvers are used incrementally via JNI calls. Currently supported: glucose, cadical, and nbc_minisat_all.

-interactive-sat

When using SAT or SMT solvers, optimisation is performed with multiple calls to the solver. There are three modes: bisect (default), linear, and unsat. Each places constraints on the (encoding of the) objective variable. Bisect splits the interval of the objective variable into two approximately equal sub-intervals, and attempts to find a solution in the better sub-interval (i.e. smaller if minimising). The interval is updated and the procedure is repeated until the interval becomes empty, at which point the last solution found is an optimal solution. Linear bounds the objective variable each time a solution is found, such that the next solution will be better. Unsat assigns the objective variable to its best remaining value (smallest value when minimising). If no solution is found, the best value is removed and the procedure iterates, continuing until a solution is found.

The optimisation strategy may be set with the following flag:

-opt-strategy [ bisect | linear | unsat ]

To set the SMT solver executable use the following flag. If it is not set, then Savile Row will look for a binary named z3, yices-smt2, or boolector in the bin directory (depending which SMT solver was selected, boolector by default, see Section 4.5.7).

-smtsolver-bin <filename>

Note that the -opt-strategy flag is relevant when doing optimisation with an SMT solver.

Savile Row has two modes of operation, Normal and ReadSolution. Normal is the default, and in this mode Savile Row reads an Essence Prime model file and optional parameter file and produces output for a solver. In some cases it will also run a solver and parse the solution(s), producing Essence Prime solution files.

When using ReadSolution mode, Savile Row will read a solution in Minion format and translate it back to Essence Prime. This allows the user to run Minion separately from Savile Row but still retrieve the solution in Essence Prime format. When running Minion, the -solsout flag should be used to retrieve the solution(s) in a table format.

The mode is specified as follows.

-mode [Normal | ReadSolution]

When using ReadSolution mode, the name of the aux file previously generated by Savile Row needs to be specified using the -out-aux flag, so that Savile Row can read its symbol table. Also the name of the solution table file from Minion is specified using -minion-sol-file. -out-solution is required to specify where to write the solutions. -all-solutions and -num-solutions <n> are optional in ReadSolution mode. Below is a typical command.

savilerow -mode ReadSolution -out-aux <filename> -minion-sol-file <filename>
                             -out-solution <filename>

When neither -all-solutions nor -num-solutions <n> is given, Savile Row parses the last solution in the Minion solutions file. For optimisation problems, the last solution will be the optimal or closest to optimal.