|
|
Home News Releases Tutorial at CP'14 |
ReleasesSavile Row 1.10.117th October 2024Download 1.10.1 for Mac (Intel) Release notes1.10.1 is a minor release, however some bugs have been fixed and so upgrading is recommended. The MaxSAT output has been updated to the current competition format, and is now compatible with current solvers such as WMaxCDCL. There is improved error handling (for example, out of memory errors are handled properly), with thanks to Christopher Jefferson. The -param-to-json flag now converts a parameter or solution file in Essence Prime into JSON without needing a corresponding model file. Also the parameter or solution file is now interpreted (i.e. any expressions contained in it are evaluated). Bundled solvers have not been updated compared to the previous release. For Windows users, the Linux distribution works well in the Windows Subsystem for Linux. Peter Nightingale Savile Row 1.10.018th December 2023Download 1.10.0 for Mac (Intel) Release notesSavile 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.111th September 2021Release notesSavile 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.029th September 2020Release notesSavile 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.029th January 2020Release notesSavile 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.0RC24th August 2018Release notesSavile 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.530th June 2017Release notesSavile 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.42nd February 2016Release notesSavile 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:
Bug fixes:
Peter Nightingale Savile Row 1.6.320th July 2015Release notesSavile 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
Improvements to SAT backend:
General improvements:
Distribution:
Peter Nightingale Savile Row 1.6.228th February 2015Download 1.6.2 as a Tar Gzip file Release notesSavile 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:
General improvements:
Bug fixes:
Peter Nightingale Savile Row 1.6.113th October 2014Download 1.6.1 as a Tar Gzip file Release notes1.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:
General improvements:
Benchmarks:
Bug fixes:
Peter Nightingale Savile Row 1.61st July 2014Download 1.6 as a Tar Gzip file Release notes
Peter Nightingale Savile Row 1.515th January 2014Download 1.5 as a Tar Gzip file Release notes
Savile Row 1.0RC1Release notes
|