Author: Nicholas Downing
Affiliation: The University of Melbourne, Data61 CSIRO

This solver is called LCG-Glucose, it is a modification of Glucose-3.01 along the lines of Chuffed and CPX, but it aims for greater efficiency in several areas.

The improvements are mostly in the highly-incremental propagators and search, and the core engine that handles wakeups and invokes propagators. The system is designed to have no virtual function call overhead. There is a switch statement that implements the different MiniZinc search strategies at each choicepoint, but otherwise all of the code is inline, and should execute in very tight loops.

The system is also quite minimal and makes extensive use of decomposition. The few propagators in the system are those which can execute extremely fast. All propagators have lazy explanation capability, so they run as simple FD propagators in the first instance, and they only explain themselves if it becomes necessary.

A further improvement is in the front-end FlatZinc driver that encodes the problem to the solver, and then prints the solver results afterwards, as follows:

(1) It automatically uses a value or an order encoding or both. Most constraints require a particular encoding, but search strategies and several constraints like "x = y" and "x != y" have both options. If both encodings are required then a decomposition approach is used with a linking constraint that understands both encodings. In some cases the linking constraint also occurs in reified form, for example "x = a[i]" may use a decomposition approach "(i = v) -> (x = a[v])" with v constrant, and x may be a bounds variable where a[] are domain variables.

(2) It does not create extra variables for common operations, and it exposes the Boolean representation of the model to the modeller in a natural way. Examples:

  x = bool2int(y) aliases the literals [x > 0] and y internally.

  x = (y > 5) aliases the literals x and [y > 5] internally.

  alldifferent(x) where x[1..10] in 1..10 might efficiently be implemented as:
  forall (i in 1..10) (sum (j in 1..10) (bool2int(x[i] = j)) = 1)

(4) It uses half-reification so that reified constraints are considered as two separate halves, and each half is only emitted if necessary. Example:

  (a \/ b) /\ (a = (x < 10)) /\ (b = (x > 10)) would be encoded as:
  (a \/ b) /\ (a -> (x < 10)) /\ (b -> (x > 10))
This transformation is possible when there is nothing in the rest of the model which could force a or b to "false", hence there will never be any need for the negations of the constraints (x < 10) or (x > 10) to hold.

(5) All propagators have reification capability, but the negative propagator is only implemented where it is reasonable to do so. The system accepts a constraint such as "a = alldifferent(...)" and either enters it as "a -> alldifferent(...)", if there is nothing else in the model which forces a to "false", or prints a sensible error message if there is. (The user can resort to decomposition).

(6) All bounds constraints are also considered in separate halves. Examples:

  z = ax + by /\ z < c would be encoded as ax + by <= z < c
This transformation is possible when there is nothing in the rest of the model which would force z > ax + by, hence no need to enforce z <= ax + by.

  a / b = c would be encoded as (c * b <= a) /\ ((c + 1) * b >= a + 1)
This transformation is equivalent, but now there are two halves, and only the necessary halves will be emitted depending on how a, b and c appear elsewhere..

(7) All preprocessing is unscrambled at solution printing time for correctness.

Where an integer variable x uses an order encoding, the literals [x > v] are created lazily, so x can have a large domain. Where an integer variable x uses a value encoding, the literals [x = v] are created upfront, so x can only have a small domain. This compromise works well in practice and runs extremely efficiently. The user can rewrite domain constraints to bounds constraints if necessary.

Given an objective such as "solve minimize 3*x + 2*y + 7*z" the solver can also run in an "unsatisfiable cores" mode where x, y and z are set to their minimum values via Glucose's assumptions framework, and these assumptions are backed off progressively according to the unsatisfiable cores returned by Glucose. Several unsatisfiable-core algorithms are available, we select "OLL" for the competition. We enter the standard (branch-and-bound) variant in the "fd" and "free" categories, and the unsatisfiable-core (OLL) variant in just the "free" category.