Tutorials

We demonstrate the use of Conjure for some small problems.

Number puzzle

Authors: András Salamon, Özgür Akgün

We first show how to solve a classic word addition puzzle, due to Dudeney [Dud24]. This is a small toy example, but already illustrates some interesting features of Conjure.

   SEND
+  MORE
-------
= MONEY

Here each letter represents a numeric digit in an addition, and we are asked to find an assignment of digits to letters so that the number represented by the digits SEND when added to the number represented by MORE yields the number represented by MONEY.

Initial model

We are looking for a mapping (a function) from letters to digits. We can represent the different letters as an enumerated type, with each letter appearing only once.

language Essence 1.3
letting letters be new type enum {S,E,N,D,M,O,R,Y}
find f : function letters --> int(0..9)
such that
                   1000 * f(S) + 100 * f(E) + 10 * f(N) + f(D) +
                   1000 * f(M) + 100 * f(O) + 10 * f(R) + f(E) =
    10000 * f(M) + 1000 * f(O) + 100 * f(N) + 10 * f(E) + f(Y)

Each Essence specification can optionally contain a declaration of which dialect of Essence it is written in. The current version of Essence is 1.3. We leave out this declaration in the remaining examples.

This model is stored in sm1.essence; let’s use Conjure to find the solution:

conjure solve -ac sm1.essence

Unless we specify what to call the solution, it is saved as sm1.solution.

letting f be function(S --> 0, E --> 0, N --> 0, D --> 0, M --> 0, O --> 0, R --> 0, Y --> 0)

This is clearly not what we wanted. We haven’t specified all the constraints in the problem!

Identifying a missing constraint

In these kinds of puzzles, usually we need each letter to map to a different digit: we need an injective function. Let’s replace the line

find f : function letters --> int(0..9)

by

find f : function (injective) letters --> int(0..9)

and save the result in file sm2.essence. Now let’s run Conjure again on the new model:

conjure solve -ac sm2.essence

This time the solution sm2.solution looks more like what we wanted:

letting f be function(S --> 2, E --> 8, N --> 1, D --> 7, M --> 0, O --> 3, R --> 6, Y --> 5)

Final model

There is still something strange with sm2.essence. We usually do not allow a number to begin with a zero digit, but the solution maps M to 0. Let’s add the missing constraints to file sm3.essence:

letting letters be new type enum {S,E,N,D,M,O,R,Y}
find f : function (injective) letters --> int(0..9)
such that
                   1000 * f(S) + 100 * f(E) + 10 * f(N) + f(D) +
                   1000 * f(M) + 100 * f(O) + 10 * f(R) + f(E) =
    10000 * f(M) + 1000 * f(O) + 100 * f(N) + 10 * f(E) + f(Y)

such that f(S) > 0, f(M) > 0

Let’s try again:

conjure solve -ac sm3.essence

This now leads to the solution we expected:

letting f be function(S --> 9, E --> 5, N --> 6, D --> 7, M --> 1, O --> 0, R --> 8, Y --> 2)

Finally, let’s check that there are no more solutions:

conjure solve -ac sm3.essence --number-of-solutions=all

This confirms that there is indeed only one solution. As an exercise, verify that the first two models have multiple solutions, and that the solution given by the third model is among these. (The first has 1155 solutions, the second 25.)

The Knapsack problem

Authors: Saad Attieh and Christopher Stone

The Knapsack problem is a classical combinatorial optimisation problem, often used in areas of resource allocation. A basic variant of the Knapsack problem is defined as follows:

• Given:

  1. A set of items, each with a weight and a value,

  2. A maximum weight which we call capacity,

• find a set of the items such that

  1. The sum of the weights of the items in our set is less than or equal to the capacity,and

  2. The sum of the values of the items is maximised.

Informally, think about putting items in a sack such that we maximise the total value of the sack whilst not going over the sack’s weight limit.

We begin by showing the entire problem as defined in Essence:

given items new type enum
given weight : function (total) items --> int
given gain : function (total) items --> int
given capacity : int
find picked : set of items
maximising sum i in picked . gain(i)
such that (sum i in picked . weight(i)) <= capacity

Going through the problem line by line:

We begin by defining the parameters to the problem. Parameters are given in a separate file, allowing different instances of the same problem to be solved without having to change the specification.

Each parameter is denoted with the given keyword.

given items new type enum

This line says that a set of items will be provided in the parameter file as an enum type. Enums are good for labeling items where it makes no sense to attribute a value to each item. So instead of using integers to represent each item, we may just assign names to each item and group the names under an enum type. Below is an example enum declaration, as it would be written in the parameter file:

letting items be new type enum {a,b,c,d,e}

a, b, etc. are just names we have given, they could be anything bread, whiskey, …

given weight : function (total) items --> int

Another parameter, a function that maps from each item to an integer, we will treat these integers as weights. Since we are describing integers that will be given in the parameter file, no domain (lower/upper bound) is required. Here is an example function parameter as given in a parameter file:

letting weight be function
    ( a --> 15
    , b --> 25
    , c --> 45
    , d --> 50
    , e --> 60
    )

given gain : function (total) items --> int

Just the same as the weight parameter, this parameter is used to denote a mapping from each item to a value. An example value for this parameter as it would be defined in the parameter file is:

letting gain be function
    ( a --> 10
    , b --> 20
    , c --> 40
    , d --> 40
    , e --> 50
    )

The final given:

given capacity : int

The final parameter – a weight limit. Example value in parameter file:

letting capacity be 80

find picked : set of items

The find keyword denotes decision variables, these are the variables for which the solver will search for a valid assignment. As is common in Essence problems, our entire problem is modelled using one decision variable named picked. Its type is set of items; a set of any size whose elements are taken from the items domain. Note, the maximum cardinality of the set is implicitly the size of the items domain.

maximising sum i in picked . gain(i)

The maximising keyword denotes the objective for the solver; a value for the solver to maximise. minimise is also a valid objective keyword. The expression sum i in picked . is a quantifier. The sum says that the values we produce should be summed together. The i in picked says we want to list out every element of the set picked. The expression given to the sum are described by the expression that follows the full-stop (.). In this case, we are asking for the image of i in the gain function. That is, for each item in the set, we are looking up the integer value that the item maps to in the gain function and summing these integers.

such that (sum i in picked . weight(i)) <= capacity

The such that keyword denotes a constraint. Here the constraint is formulated in a similar manner to the objective. We are quantifying over the set of chosen items picked, looking up the value that the item maps to in the weights function and summing these values to together. We enforce that the result of the sum must be less than or equal to the capacity <= capacity.

Note that you can post multiple constraints either by using commas between each constraint , or by reusing the keyword such that.

Nurse rostering

Authors: András Salamon, Nguyen Dang, Saad Attieh

We now discuss a version of Nurse Rostering, a constrained scheduling problem. Variants of this problem are also known by other names, such as workforce planning and staff scheduling. Unlike versions of this problem studied by operations research practitioners and researchers (such as competition instances [CDDC+19]), we here focus on just a few of the simplest constraints.

Some nurses are available to work in a hospital. Each day is divided into a sequence of shifts, for instance an early-morning shift, a day shift, and a night shift. Each nurse should be assigned to work some shifts during the course of a period of consecutive days. A nurse can be assigned to at most one shift per day. Moreover, for each nurse we need to avoid some forbidden shift patterns within two consecutive days. For example, a nurse cannot work a night shift on one day, and an early-morning shift the next day. We also must make sure to meet the minimum number of nurses required for each shift. These demand values may vary between different days.

Initial specification

To begin with, let’s ignore the forbidden patterns, and focus instead on the elements needed to model the problem. We need nurses, shifts for each day, the minimum demand, and a roster.

given nNurses, nDays : int(1..)
given shifts new type enum
letting days be domain int(1..nDays)
letting nurses be domain int(1..nNurses)
letting nShifts be |`shifts`|
given forbiddenPatterns : set of tuple (shifts, shifts)
given minimumDemand : function (total) (days, shifts) --> int(0..nNurses)
where
   forAll d : days .
      (sum s : shifts . minimumDemand((d,s))) <= nNurses

find roster: function (days, shifts) --> nurses
$ constraint 1 (Single assignment per day)
$ a nurse can be assigned to at most one shift per day
such that
   forAll nurse : nurses .
      forAll day : days .
         (sum ((d,_),n) in roster . toInt(n=nurse /\ d=day)) <= 1

This specification contains the basic elements. We made the choice to use an enumerated type for shifts, positive integers to number the nurses and the days, a set of forbidden patterns (each being a pair of shifts), and a total function mapping each shift slot to a number of nurses to represent the minimum demands. Because we only allow a nurse to work one shift each day, the forbidden patterns can only apply to one day and the next day, with the first shift in a forbidden pattern referring to the first day and the second shift referring to the subsequent day. We also added a where condition to ensure that instances are not trivially impossible, by requiring the minimum demand to never exceed the number of nurses.

We also need a test instance. Generating test instances is an interesting subject (for instance, see [AkgunDM+19a]) but here we have just made one up.

letting nNurses be 5
letting nDays be 7
letting shifts be new type enum {Early, Late, Night}
letting forbiddenPatterns be {
   (Late,Early), (Night,Early), (Night,Late)
}
letting minimumDemand be function (
   (1,Early) --> 2, (1,Late) --> 2, (1,Night) --> 0,
   (2,Early) --> 1, (2,Late) --> 1, (2,Night) --> 2,
   (3,Early) --> 1, (3,Late) --> 1, (3,Night) --> 1,
   (4,Early) --> 0, (4,Late) --> 0, (4,Night) --> 1,
   (5,Early) --> 1, (5,Late) --> 1, (5,Night) --> 2,
   (6,Early) --> 2, (6,Late) --> 1, (6,Night) --> 1,
   (7,Early) --> 0, (7,Late) --> 1, (7,Night) --> 1
)

We have 5 nurses, 7 days in the period, three shifts each day, three forbidden pairs of shifts, and some minimum demands for the various shifts.

Changing an overly restrictive assumption

However, on further reflection this first specification is not correct. Since roster is a function (days, shifts) --> nurses only one nurse can be assigned to the same shift of the same day. This means that if the minimum demand asks for 2 or more nurses for a particular day and shift, then we can’t satisfy this demand. We need to remove the overly restrictive assumption enforced by our choice of representation for roster.

Let’s change the representation of roster, leaving the specification exactly the same up to and including the where condition. Instead of mapping each day/shift pair to a single nurse, we could map each day/shift pair to a set of nurses, map each nurse to a set of day/shift pairs, or map each combination of day and nurse to a shift (but with not all combinations needing to be assigned). Each of these choices leads to a slightly different way to model the problem; here we have picked the last. It is left as an exercise to try the others!

find roster: function (days, nurses) --> shifts
$ constraint 1 (Single assignment per day)
$ a nurse can be assigned to at most one shift per day
$ NOTE: automatically satisfied because of how "roster" is defined

$ constraint 2 (Under staffing)
$ the number of nurses for each shift suffice for the minimum demand
such that
   forAll day : days .
      forAll shift : shifts .
         (sum ((d,_),s) in roster . toInt(d=day /\ s=shift))
            >= minimumDemand((day,shift))

$ constraint 3 (Shift type successions)
$ the shift type assignments of one nurse on two consecutive days
$ must not violate any forbidden succession
such that
   forAll d : int(1..(nDays-1)) .
      forAll n : nurses .
         !((roster(d,n), roster(d+1,n)) in forbiddenPatterns)

Note that in this specification, the first constraint is automatically satisfied because of the way we have defined roster as a function from a day/nurse pair to a shift. So changing the representation of roster has not only removed the overly restrictive assumption that only one nurse can be assigned to a day/shift pair, but also dealt with the first real constraint.

We have added a second constraint to enforce the minimum demand for each shift, by requiring that the number of nurses mapped to each day/shift pair is at least as large as the minimum demand for that day/shift pair.

Finally, we have added a third constraint to ensure that forbidden shift patterns do not occur.

Final model

Unfortunately, the second specification is not accepted by Conjure. The roster function is expecting a single pair as its argument, but we have given two arguments (a day and a nurse). We replace the last constraint by a version that corrects this syntax error:

$ constraint 3 (Shift type successions)
$ the shift type assignments of one nurse on two consecutive days
$ must not violate any forbidden succession
such that
   forAll d : int(1..(nDays-1)) .
      forAll n : nurses .
         !((roster((d,n)), roster((d+1,n))) in forbiddenPatterns)

This is a specification that is acceptable to Conjure and which captures the key constraints we wanted to include.

Assuming that the third specification is in file model3.essence and the test instance in file test.param, we can run Conjure to solve the instance.

conjure solve -ac model3.essence test.param

Without any specification, the default solver is Minion [CDDC+19], a constraint programming solver. After quite some time, this creates the following solution:

letting roster be function(
   (1, 2) --> Early, (1, 3) --> Early, (1, 4) --> Late,  (1, 5) --> Late,
   (2, 2) --> Early, (2, 3) --> Late,  (2, 4) --> Night, (2, 5) --> Night,
   (3, 2) --> Early, (3, 3) --> Late,  (3, 4) --> Night, (4, 5) --> Night,
   (5, 2) --> Early, (5, 3) --> Late,  (5, 4) --> Night, (5, 5) --> Night,
   (6, 1) --> Early, (6, 2) --> Early, (6, 3) --> Late,  (6, 4) --> Night,
   (7, 4) --> Night, (7, 5) --> Late)

A much faster way to obtain a solution is to ask Minion to use the domoverwdeg variable ordering, which is often effective on constrained scheduling problems:

conjure solve -ac --solver-options='-varorder domoverwdeg' model3.essence test.param

Choosing the right parameters to control solver behaviour is important but not generally well understood, and we leave discussion of this problem for another time.

Labelled connected graphs

Author: András Salamon (with thanks to Roy Dyckhoff for proofreading)

We illustrate the use of Conjure to enumerate all labelled connected graphs. The number of labelled connected graphs over a fixed set of n distinct labels grows quickly; this is OEIS sequence A001187.

We first need to decide how to represent graphs. A standard representation is to list the edges. One natural representation for each edge is as a set of two distinct vertices. Vertices of the graph are labelled with integers between 1 and n, and each vertex is regarded as part of the graph, whether there is some edge involving that vertex or not.

letting n be 4
letting G be {{1,2},{2,3},{3,4}}

In this specification, we declare two aliases. The number of vertices n is first defined as 4. Then G is defined as a set of edges.

This specification is saved in a file path-4.param that we refer to later. We should also have a different graph that is not connected:

letting n be 4
letting G be {{1,2},{4,3}}

which is saved in file disconnected-4.param.

We now need to express what it means for a graph to be connected.

Model 1: distance matrix

In our first attempt, we use a matrix of distances. Each entry reach[u,v] represents the length of a shortest path from u to v, or n if there is no path from u to v. To enforce this property, we use several constraints, one for each possible length; there are four ranges of values we need to cover. A distance of 0 happens when u and v are the same vertex. A distance of 1 happens when there is an edge from u to v. When the distance is greater than 1 but less than n, then there must be some vertex that is a neighbour of u from which v is reachable in one less step. Finally, the distance of n is used when no neighbour of u can reach v (and in this case, the neighbours all have distance of n to v as well).

given n : int(1..)
letting vertices be domain int(1..n)
given G : set of set (size 2) of vertices
find reach : matrix indexed by [vertices, vertices] of int(0..n)
such that
  forAll u,v : vertices .
     ((reach[u,v] = 0) -> (u=v))
  /\ ((reach[u,v] = 1) -> ({u,v} in G))
  /\ (((reach[u,v] > 1) \/ (reach[u,v] < n)) ->
      (exists w : vertices . ({u,w} in G) /\ (reach[w,v] = reach[u,v] - 1)))
  /\ ((reach[u,v] = n) -> (forAll w : vertices . !({u,w} in G) \/ (reach[w,v] = n)))
find connected : bool
such that
  connected = (forAll u,v : vertices . reach[u,v] < n)

This is stored in file gc1.essence. The values of n and G will be specified later as parameters, such as via the path-4.param or disconnected-4.param files.

In the model, first the matrix reach is specified by imposing the four conditions that we mentioned. Finally a Boolean variable connected is used to conveniently indicate whether the reach matrix represents a connected graph or not; in a connected graph every vertex is reachable from every other vertex.

Let’s now try this model with the two graphs defined so far.

conjure solve -ac gc1.essence path-4.param
conjure solve -ac gc1.essence disconnected-4.param

In the solutions found by Conjure, the matrix reach indicates the distances between each pair of vertices. In the solution for the connected graph gc1-path-4.solution all entries are at most 3.

letting connected be true
letting reach be
  [[0, 1, 2, 3; int(1..4)], [1, 0, 1, 2; int(1..4)],
   [2, 1, 0, 1; int(1..4)], [3, 2, 1, 0; int(1..4)]; int(1..4)]
$ Visualisation for reach
$ 0 1 2 3
$ 1 0 1 2
$ 2 1 0 1
$ 3 2 1 0

In contrast, in the solution for the disconnected graph gc1-disconnected-4.solution there are some entries that are 4:

letting connected be false
letting reach be
  [[0, 1, 4, 4; int(1..4)], [1, 0, 4, 4; int(1..4)],
   [4, 4, 0, 1; int(1..4)], [4, 4, 1, 0; int(1..4)]; int(1..4)]
$ Visualisation for reach
$ 0 1 4 4
$ 1 0 4 4
$ 4 4 0 1
$ 4 4 1 0

Graphs with four vertices are good for quick testing but are too small to notice much difference between models. Small differences are important for tasks such as enumerating many objects, when even a small difference is multiplied by the number of objects. For testing we can create other parameter files containing graphs with more vertices. Notice that we do not have to change the model, only the parameter files containing the input data.

Testing with larger graphs of say 1000 vertices, it becomes clear that this first model works but does not scale well. It computes the lengths of the shortest paths between pairs of vertices, from which we can deduce whether the graph is connected. This is quite round-about! We can now try to improve the model by asking the system to do less work. After all, we don’t actually need all the pairwise distances.

Model 2: reachability matrix

In the following model, stored as file gc2.essence, the reachability matrix uses Boolean values for the distances rather than integers, with true representing reachable and false unreachable. Each entry reach[u,v] represents whether it is possible to reach v by some path that starts at u. This is modelled as the disjunction of three conditions: u is reachable from itself, any neighbour of u is reachable from it, and if v is not a neighbour of u then there should be a neighbour w of u so that v is reachable from w.

given n : int(1..)
letting vertices be domain int(1..n)
given G : set of set (size 2) of vertices
find reach : matrix indexed by [vertices, vertices] of bool
such that
  forAll u,v : vertices . reach[u,v] =
    ((u = v) \/ ({u,v} in G) \/
    (exists w : vertices . ({u,w} in G) /\ reach[w,v]))
find connected : bool
such that
  connected = (forAll u,v : vertices . reach[u,v])

In the solutions found by Conjure, the reachability matrix contains regions of true entries indicating the connected components.

In the connected graph all entries are true:

letting connected be true
letting reach be
  [[true, true, true, true; int(1..4)], [true, true, true, true; int(1..4)],
   [true, true, true, true; int(1..4)], [true, true, true, true; int(1..4)];
   int(1..4)]
$ Visualisation for reach
$ T T T T
$ T T T T
$ T T T T
$ T T T T

In contrast, in the disconnected graph there are some false entries:

letting connected be false
letting reach be
  [[true, true, false, false; int(1..4)], [true, true, false, false; int(1..4)],
   [false, false, true, true; int(1..4)], [false, false, true, true; int(1..4)];
   int(1..4)]
$ Visualisation for reach
$ T T _ _
$ T T _ _
$ _ _ T T
$ _ _ T T

This model takes about half as long as the previous one, but is still rather slow for large graphs. Moreover, this model fails to capture all the constraints: it will always allow the all-true reachability matrix as one solution, and so it will potentially always consider every graph to be connected. The reader is encouraged to think about this flaw in the model.

Model 3: structured reachability matrices

In the previous two models the solver may spend a long time early in the search process looking for ways to reach vertices that are far away, even though it would be more efficient to focus the early stages of search on vertices close by. It is possible to improve performance by guiding the search to consider nearby vertices before vertices that are far from each other. The following model gc3.essence uses additional decision variables to more precisely control how the desired reachability matrix should be computed. There are multiple reachability matrices. Each corresponds to a specific maximum distance. The first n by n matrix reach[0] expresses reachability in one step, and is simply the adjacency matrix of the graph. The entry reach[k,u,v] expresses whether v is reachable from u via a path of length at most 2**k. If a vertex v is reachable from some vertex u, then it can be reached in at most n-1 steps. (Note: in this model a vertex cannot reach itself in zero steps, so a graph with a single vertex is not regarded as connected.)

given n : int(1..)
letting vertices be domain int(1..n)
given G : set of set (size 2) of vertices
letting m be sum([1 | i : int(0..64), 2**i <= n])
find reach : matrix indexed by [int(0..m), vertices, vertices] of bool
such that
  forAll u,v : vertices . reach[0,u,v] = ({u,v} in G),
  forAll i : int(0..(m-1)) . forAll u,v : vertices . reach[i+1,u,v] =
    (reach[i,u,v] \/ (exists w : vertices . (reach[i,u,w] /\ reach[i,w,v]))),
find connected : bool
such that
  connected = (forAll u,v : vertices . reach[m,u,v])

The variable m is used to compute the number of matrices that are required; this is the smallest integer that is not less than the base-2 logarithm of n. (This is computed by discrete integration as Essence currently does not have a logarithm operator.) The value of connected is then based on whether whether reach[m] contains any false entries.

This model performs well for small graphs, but it generates intermediate distance matrices, each containing n**2 variables. For large graphs the number of intermediate variables used to represent these intermediate distance matrices grows quickly, which causes Savile Row to run out of memory. We omit the solutions here. The sequence of solutions shows how the number of true values in the reachability matrices increases, until reaching a fixed point.

Model 4: connected component

Each of the three models so far deals with all possible pairs of vertices. The number of possible pairs of vertices is quadratic in the number of vertices. However, many graphs are sparse, with a number of edges that is bounded by a linear function of the number of vertices. For sparse graphs, and especially those with many vertices, it is therefore important to only consider the edges that are present rather than all possible pairs of vertices. The next model gc4.essence uses this insight, and is indeed faster than any of the three previous ones.

The model builds on the fact that a graph is disconnected if, and only if, its vertices can be partitioned into two sets, with no edges between vertices in the two different sets. Here C is used to indicate a subset of the vertices. There are three constraints. The first is that C must contain some vertex. The second is that C must be a connected component; each vertex in C is connected to some other vertex in C (unless C only contains a single vertex). The third is that the value of connected is determined by whether it is possible to find some vertex that is not in C. The following is an attempt to capture these constraints in an Essence specification.

given n : int(1..)
letting vertices be domain int(1..n)
given G : set of set (size 2) of vertices
find C : set of vertices
find connected : bool
such that
  exists u : vertices . u in C,
  forAll e in G . (min(e) in C) = (max(e) in C),
  connected = !(exists u : vertices . !(u in C))

This is the solution for disconnected-4.param:

letting C be {1, 2}
letting connected be false

Model gc4.essence yields a solution quickly. Unfortunately, like Model 2 above, it can also give incorrect results: letting C be the set of all vertices and letting connected be true is always a solution, whether the graph is connected or not. This can be confirmed by asking Conjure to generate all solutions:

conjure solve -ac --number-of-solutions=all gc4.essence

This gives two solutions, the one above and the following one:

letting C be {1, 2, 3, 4}
letting connected be true

It is actually possible to ensure that this “solution” is never the first one generated, and then to ask Conjure to only look for the first solution; if the graph is not connected then the first solution will correctly indicate its status. However, this relies on precise knowledge of the ordering heuristics being employed at each stage of the toolchain.

The problem with this fourth specification is that it only captures the property that C is a union of connected components. We would need to add additional constraints to enforce the property that C should contain only one connected component. This can be done, but is not especially efficent.

For the mathematically minded, the problem is that connectivity is not expressible in monadic existential second order logic, forcing us to express the problem differently, such as in non-monadic existential or monadic universal second order logic, or in first-order logic with fixed points. The first two approaches tend to increase the search effort, while Essence lacks fixed point operators so we can’t use the third approach.

Model 5: minimal connected component

Let’s look for a robust approach that won’t unexpectedly fail if parts of the toolchain change which optimisations they perform or the order in which evaluations occur.

One option could be to look for solutions of a more restrictive model which includes an additional constraint that requires some vertex to not be in C. This model would have a solution precisely if the graph is not connected. Failure to find solutions to this model would then indicate connectivity. It is possible to call Conjure from a script that uses the failure to find solutions to conclude connectivity, but the Conjure toolchain currently does not support testing for the presence of solutions directly.

In place of such an “if-has-solution” directive (which is not currently supported), we could instead quantify over all possible subsets of vertices. Such an approach quickly becomes infeasible as n grows (and is much worse than the models considered so far), because it attempts to check 2**n subsets.

As another option, we can make use of the optimisation features of Essence to find a solution with a C of minimal cardinality. This ensures that C can only contain one connected component. Choosing a minimal C ensures that when there is more than one solution, then the one that is generated always indicates the failure of connectivity. Since we don’t care about the minimal C, as long as it is smaller than the set of all vertices if possible, we also replace the general requirement for non-emptiness by a constraint that always forces the set C to contain the vertex labelled 1.

given n : int(1..)
letting vertices be domain int(1..n)
given G : set of set (size 2) of vertices
find C : set of vertices
find connected : bool
such that
  1 in C,
  forAll e in G . (min(e) in C) = (max(e) in C)
minimising |C|

This model gc5.essence is still straightforward, even with the additional complication to rule out incorrect solutions. Out of the correct models so far, this tends to generate the smallest input files for the back-end constraint or SAT solver, and also tends to be the fastest. Moreover, it scales to large sparse graphs as it avoids quadratic growth in the number of intermediate variables.

Generating all connected graphs

We now have a fast model for graph connectivity. Let’s modify it as gce1.essence, hardcoding n to be 4 and asking the solver to find G as well as C.

letting n be 4
letting vertices be domain int(1..n)
find G : set of set (size 2) of vertices
find C : set of vertices
such that
  1 in C,
  forAll e in G . (min(e) in C) = (max(e) in C)
minimising |C|

We now ask for all solutions:

conjure solve -ac --number-of-solutions=all gce1.essence

However, this finds only one solution!

The solver finds one solution that minimises |C|; this minimisation is performed globally over all possible solutions. This is what we intended when G was given, but is not what we want if our goal is to generate all connected graphs. We want to minimise C for each choice of G, producing one solution for each G. There is no way to tell Conjure that minimisation should be restricted to the decision variable C.

Checking whether there is a nontrivial connected component seems to be the most efficient model for graph connectivity, but it doesn’t work in the setting of generating all connected graphs. We therefore need to choose one of the other models to start with, say the iterated adjacency matrix representation.

We now use this model of connectivity to enumerate the labelled connected graphs over the vertices {1,2,3,4}. Previously we checked connectivity of a given graph G. We now instead ask the solver to find G, specifying that it be connected. We do this by asking for the same adjacency matrix reach as before, but in addition asking for the graph G. We also hardcode n, so no parameter file is needed, and add the condition that previously determined the value of the connected decision variable as a constraint.

letting n be 4
letting vertices be domain int(1..n)
find G : set of set (size 2) of vertices
letting m be sum([1 | i : int(0..64), 2**i <= n])
find reach : matrix indexed by [int(0..m), vertices, vertices] of bool
such that
  forAll u,v : vertices . reach[0,u,v] = ({u,v} in G),
  forAll i : int(0..(m-1)) . forAll u,v : vertices . reach[i+1,u,v] =
    (reach[i,u,v] \/ (exists w : vertices . (reach[i,u,w] /\ reach[i,w,v]))),
  forAll u,v : vertices . reach[m,u,v]

If this model is in the file gce2.essence, then we now need to explicitly ask Conjure to generate all the possible graphs:

conjure solve -ac --number-of-solutions=all gce2.essence

In this case Conjure generates 38 solutions, one solution per file.

Instead of listing the edges of a graph, and then deriving the adjacency matrix as necessary, it is also possible to use the adjacency matrix representation. As an exercise, modify the models of connectivity to use the adjacency matrix representation instead of the set of edges representation.

Futoshiki

Authors: Ruth Hoffmann and Gökberk Koçak

Problem

n x n board where each column and row is filled with the unique numbers from 1 to n, similar to a sudoku. In contrast to sudoku, there are less than and greater than symbols between cells indicating that one cell has to be filled with a number greater than (or less than) than the cell on the other side of the operator.

Essence Model

Let us look at the model first.

language Essence 1.3
given n : int
letting DOMAIN be domain int(1..n)
given hints : function (DOMAIN, DOMAIN) --> DOMAIN
given less_than : relation of ((DOMAIN, DOMAIN) * (DOMAIN, DOMAIN))
find board : matrix indexed by [DOMAIN, DOMAIN] of DOMAIN
such that
    forAll (hint,num) in hints .
        board[hint[1], hint[2]] = num,
    forAll i: DOMAIN .
        allDiff(board[i,..]),
    forAll j: DOMAIN .
        allDiff(board[..,j]),
    forAll (l,g) in less_than .
        board[l[1],l[2]] < board[g[1],g[2]]

The line by line explanation starts here.

given n : int

Defines the size of the matrix and the maximal number of elements that we will add.

letting DOMAIN be domain int(1..n)

We start at 1 and go up to n (for both the elements of the cells and the cell locations).

given hints : function (DOMAIN, DOMAIN) --> DOMAIN

Here we define which cells are already filled in using a function. We map the coordinates onto the number that is in that cell. It is important to notice that functions in essence are partial functions not total. This means that not everything gets mapped.

given less_than : relation of ((DOMAIN, DOMAIN) * (DOMAIN, DOMAIN))

Here we define where the relation symbols are placed, it depends on which way you read the symbol we are “only” modelling less than. So should there be a “greater than” signs between two cells, say (2,1) and (1,1) then we would order them as (1,1) is less than (2,1).

find board : matrix indexed by [DOMAIN, DOMAIN] of DOMAIN

We are now telling the solver that we are trying to find a n x n board with elements from 1 to n in each cell.

such that

This is the beginning of the constraints block.

forAll (hint,num) in hints .
   board[hint[1], hint[2]] = num,

This constraint defines the hints, so the cells that are filled in when we get the puzzle.

forAll i: DOMAIN .
    allDiff(board[i,..]),

This constraint defines that every cell in a row has to be a unique number between 1 and n.

forAll j: DOMAIN .
    allDiff(board[..,j]),

This constraint defines that every cell in a column has to be a unique number between 1 and n.

forAll (l,g) in less_than .
    board[l[1],l[2]] < board[g[1],g[2]]

Finally this constraint enforces the less than relation. l is the number that is the cell that contains the number that is less than then the cell g.

Instance

We save the instance in a .essence-param file.

letting n be 4
letting hints be function(
        (1,1) --> 2,
        (2,2) --> 2
)
letting less_than be relation(
        ((1,1) , (2,1)),
        ((4,2) , (3,2)),
        ((3,3) , (3,4)),
        ((3,4) , (4,4))
)

The .essence-param file contains the information about our starting board of a specific instance that we want to solve. See the picture at the beginning to see what it looks like.

letting n be 4

We are dealing with a 4 by 4 board.

letting hints be function(
        (1,1) --> 2,
        (2,2) --> 2
)

There will be two 2 s on the board given as a hint. One in the top left corner (1,1) and the second number 2 in cell (2,2).

letting less_than be relation(
        ((1,1) , (2,1)),
        ((4,2) , (3,2)),
        ((3,3) , (3,4)),
        ((3,4) , (4,4))
)

There are 4 relation symbols on the board, between cells.

Solving

Using the ESSENCE pipeline, we can solve our sample instance by typing the following:

conjure solve futoshiki-model.essence futoshiki-instance.essence-param

The result will be saved into a .solution file which will look something like this:

letting board be
        [[2, 1, 4, 3; int(1..4)], [4, 2, 3, 1; int(1..4)], [3, 4, 1, 2; int(1..4)], [1, 3, 2, 4; int(1..4)]; int(1..4)]
$ Visualisation for board
$ 2 1 4 3
$ 4 2 3 1
$ 3 4 1 2
$ 1 3 2 4

BIBD

Authors: Chris Jefferson and Alice Lynch

This tutorial discusses a classic constraint problem and introduces the use of quantifiers in Essence.

The Problem

Balanced Incomplete Block Design (BIBD) is a problem from the field of experimental design. It is best explained with an example.

Emily wants to establish which crops (🥔, 🌽, 🥦, 🥕, 🥒, 🍅) grow best in Scotland. She has recruited 4 farmers who are happy to help by growing some of the crops. Unfortunately none of the farmers have enough space to grow every crop, they can each grow 3 different crops. Emily is concerned that the different environment of each farm may impact the crops growth. Therefore she wants to make sure that each farmer grows a different combination of crops and that every crop has been grown in the same number of different farms. This approach is called Balanced Incomplete Block Design (BIBD).

We can build a model to tell us the crops that each farm should grow.

The Model

We need to specify the crops, the number of farms, the number of crops that can be grown per farm, the number of different farms that will grow each crop and the number of crops each pair of farmers has in common.

Emily has decided that she wants each crop to be grown in 2 different farms, and that each pair of farmers will have 1 crop in common.

Essence will take a .param file containing the values of the initial parameters. In the .param file we should define the parameters:

letting crops be new type enum {🥔, 🌽, 🥦, 🥕, 🥒, 🍅}
letting farms be 4
letting crops_per_farm be 3
letting farms_per_crop be 2
letting overlap be 1

The model will be in a .essence file. It should start by accessing the provided parameters, this uses the given keyword, followed by the names of the parameters and their type.

given farms, crops_per_farm, farms_per_crop, overlap: int
given crops new type enum

Next, we need to define what we are looking for. The find keyword indicates that the solver should find a value for that variable. We want to find a set containing sets of crops. Each set of crops is a crop assignment for a farm.

given farms, crops_per_farm, farms_per_crop, overlap: int
given crops new type enum

find crop_assignment: set of set of crops

Once the parameters and decision variables of the model have been defined, we should define the constraints. such that indicates the start of the constraints.

given farms, crops_per_farm, farms_per_crop, overlap: int
given crops new type enum

find crop_assignment: set of set of crops

such that

Result:

{}

With no constraints it produces an empty set for crop assignment.

The first, basic, constraint is the number of farms. The number of sets in the crop_assignment set should equal the number of farms. |crop_assignment| indicates the size of the crop_assignment set. By setting the size equal to the number of farms (after the such that keyword) the solver will only produce solutions where the size of the set is the same as the number of farms. A comma separates constraints, so at the end of a line this indicates that there are more constraints to follow (none for the moment).

given farms, crops_per_farm, farms_per_crop, overlap: int
given crops new type enum

find crop_assignment: set of set of crops

such that

|crop_assignment| = farms,

Result:

{{},
 {🥒},
 {🥒, 🍅},
 {🍅}}

The model now produces four ‘farms’ but the number of crops assigned to each are not suitable.

Next we want to apply the number of crops per farm constraint to every set in the crop assignment set. The forAll keyword will apply the constraint (|farm| = crops_per_farm) across every element in the crop_assignment set (represented by farm). The . separates the constraint from the quantifier setup.

given farms, crops_per_farm, farms_per_crop, overlap: int
given crops new type enum

find crop_assignment: set of set of crops

such that

|crop_assignment| = farms,
forAll farm in crop_assignment . |farm| = crops_per_farm,

Result:

{{🥦, 🥕, 🥒},
 {🥦, 🥕, 🍅},
 {🥦, 🥒, 🍅},
 {🥕, 🥒, 🍅}}

The model now has the correct number of farms and assigns the correct number of crops per farm, but doesn’t assign all types of crops.

The next constraint is number of farms with a given crop. This is more complex than the previous constraints. Let’s go over it step by step. For every crop we need to find the number of farms assigned that crop and set it to equal the parameter Emily chose for farms per crop. In order to find this we first use a forAll to apply the constraint to every crop. forAll crop : crops . [OurCalculation] = farms_per_crop

Then we need to count every farm that is planting that crop. For this we should use the sum quantifier rather than the forAll (sum farm in crop_assignment . [Action]). sum will add together all the results of the chosen action. In order to use sum to count the number of farms that contain a crop we need to return 1 if the farm is planting the crop and 0 otherwise. The in keyword can be used to check if a crop is present in a farm, the resulting boolean can be converted to 1 or 0 using toInt.

given farms, crops_per_farm, farms_per_crop, overlap: int
given crops new type enum

find crop_assignment: set of set of crops

such that

|crop_assignment| = farms,
forAll farm in crop_assignment . |farm| = crops_per_farm,
forAll crop : crops . (sum farm in crop_assignment . toInt(crop in farm)) = farms_per_crop,

Result:

{{🥔, 🥕, 🍅},
 {🥔, 🥒, 🍅},
 {🌽, 🥦, 🥕},
 {🌽, 🥦, 🥒}}

Our model now produces a crop assignment that assigns the correct number of crops to each farmer and the correct number of crops in total but there is lot of overlap between the first and second farmer and between the third and fourth farmer but very little overlap between the two pairs. This is why Emily specified the overlap constraint (sometimes called lambda in BIBD models). In order to make sure that every pair of farmers have at least 1 crop in common we need to define another constraint.

We need to check every pair of farms, we can do this by using two forAll keywords (forAll farm1 in crop_assignment. forAll farm2 in crop_assignment . [OurConstraint]). We can then use the intersect keyword to get all crops that the two farms have in common, and require the size of this intersection to be equal to the overlap parameter (|farm1 intersect farm2| = overlap).

However, running the model at this point produces no solutions, as iterating over the crop_assignment in this way means that sometimes farm1 and farm2 will be the same farm, so the intersection will be the number of crops assigned to the farm (3) and never be 1 (the overlap parameter), resulting in no valid solutions.

In order to avoid this we need to add a further condition to the constraint which checks they are not the same farm before applying the constraint. -> is used, where the left hand side has a condition and the right hand side has a constraint which is only used if the left hand side is true. farm1 != farm2 -> |farm1 intersect farm2| = overlap

given farms, crops_per_farm, farms_per_crop, overlap: int
given crops new type enum

find crop_assignment: set of set of crops

such that

|crop_assignment| = farms,
forAll farm in crop_assignment . |farm| = crops_per_farm,
forAll crop : crops . (sum farm in crop_assignment . toInt(crop in farm)) = farms_per_crop,
forAll farm1 in crop_assignment. forAll farm2 in crop_assignment . farm1 != farm2 -> |farm1 intersect farm2| = overlap

Result:

{{🥔, 🥦, 🍅},
 {🥔, 🥕, 🥒},
 {🌽, 🥦, 🥒},
 {🌽, 🥕, 🍅}}

This model produces a valid solution!

Improvements

Our model now works and produces a correct solution but the code could be improved in places.

There is a nicer way to do the final constraint, instead of using a second forAll we can use {farm1, farm2} and subsetEq to generate all pairs that can be made up from a given set.

given farms, crops_per_farm, farms_per_crop, overlap: int
given crops new type enum

find crop_assignment: set of set of crops

such that

|crop_assignment| = farms,
forAll farm in crop_assignment . |farm| = crops_per_farm,
forAll crop : crops . (sum farm in crop_assignment . toInt(crop in farm)) = farms_per_crop,
forAll {farm1, farm2} subsetEq crop_assignment . |farm1 intersect farm2| = overlap

Providing information in the find statements rather than as constraints often leads to better performance. Essence provides domain attributes which can be attached to find statements . One of them is size k, which tells Essence that a set is of size k. In our model the number of farms and the number of crops per farm are in effect the size of the crop_assignment set and the size of the sets within the crop_assignment set. Therefore we can move these definitions out of the list of constraints and into the find statement.

given farms, crops_per_farm, farms_per_crop, overlap: int
given crops new type enum

find crop_assignment: set (size farms) of set (size crops_per_farm) of crops

such that
forAll crop : crops . (sum farm in crop_assignment . toInt(crop in farm)) = farms_per_crop,
forAll {farm1, farm2} subsetEq crop_assignment . |farm1 intersect farm2| = overlap

Semigroups, Monoids and Groups

Authors: Chris Jefferson and Alice Lynch

This tutorial discusses how to model semigroups, monoids and groups in Essence.

The Problem

Semigroups, monoids and groups are all examples of binary operations, with added conditions.

We will begin by building a binary operation. A binary relation R on a domain S is a two-argument function which maps two elements of S to a third element of S. We will make S be the integers from 1 to n, for some given n.

given n : int
letting S be domain int(1..n)

find R : function(total) (S,S) --> S

We make a new type of size n to represent the set the operation is defined on. We then define a function from (S,S) to S. Technically, this function doesn’t take two arguments - it takes a single argument which is a pair of values from S. This is mathematically the same, but will change how we use R.

We will begin by creating a solution to this, for n = 4.

Result:

letting R be
      function((1, 1) --> 1, (1, 2) --> 1, (1, 3) --> 1, (1, 4) --> 1,
               (2, 1) --> 1, (2, 2) --> 1, (2, 3) --> 1, (2, 4) --> 1,
               (3, 1) --> 1, (3, 2) --> 1, (3, 3) --> 1, (3, 4) --> 1,
               (4, 1) --> 1, (4, 2) --> 1, (4, 3) --> 1, (4, 4) --> 1)

At the moment this is quite boring, as the function can take any value at all! Asking Conjure how many solutions this problem has is unreasonable, but we can figure it out with maths: $$4^{16} = 4,294,967,296$$. Let’s try adding some constraints.

Semigroups

The simplest object we will consider is a semigroup. A semigroup adds one constraint to our binary operation, associativity. A binary operation is associative if for all i,j and k in S, R(i,R(j,k)) = R((R(i,j),k). This might look very abstract, but it is true of many binary operations, for example given integers i,j and k, (i+j)+k = i+(j+k), and (i * j) * k = i * (j * k).

We begin by saying we want to check forAll i,j,k: S. The strangest bit is all of the brackets seem doubled. Your vision isn’t failing, this is because M is a one argument function (and we use M(x) to apply M to x), but M takes a tuple as its argument (which we write as (i,j)), so to apply M to i and j we write M((i,j)).

given n : int
letting S be domain int(1..n)

find R : function(total) (S,S) --> S

such that

forAll i,j,k: S. R((i,R((j,k)))) = R((R((i,j)),k))

Result:

letting R be
      function((1, 1) --> 1, (1, 2) --> 1, (1, 3) --> 1, (1, 4) --> 1,
               (2, 1) --> 1, (2, 2) --> 1, (2, 3) --> 1, (2, 4) --> 1,
               (3, 1) --> 1, (3, 2) --> 1, (3, 3) --> 1, (3, 4) --> 1,
               (4, 1) --> 1, (4, 2) --> 1, (4, 3) --> 1, (4, 4) --> 1)

The first result is still the same, but there are fewer solutions to be found now - only 3,492. Is this correct? It’s always good to check. This number was first published in 1955, by George E. Forsythe, in his paper “SWAC Computes 126 Distinct Semigroups of Order 4”. Where does the number 126 come from? This small number comes from ignoring cases where the semigroup is the same except for rearranging the numbers 1,2,3,4. The number we found, 3,492, is found in the paper.

Monoids

Let’s move further to monoids. A monoid is a semigroup with an extra condition, there has to exist some element of the semigroup, which we will call e, which acts as an identity. An identity is an element such that for all i in S, R(e,i) = R(i,e) = e.

Firstly we will add a variable to store the value of this e, and then add the extra constraint which makes it an identity:

given n : int

letting S be domain int(1..n)

find R : function (total) (S,S) --> S

find e : S

such that

forAll i,j,k: S. R((i,R((j,k)))) = R((R((i,j)),k)),
forAll i : S. M((e,i)) = i /\ M((i,e)) = i,

Result:

letting R be
      function((1, 1) --> 1, (1, 2) --> 1, (1, 3) --> 1, (1, 4) --> 1,
               (2, 1) --> 1, (2, 2) --> 1, (2, 3) --> 1, (2, 4) --> 2,
               (3, 1) --> 1, (3, 2) --> 1, (3, 3) --> 1, (3, 4) --> 3,
               (4, 1) --> 1, (4, 2) --> 2, (4, 3) --> 3, (4, 4) --> 4)
letting e be 4

We now have only 624 solutions! We can check this by looking at the amazing online encyclopedia of integer sequences https://oeis.org/A058153 , which tells us there are indeed 624 “labelled monoids” of order n.

Groups

Finally, let us move to groups. Groups add one important requirement, the concept of an inverse. Given some i in S, j is an inverse of i if R((i,j)) = R((j,i)) = e, where e is our already existing identity.

We will store the inverses as an extra array, and then add this final constraint:

given n : int

letting S be domain int(1..n)

find R : function (total) (S,S) --> S

find e : S

find inv: function S --> S

such that

forAll i,j,k: S. R((i,R((j,k)))) = R((R((i,j)),k)),
forAll i : S. R((e,i)) = i /\ R((i,e)) = i,

forAll i : S. R((i,inv(i))) = e /\ R((inv(i),i)) = e

Result:

letting R be
      function((1, 1) --> 1, (1, 2) --> 2, (1, 3) --> 3, (1, 4) --> 4,
               (2, 1) --> 2, (2, 2) --> 1, (2, 3) --> 4, (2, 4) --> 3,
               (3, 1) --> 3, (3, 2) --> 4, (3, 3) --> 1, (3, 4) --> 2,
               (4, 1) --> 4, (4, 2) --> 3, (4, 3) --> 2, (4, 4) --> 1)
letting e be 4
letting inv be function(1 --> 1, 2 --> 2, 3 --> 3, 4 --> 4)

This solution has much more going on than our previous ones! For example, each row and column contains the numbers from 1 to 4, in some order. This (and many, many other results) are true for all groups (but we won’t prove this here!). This problem only has 16 solutions, and once we removed the groups which are made by just swapping around 1,2,3 and 4, we would find there was only 2 groups! The extra structure means there are only a small number of groups for each size, compared to the number of semigroups and monoids.

There are many special types of groups; we will consider just one here, abelian groups. A group is abelian if for all i and j in S, R((i,j)) = R((j,i)). Let’s add this condition!

given n : int

letting S be domain int(1..n)

find R : function (total) (S,S) --> S

find e : S

find inv: function S --> S

such that

forAll i,j,k: S. R((i,R((j,k)))) = R((R((i,j)),k)),
forAll i : S. R((e,i)) = i /\ R((i,e)) = i,
forAll i : S. R((i,inv(i))) = e /\ R((inv(i),i)) = e,
forAll i,j : S. R((i,j)) = R((j,i))

Result:

letting R be
      function((1, 1) --> 1, (1, 2) --> 2, (1, 3) --> 3, (1, 4) --> 4,
               (2, 1) --> 2, (2, 2) --> 1, (2, 3) --> 4, (2, 4) --> 3,
               (3, 1) --> 3, (3, 2) --> 4, (3, 3) --> 1, (3, 4) --> 2,
               (4, 1) --> 4, (4, 2) --> 3, (4, 3) --> 2, (4, 4) --> 1)
letting e be 4
letting inv be function(1 --> 1, 2 --> 2, 3 --> 3, 4 --> 4)

This gives us the same first solution. In fact, there is the same number of solutions (16) to this problem as the previous one, proving that all groups of size 4 are abelian! In fact, the smallest non-abelian group is size 60, and that is beyond the size of problems we can find all solutions to with our current, simple model.

Handcrafting Instance Generators in Essence

Authors: Joan Espasa Arxer and Christopher Stone

In modelling it is common to create an abstract model that expects some input parameters (Also known as “instances”) which are required to run and test the model. In this tutorial we demonstrate how to use ESSENCE to handcraft a generator of instances that can be used to produce input parameters for a specific model.

Instances for the Knapsack problem

Here is the model of the Knapsack Problem from (<link to other tutorial>) - knapsack.essence

given number_items : int
letting items be domain int (1..number_items)
given weight, gain : function (total) items --> int
given capacity : int
find picked : set of items
maximising sum i in picked . gain(i)
    such that (sum i in picked . weight(i)) <= capacity

This model has 4 different “given” statements :

• number_items: an integer for number of items

• weight: a functions that associates an integer(weight) to each item

• gain: a function that associates an integer(gain) to each item

• capacity: an integer that defines the capacity of the knapsack

The first parameter is fairly simple and we can even write this parameter with some value by hand by writing on a separate file (which we will call items.param):

letting number_items be 20

The remaining 3 parameters are more complex and labourious to be defined (too much work to be done by hand!) so we are going to write an ESSENCE specification that will create them for us. The fundamental starting step is writing find statements for each variable we wish to generate and ensure that the names of the variable (identifiers) are left unchanged. We can do so by creating a new file called generator.essence and write:

given number_items : int
letting items be domain int(1..number_items)
find weight: function (total) items --> int(1..1000)
find gain: function (total) items --> int(1..1000)
find capacity: int(1..5000)

Solving the above model (by running ‘conjure solve generator.essence items.param’ on the console) will create a set of parameters for our knapsack model. However, these instances are not interesting enough yet.

language Essence 1.3
letting capacity be 1
letting gain be
        function(1 --> 1, 2 --> 1, 3 --> 1, 4 --> 1, 5 --> 1, 6 --> 1, 7 --> 1, 8 --> 1, 9 --> 1, 10 --> 1, 11 --> 1,
                 12 --> 1, 13 --> 1, 14 --> 1, 15 --> 1, 16 --> 1, 17 --> 1, 18 --> 1, 19 --> 1, 20 --> 1)
letting weight be
        function(1 --> 1, 2 --> 1, 3 --> 1, 4 --> 1, 5 --> 1, 6 --> 1, 7 --> 1, 8 --> 1, 9 --> 1, 10 --> 1, 11 --> 1,
                 12 --> 1, 13 --> 1, 14 --> 1, 15 --> 1, 16 --> 1, 17 --> 1, 18 --> 1, 19 --> 1, 20 --> 1)

We can make our instances more interesting by adding constraints into our generator’s model. The first thing we notice is that all values assigned are identical, a bit TOO symmetrical for our taste. One simple solution to this issue is ensuring that all weights and gains assignments are associated with distinct values. This can be done by imposing injectivity as a property of the function.

find weight: function (total, injective) items --> int(1..1000)
find gain: function (total, injective) items --> int(1..1000)

And the results would be

language Essence 1.3
letting capacity be 1
letting gain be
        function(1 --> 1, 2 --> 2, 3 --> 3, 4 --> 4, 5 --> 5, 6 --> 6, 7 --> 7, 8 --> 8, 9 --> 9, 10 --> 10, 11 --> 11,
                 12 --> 12, 13 --> 13, 14 --> 14, 15 --> 15, 16 --> 16, 17 --> 17, 18 --> 18, 19 --> 19, 20 --> 20)
letting weight be
        function(1 --> 1, 2 --> 2, 3 --> 3, 4 --> 4, 5 --> 5, 6 --> 6, 7 --> 7, 8 --> 8, 9 --> 9, 10 --> 10, 11 --> 11,
                 12 --> 12, 13 --> 13, 14 --> 14, 15 --> 15, 16 --> 16, 17 --> 17, 18 --> 18, 19 --> 19, 20 --> 20)

This gives us a slighly more interesting parameters set but it is not there yet The specific order that appears in the results is solver dependent. The default solver used by conjure is Minion and we can use an optional flag to have the variables assigned in a random order. This can be done with this command:

conjure solve generator.essence items.param --solver-options=-randomiseorder

Alternatively one can use another solver that uses randomness by default

language Essence 1.3
letting capacity be 2841
letting gain be
        function(1 --> 858, 2 --> 653, 3 --> 673, 4 --> 365, 5 --> 389, 6 --> 783, 7 --> 566, 8 --> 664, 9 --> 387,
                 10 --> 576, 11 --> 864, 12 --> 741, 13 --> 102, 14 --> 735, 15 --> 276, 16 --> 41, 17 --> 132,
                 18 --> 974, 19 --> 293, 20 --> 381)
letting weight be
        function(1 --> 946, 2 --> 435, 3 --> 796, 4 --> 653, 5 --> 291, 6 --> 101, 7 --> 924, 8 --> 988, 9 --> 854,
                 10 --> 952, 11 --> 228, 12 --> 189, 13 --> 88, 14 --> 270, 15 --> 868, 16 --> 903, 17 --> 743,
                 18 --> 396, 19 --> 174, 20 --> 446)

Now it is starting to look more like a proper instance. At this point we can add some knowledge about the problem to formulate some constraints that will ensure that the instances are not trivial. ie when the sum of all the weights is smaller than the capacity so we can’t put all the objects in the knapsack or when all the objects are heavier than the capacity so that no object can be picked. Thefore we add constraints such as:

such that (sum ([w | (_,w) <- weight]) > capacity*2)

This means that the sum of all the weights should be greater than twice the capacity of the knapsack. From this we can expect that on average no more than half of the objects will fit in the knapsack. The expression [w | (_,w) <- weight] is a list comprehension that extracts all right hand values of the weight function. The underscore character means we do not care about the left hand side values. To ensure that the solver does not take it too far we impose an upper bound using a similar constraint. We impose that the sum of the objects weights 5 times the capacity of the knapsack, so we can expect that only between 20% and 50% of the items will fit in the knapsack in each instance.

such that (sum ([w | (_,w) <- weight]) < capacity*5)

At this point it will be harder to see specific properties of the instances just by eyeballing the parameters but we can be confident that the properties we have imposed are there. We can add some more constraints to refine the values of the instances for practice/exercise by enforcing that no object is heavier than a third of the knapsack capacity

such that forAll (_,w) in weight .  w < capacity / 3

On top of that we can enfore a constraint on the density of the values in each object by limiting the ratio between the weight and gain of each specific object with:

such that forAll element : items .
        gain(element) <= 3*weight(element)

Finally the model of the generator is now :

given number_items : int
letting items be domain int(1..number_items)

find weight: function (total, injective) items --> int(1..1000)
find gain: function (total, injective) items --> int(1..1000)
find capacity: int(1..5000)
such that (sum ([w | (_,w) <- weight]) > capacity*2)
such that (sum ([w | (_,w) <- weight]) < capacity*3)
such that forAll (_,w) in weight .  w < capacity / 3
such that forAll element : items .
            gain(element) <= 3*weight(element)

After running once again the solver we can take the output solution file generator-items.solution and append it to the items.param (by concatenating the files or simply coping the content into it) We can finally test our instance by running “conjure solve knapsack.essence items.param”

Tada! your model is being tested on some instance!

If your computer is powerful enough you can try larger values in “letting number_items be 20” (40-50 items will already produce substantially harder instances) Like for other forms of modelling writing instance generators is in large part an art. If this is not your kind of thing and you would like a fully automated system that can produce instances you may check out this method [ code available here ]

Simple Permutations

Authors: Ruth Hoffmann and Gökberk Koçak, edited by András Salamon

Problem

Let a permutation be a sequence of length \(n\) consisting of numbers between 1 and \(n\), in any order with each number occurring exactly once.

An interval in a permutation \({\sigma}\) is a factor of contiguous values of σ such that their indices are consecutive. For example, in the permutation \({\pi} = 346978215\), \({\pi}(4){\pi}(5){\pi}(6) = 978\) is an interval, whereas \({\pi}(1){\pi}(2){\pi}(3){\pi}(4) = 3469\) is not. It is easy to see that every permutation of length \(n\) has intervals of length 0, 1 and \(n\) , at least. The permutations of length \(n\) that only contain intervals of length 0, 1 and \(n\) are said to be simple. So for example the permutation \({\pi} = 346978215\) is not simple as we have seen in the example above that it contains an interval, on the other hand \({\sigma} = 526184937\) is simple as there are no intervals of length strictly greater than 1, except the whole of \({\sigma}\). See [Hof15] for more information on permutation patterns and simple permutations.

Enumeration/Generation Model

language Essence 1.3
given n : int
find perm : sequence (bijective, size n) of int(1..n)
such that
    and([ max(subs) - min(subs) + 1 != |subs| |
        i : int(1..n-1), j : int(2..n),
        i < j,
        !(i = 1 /\ j = n),
        letting subs be [perm(k) | k : int(i..j)]]
    )

given n : int
find perm : sequence (bijective, size n) of int(1..n)

We define the size of the permutation to be n and we are trying to find all the permutations perm to contain the integers 1 to n, by specifying that it is bijective.

The idea of our approach is the property of an interval, where when sorted it creates a complete range. This can be translated to checking that the difference between the maximal and the minimal elements of the interval is not equal to the cardinality of the interval.

We have one constraint to say that there are only intervals of length 0,1 and n. This constraint is defined as a matrix comprehension, which will build a matrix consisting of only boolean entries. We then check the matrix with an and constraint, to spot if there are any false entries, which would mean that we have an interval.

[ num | num : int(1..5), num != 3 ]

This is an example which creates a 1-dimensional matrix of num s where none of the entries are 3. We allow also for letting statements inside the matrix comprehensions, which allow us to define intermediary statements.

and([ max(subs) - min(subs) + 1 != |subs| |
    i : int(1..n-1), j : int(2..n),
    i < j,
    !(i = 1 /\ j = n),
    letting subs be [perm(k) | k : int(i..j)]]
)

We extract i and j to be the beginning and the end of the interval, and we need to make sure that i is less than j to have the right order. As we do not want to include the whole permutation as an interval, we restrict that i and j cannot be simultaneously at the respective ends of the permutation. The final line of the comprehension sets up the continuous subsequences. On the left hand side of the matrix comprehension we use the interval property that when it is turned into a sorted set it is a complete range.

Parameter

language Essence 1.3
letting n be 5

Solving

Using the ESSENCE pipeline, we can solve our sample size by typing the following:

conjure solve simple_perm-gen-model.essence simple_perm-gen-param.essence-param

You will be then returned one .solution file, which contains a sample solution such as:

language Essence 1.3

letting perm be sequence(2, 4, 1, 5, 3)

If you look for an enumeration (or generation) of all solutions, type:

conjure solve simple_perm-gen-model.essence simple_perm-gen-param.essence-param --number-of-solutions=all

The results will be saved into many (for n be 5 you should get 6) .solution files which will contain a solution each.

Checking Model

language Essence 1.3
given n : int
given perm : sequence (bijective, size n) of int
find result : bool
such that
    result = and([ max(subs) - min(subs) + 1 != |subs| |
        i : int(1..n-1), j : int(2..n),
        i < j,
        !(i = 1 /\ j = n),
        letting subs be [perm(k) | k : int(i..j)]]
    )

given n : int
given perm : sequence (size n) of int

We define the size of the permutation to be n and the permutation perm to contain integers.

find result : bool

What the model will tell us is that the permutation is simple (true) or not.

Instances

letting n be 5
letting perm be sequence( 1, 4, 2, 5, 3)

This a non-simple permutation.

letting n be 5
letting perm be sequence(2, 4, 1, 5, 3)

This is a simple permutation.

Solving

Using the ESSENCE pipeline, we can solve our sample instance by typing the following:

conjure solve simple_perm-check-model.essence simple_perm-check-instance.essence-param

The result will be saved into a .solution file which will look something like this (or say false):

language Essence 1.3

letting result be true