Introduction

Constraint Programming (CP) is a flexible approach to combinatorial optimization that has been applied to a wide range of important problems. In recent CP conferences we have seen many diverse applications: design problems (design of cryptographic S-boxes, carpet cutting to minimize waste), scheduling (nurse rostering with real-world constraints, resource allocation for datacentres), planning (contingency planning for air traffic control, route finding for international container shipping, assigning service professionals to tasks).

Savile Row is a modelling assistant for CP. It provides a high-level language for the user to specify their constraint problem, and automatically translates that language to the input language of a constraint solver. It is a research tool, so it is designed to be flexible. It is very easy to add new rules and program new translation pipelines.

During the translation process, Savile Row applies some reformulations to improve the model. One interesting class of reformulations is common subexpression elimination (CSE). If the same (or equivalent) expression appears in different parts of a model, CSE replaces the expression with a single variable everywhere it appears. In this way it connects together different expressions in the model. This often improves constraint propagation, and even when it does not do that it can improve the efficiency of a solver by reducing the number of constraints. Savile Row implements several types of CSE, including Associative-Commutative CSE where common sets of terms are factored out of associative-commutative operators such as sums.

Savile Row is the successor to Tailor, developed by Andrea Rendl as part of her PhD. Some of the techniques used by Savile Row were pioneered by Andrea.

The main author of Savile Row is Peter Nightingale. Many others have contributed to the project at various times. To report bugs or ask any questions about Savile Row, contact Peter:

Modelling Language

Savile Row takes in the Essence Prime constraint modelling language. Essence Prime is intended to be solver-independent and high-level. More information about Essence Prime is available in the tutorial that is included with the releases of Savile Row.

Constraint Solvers

Savile Row supports various solvers and solver types:

• Minion is supported as a backend solver and is also used for reformulations such as domain filtering and mutex detection.
• Gecode and Chuffed are also fully supported.
• SAT solvers are supported by a configurable SAT encoding backend, with various options in particular for arithmetic and at-most-one constraints.
• MaxSAT solvers are supported with an extension to the SAT backend, and often work well when the objective function is a sum.
• SMT solvers are supported with an SMT backend that can generate theories QV_BV, QF_IDL, QF_LIA, and QF_NIA.
• All FlatZinc solvers are supported via standard FlatZinc, although for many solvers this output will not be ideal.
• Savile Row can also produce the MiniZinc language.

Unfortunately the output of SAT, MaxSAT, and SMT solvers is not uniform so a parser must be implemented for each solver that we wish to completely support (i.e. run the solver from Savile Row and translate solutions back to Essence Prime). Cadical, Glucose and some others are supported for SAT, Open-WBO for MaxSAT, and Z3, Boolector, and Yices2 for SMT.

Why is it called Savile Row?

Savile Row is a street in London with many bespoke tailors. The name comes from the idea of "tailoring" a constraint model in a variety of different ways.