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:
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.
Savile Row supports various solvers and solver types:
supported as a backend solver and is also used for reformulations such as domain filtering and mutex detection.
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