Input Format

This section describes the Minion file format. Usually, it is easier to look at an example, as the foramt is fairly self-explanatory, but this section contains full technical deails. This section only describes the file format, the full description of the different types of variables and constraints is given in earlier sections.

The Minion input format is expressed as a series of sections, each section starts with two starts (for example **VARIABLES** for variables). The format of each section is different.

Files start with the string MINION 3, and end with **EOF**.

Minion3Input::= MINION 3

<InputSection>+ EOF

InputSection::= <VariablesSection>
<SearchSection>
<ConstraintsSection>
<TuplelistSection>
<ShortTuplelistSection>

All text from a ‘#’ character to the end of the line is ignored.

See the associated help entries below for information on each section.

Variables

The variables section consists of any number of variable declarations on separate lines.

VariablesSection::= VARIABLES

<VarDeclaration>*

Example

**VARIABLES**

BOOL bool                          #boolean var
BOUND b {1..3}                     #bounds var
SPARSEBOUND myvar {1,3,4,6,7,9,11} #sparse bounds var
DISCRETE d[3] {1..3}               #array of discrete vars

Constants

Minion supports the use of constants anywhere where a variable can be used. For example, in a constraint as a replacement for a single variable, or a vector of constants as a replacement for a vector of variables.

Example

Use of a constant:

eq(x,1)

Use of a constant vector:

element([10,9,8,7,6,5,4,3,2,1],idx,e)

Vectors

Vectors, matrices and tensors can be declared in minion input. Matrices and tensors are for convenience, as constraints do not take these as input; they must first undergo a flattening process to convert them to a vector before use. Additional commas at the end of vectors are ignored (see example below).

Example

A vector of 0/1 variables:

BOOL myvec[5]

A matrix of discrete variables:

DISCRETE sudoku[9,9] {1..9}

A 3D tensor of 0/1s:

BOOL mycube[3,3,2]

One can create a vector from scalars and elements of vectors, etc.:

alldiff([x,y,myvec[1],mymatrix[3,4]])

When a matrix or tensor is constrained, it is treated as a vector whose entries have been strung out into a vector in index order with the rightmost index changing most quickly, e.g.:

alldiff(sudoku)

is equivalent to

::

alldiff([sudoku[0,0],…,sudoku[0,8],…,sudoku[8,0],…,sudoku[8,8]]):

Furthermore, with indices filled selectively and the remainder filled with underscores (_) the flattening applies only to the underscore indices:

alldiff(sudoku[4,_])

is equivalent to:

alldiff([sudoku[4,0],...,sudoku[4,8]])

Lastly, one can optionally add square brackets ([]) around an expression to be flattened to make it look more like a vector:

alldiff([sudoku[4,_]])

is equivalent to:

alldiff(sudoku[4,_])

Additional hanging commas at the end of array are ignored, e.g.:

lexleq([A,B,C,],[D,E,F,])

is equivalent to

::

lexleq([A,B,C],[D,E,F]):

Aliases

Specifying an alias is a way to give a variable another name. Aliases appear in the VARIABLES section of an input file. It is best described using some examples:

ALIAS c = a

ALIAS c[2,2] = [[myvar,b[2]],[b[1],anothervar]]

Booleans

Booleans, or 0/1 variables are used very commonly for logical expressions. Note that wherever a 0/1 variable can appear, the negation of that variable can also appear. A boolean variable x’s negation is written as !x identified by !x.

Example

Declaration of a 01 variable called bool in input file:

BOOL bool

Use of this variable in a constraint:

eq(bool, 0) #variable bool equals 0

Discrete

Discrete variables are given a domain with a lower and upper bound.

Example

Declaration of a discrete variable x with domain {1,2,3,4} in input file:

DISCRETE x {1..4}

Use of this variable in a constraint:

eq(x, 2) #variable x equals 2

Bounds

Bounds variables, where only the upper and lower bounds of the domain are maintained. These domains must be continuous ranges of integers i.e. holes cannot be put in the domains of the variables.

Example

Declaration of a bound variable called myvar with domain between 1 and 7 in input file:

BOUND myvar {1..7}

Use of this variable in a constraint:

eq(myvar, 4) #variable myvar equals 4

Sparse Bound

In sparse bounds variables the domain is composed of discrete values (e.g. {1, 5, 36, 92}).

Example

Declaration of a sparse bounds variable called myvar containing values {1,3,4,6,7,9,11} in input file:

SPARSEBOUND myvar {1,3,4,6,7,9,11}

Use of this variable in a constraint:

eq(myvar, 3) #myvar equals 3

Constraints

The constraints section consists of any number of constraint declarations on separate lines.:

ConstraintsSection::= **CONSTRAINTS**
                      <ConstraintDeclaration>*

A tuplelist section lists of allowed tuples for table constraints can be specified. This technique is preferable to specifying the tuples in the constraint declaration, since the tuplelists can be shared between constraints and named for readability.

The required format is

TuplelistSection::= TUPLELIST

<Tuplelist>*

Tuplelist::= <name> <num_tuples> <tupleLength> <numbers>+

Example

**TUPLELIST** AtMostOne 4 3 0 0 0 0 0 1 0 1 0 1 0 0

Short Tuple Lists

A shorttuplelist section lists of allowed tuples for haggisgac, shortstr2, shortctuplestr2 and other constraints which accept short tuple lists.

The required format is:

TuplelistSection::= **TUPLELIST**
                    <Tuplelist>*

Tuplelist::= <name> <num_tuples> <shortTuple>+

shortTuple ::= [ <literal>*, ]

literal ::= (<num>, <num>)

Example

An example is given below:

**SHORTTUPLELIST**
mycon 4
[(0,0),(3,0)]
[(1,0),(3,0)]
[(2,0),(3,0)]
[(0,1),(1,1),(2,1),(3,1)]

Which represents the same constraint as:

**TUPLELIST**
mycon 8 4
0 0 0 0
0 0 1 0
0 1 0 0
0 1 1 0
1 0 0 0
1 0 1 0
1 1 0 0
1 1 1 1

Short tuples give us a way of shrinking some constraints. Short tuples consist of pairs (x,y), where x is a varible position, and y is a value for that variable. For example, [(0,0),(3,0)] represents “If the variable at index 0 is 0, and the variable at index 3 is 0, then the constraint is true”.

Some constraints (currently just shortctuplestr2) allow more than one literal per variable for example, [(0,0),(0,1),(3,0)] represents ‘if the variable at index 0 is 0 or 1, and the variable at index 3 is 0, then the constraint is true’.

Note that some tuples are double-represented in the example ‘mycon’. The first 3 short tuples all allow the assignment ‘0 0 0 0’. This is fine. The important thing for efficency is to try to give a small list of short tuples.