Savile Row




Tutorial at CP'14


Savile Row 1.7.0RC

24th August 2018

Download 1.7.0RC for Linux

Download 1.7.0RC for Mac

Release notes

Savile Row 1.7.0RC is the first release candidate for version 1.7.0. Compared to the 1.6 series, there are many changes including many improvements to the SAT backend, and addition of (weighted, partial) MaxSAT as another backend targeting solvers such as Open-WBO. Automatic variable symmetry breaking is now implemented (thanks to Saad Attieh) using a graph automorphism solver to find variable symmetries. Tabulation (described in a paper at CP 2018) is now included as an optional reformulation.

Several bugs have been fixed compared to 1.6.5, with perhaps the most serious being a problem with matrix slicing.

Savile Row now includes the Glucose SAT solver and Chuffed conflict-learning CP solver, in addition to Minion. Also the partition-backtrack solver Ferret is included, and is used to find graph automorphisms for the automatic variable symmetry breaking.

There is no longer a Windows distribution. The Linux distribution works well in the Ubuntu app on Windows Subsystem for Linux on Windows 10. Instructions for running Savile Row on Windows are in the savilerow-manual.pdf

Peter Nightingale

Savile Row 1.6.5

30th June 2017

Download 1.6.5 for Linux

Download 1.6.5 for Mac

Download 1.6.5 for Windows

Release notes

Savile Row 1.6.5 is mainly a maintenance release. There are two main changes. When AC-CSE is switched on, the implied sum constraints generated from allDifferent and GCC have been improved (bounds on the sum have been tightened) by using a min-cost max-flow formulation instead of a simple one-pass greedy algorithm. Also, domain filtering has been sped up by improving the interface between Savile Row and Minion.

A bug in the MiniZinc backend has been fixed.

Peter Nightingale

Savile Row 1.6.4

2nd February 2016

Download 1.6.4 for Linux

Download 1.6.4 for Mac

Download 1.6.4 for Windows

Release notes

Savile Row 1.6.4 is mainly a maintenance release. One new feature has been added, three bugs have been fixed and the documentation has been slightly improved. Also the two documentation articles have been given more sensible names.

New feature:

  • Variable domain filtering can now be applied to auxiliary variables using the -reduce-domains-extend flag.

Bug fixes:

  • For a boolean variable x, the expression x = !x is now rewritten to false, avoiding a problem with variable unification.
  • A matrix expression enclosed in brackets may now be indexed or sliced.
  • A minor bug in matrix slicing has been fixed.

Peter Nightingale

Savile Row 1.6.3

20th July 2015

Download 1.6.3 for Linux

Download 1.6.3 for Mac

Download 1.6.3 for Windows

Release notes

Savile Row 1.6.3 has some improvements to the SAT backend, improving performance of the SAT solver on some problem classes. Minion is now included so that Savile Row works out of the box. There are now three archives for Linux, Mac and Windows, and each includes a static build of Minion 1.8 for that architecture.

Improvements to SAT backend:

  • Reduced memory use when dealing with large decision variable domains
  • Improved decomposition of sums for SAT, leading to a smaller and better encoding
  • Default SAT solver (if not specified on the command line) has been changed from minisat to lingeling.

General improvements:

  • Addition of flatten(n, X) function that flattens first n+1 dimensions of a matrix into one dimension.
  • Addition of toInt function for consistency with Essence. toInt converts a boolean value to an integer. In Essence' toInt is never required because booleans are automatically cast to integers.
  • Type checking of quantifiers has been tightened up.
  • Various minor improvements and bug fixes


  • GNU Trove is now included ( (in the lib directory) to provide more memory efficient hash tables.
  • Minion 1.8 is included (static build for linux, mac or windows). This is used for variable domain filtering and also as the default solver if no solver is specified on the command line.

Peter Nightingale

Savile Row 1.6.2

28th February 2015

Download 1.6.2 as a Tar Gzip file

Download 1.6.2 as a Zip file

Release notes

Savile Row 1.6.2 adds a new backend for SAT solvers, with support for running MiniSat and Lingeling. Also there has been some maintenance, in particular fixing a bug affecting Active CSE.

New features:

  • A SAT backend has been added, producing the standard DIMACS CNF representation. The whole Essence' language is supported.
  • Support for running and parsing the output of SAT solvers MiniSat and Lingeling has been added.

General improvements:

  • Speed of certain operations on matrices has been improved.
  • Generation of implied sum constraints from allDifferent and GCC has been improved: they are only generated when AC-CSE is switched on, and they are removed if they are not changed by AC-CSE. This improves solver performance when the implied constraints are not used by AC-CSE.
  • Type checking has been improved throughout the language.

Bug fixes:

  • A serious bug affecting Active CSE has been fixed. The bug caused negated global constraints to be lost in some cases.

Peter Nightingale

Savile Row 1.6.1

13th October 2014

Download 1.6.1 as a Tar Gzip file

Download 1.6.1 as a Zip file

Release notes

1.6.1 is a maintenance release to fix a few bugs and tidy up and add to the collection of benchmarks. I have also added a few new features, with possibly the most interesting being Active AC-CSE on sums.

New features:

  • Active AC-CSE has been added as an optional optimisation. This extends AC-CSE by matching subexpressions when one is the integer negation of the other.
  • Unify two boolean variables when one is the negation of the other. This optimisation only applies with the Minion backend.
  • Add aggregation of GCC from atmost/atleast constraints.
  • The 'in' infix operator has been added (item in a set).
  • The toSet function has been added to allow construction of integer sets from matrices.

General improvements:

  • Scalability of unrolling quantifiers with very large domains has been improved by using binary splitting.
  • Generating implied sum constraints from alldifferent is now only done when AC-CSE is enabled. This improves solver performance when the implied constraints are not used by AC-CSE.


  • Some existing models in the examples directory have been tidied up, and more parameter files have been added for: EFPA, graph colouring, futoshiki, knapsack, knights tour, Langfords problem, magic squares, N-Queens, nurse rostering, peaceable armies of queens, peg solitaire, and water bucket.
  • A new model of car sequencing has been added, with the 80 parameter files from CSPLib.

Bug fixes:

  • Fixed bug in typechecking quantifiers.
  • Active CSE has been bugfixed and extended with more transformations.
  • Bug fixes of rare cases of matrix indexing and slicing.
  • Fix parsing of >=lex.

Peter Nightingale

Savile Row 1.6

1st July 2014

Download 1.6 as a Tar Gzip file

Download 1.6 as a Zip file

Release notes

  • Associative-Commutative Common Subexpression Elimination (AC-CSE) has been added, as described in a CP 2014 paper. AC-CSE extracts common sets of terms from associative-commutative operators such as sum and product. On some problems AC-CSE can reduce search substantially.
  • Active CSE (Rendl et al) has been added and is enabled by default. Active CSE performs simple transformations (for example, negating an expression then applying De Morgans law) to reveal common subexpressions.
  • Collection of simple constraints into global constraints. In this release AllDifferent constraints are made by collecting not-equal, less-than or other AllDifferent constraints.
  • Command-line switches have been reorganised with new optimisation levels -O0 to -O3 providing easier access to optimisations.
  • Gecode support has been improved, and the Gecode solution(s) can now be parsed by Savile Row.
  • Parser error messages (line and column number of a syntax error) are now much more accurate.
  • Various improvements to simplifiers on constraints -- for example, De Morgans laws are now used to push negation towards the leaves of the expression tree.
  • Max and min functions can now be applied to matrices.
  • A bug affecting the gcc constraint has been fixed.
  • Savile Row 1.6 is best supported by Minion 1.7.

Peter Nightingale

Savile Row 1.5

15th January 2014

Download 1.5 as a Tar Gzip file

Download 1.5 as a Zip file

Release notes

  • The Essence' language has been extended in a number of ways, including adding matrix comprehensions. These provide a useful way of constructing arguments of global constraints, and also can be used as a more flexible alternative to quantifiers.
  • New backend producing an almost flat, instance-level subset of MiniZinc to allow access to more solvers.
  • New option to unify pairs of variables that are equal, and remove variables that are equal to a constant (-deletevars).
  • New option to filter domains of decision variables before CSE and flattening. This may reduce the number of auxiliary variables needed, and in some cases enables other optimisations.
  • Documentation has been much improved.
  • Many bugfixes and improvements throughout the code.
  • Now released under GPL v3.

Savile Row 1.0RC1

Download 1.0RC1

Release notes

  • Translation to Minion should cover all features of the input language (if not it's a bug).
  • Includes using watched-and and watched-or in Minion and Dominion, which means conjunctions/disjunctions/quantifiers in the input are not necessarily flattened down to reified constraints and auxiliary boolean vars.
  • Common subexpression elimination of identical subexpressions is implemented.
  • Output for Gecode is mostly in place but in some cases it may generate the reified form of a constraint that can't be reified.
  • Output for Dominion is far from complete.