Savile Row

Home

News

Releases

Tutorial at CP'14

Releases

Savile Row 1.10.0

18th December 2023

Download 1.10.0 for Linux

Download 1.10.0 for Mac (ARM)

Download 1.10.0 for Mac (Intel)

Release notes

Savile Row 1.10.0 includes performance improvements, better typechecking and error messages, some new features, and bug fixes. Updating is recommended.

The cumulative constraint has been added, with thanks to Luke Ryan for his work on that. This release also adds the cat and list functions: cat to concatenate 1-dimensional lists; and list to combine scalars or matrices (with any number of dimensions) into a single 1-dimensional list.

More SAT encodings of linear and pseudo-Boolean constraints have been added from the paper SAT encodings for Pseudo-Boolean constraints together with at-most-one constraints (AIJ 2022). These can be accessed from command-line flags.

Some bugs have been fixed, and typechecking has been tightened in some cases (producing better error messages). Integer comparison operators (<, =, etc) are now non-associative, preventing the use of counter-intuitive expressions such as x=y=z. Similarly, the logic operators implication and iff have been made non-associative.

The bundled solvers have been updated: Cadical has been replaced with Kissat 3.1.1 as the default SAT solver. Minion has been updated to a version that slightly improves on 1.9. Chuffed has been updated to 0.12.1. Ferret has been updated to 1.0.9.

For Windows users, the Linux distribution works well in the Windows Subsystem for Linux.

Mac users may find that Gatekeeper prevents Savile Row running the bundled executables for solvers. One work-around is to run the solvers (in the bin directory) once each from Finder by right-clicking on them and selecting Open.

Peter Nightingale

Savile Row 1.9.1

11th September 2021

Download 1.9.1 for Linux

Download 1.9.1 for Mac

Release notes

Savile Row 1.9.1 is mainly a maintenance release, fixing some bugs and a performance issue.

The documentation has been combined into one document and some improvements have been made, particularly in the documentation of optional reformulations (controlled by command-line flags). The command-line help text has also been updated to include the same set of command-line flags.

Some improvements have been made in the SAT/SMT backend, in particular the encoding of binary table constraints has been improved and for higher-arity tables an MDD-based encoding is now available (with the new -sat-table-mdd flag) as an alternative to an encoding based on satisfying tuples. The GPW encoding for PBs and integer linear constraints has also been improved.

The bundled version of Minion has been updated to 1.9. Bundled versions of Chuffed, Ferret (graph automorphism solver for detecting symmetry) and Cadical remain the same as in 1.9.0.

Some minor bugs have been fixed, and typechecking error messages have been improved in some cases so I would recommend updating from 1.9.0.

For Windows users, the Linux distribution works well in the Ubuntu 20.04 app on Windows Subsystem for Linux on Windows 10. Instructions for running Savile Row on Windows are in the savilerow-manual.pdf

Mac users may find that Gatekeeper prevents Savile Row running the bundled executables for solvers. One work-around is to run the solvers (in the bin directory) once each from Finder by right-clicking on them and selecting Open.

Peter Nightingale

Savile Row 1.9.0

29th September 2020

Download 1.9.0 for Linux

Download 1.9.0 for Mac

Release notes

Savile Row 1.9.0 adds an SMT backend, supporting the theories QF_IDL, QF_LIA, QF_BV, and QF_NIA, and with the ability to run (and parse output of) the solvers Z3, Boolector, and Yices2. The new backend is described in the CP 2020 paper Effective Encodings of Constraint Programming Models to SMT. Many thanks to Ewan Davidson, Marc Roig Vilamala, Joan Espasa, and Ozgur Akgun for their work on the SMT backend.

The default SAT solver (which is bundled) has been changed to Cadical 1.3.0. As in the last release, Minion, Chuffed, and the graph automorphism solver Ferret are also bundled. Ferret is included to enable automatic symmetry detection and breaking for variable symmetries. The version of Minion is the current repository version, which is close to being released as version 2.0.

Some minor bugs have been fixed, and typechecking error messages have been improved in some cases so I would recommend updating from 1.8.0.

For Windows users, 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.8.0

29th January 2020

Download 1.8.0 for Linux

Download 1.8.0 for Mac

Release notes

Savile Row 1.8.0 adds many options for encoding to SAT, particularly for encoding pseudo-Boolean sums, general (integer) sums, and at-most-one/exactly-one constraints. These include the automatic detection of at-most-one relations described in our CP 2019 paper (Ansótegui et al, Automatic Detection...) and the four encodings of pseudo-Boolean sums and general sums described in the CPAIOR 2019 paper by Bofill et al (SAT Encodings of Pseudo-Boolean Constraints with At-Most-One Relations). There are several new options for encoding at-most-one, and the default encoding has been changed to Chen's 2-product, which is often a significant improvement over the previous default. Some other constraints (e.g. allDifferent) decompose to at-most-one, so the change to the encoding of at-most-one affects many models. The MaxSAT output has been substantially improved, particularly when the objective function is a sum.

A number of bugs have been fixed so I would recommend updating from 1.7.0RC.

The constraint solvers Minion and Chuffed are bundled as executables. The version of Minion is the current repository version, which is close to being released as version 2.0. The version of Chuffed is 0.10.4. The current version of the Glucose SAT solver is also included and will be used by default with the "-sat" flag. The graph automorphism solver Ferret is bundled to support the automatic variable symmetry breaking.

For Windows users, 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.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

Distribution:

  • GNU Trove is now included (http://trove.starlight-systems.com/) (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.

Benchmarks:

  • 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.