Savile Row Manual

TL;DR

Savile Row provides a compiler-like workflow that translates Essence Prime constraint specifications into solver inputs for SAT, SMT, and CSP backends, enabling systematic reformulation experiments. Essence Prime is a strongly typed, finite-domain constraint modelling language designed for describing $\mathcal{NP}$-hard decision problems and expressed through decision variables and constraints rather than procedures. The paper details the backends (Minion, Kissat, Chuffed, Gecode, OR-Tools, Standard FlatZinc, SAT, SMT, MaxSAT, MiniZinc) and the transformation pipeline, including partial evaluation, common subexpression elimination, domain filtering, and tabulation that produce solver-ready encodings and solution outputs. It also provides practical guidance on installation, usage, and solver-control options for exploring reformulations and comparative solver performance.

Abstract

We describe the constraint modelling tool Savile Row, its input language and its main features. Savile Row translates a solver-independent constraint modelling language to the input languages for various solvers including constraint, SAT, and SMT solvers. After a brief introduction, the manual describes the Essence Prime language, which is the input language of Savile Row. Then we describe the functions of the tool, its main features and options and how to install and use it.

Figures (2)

• Figure 1: On the left is a Sudoku puzzle. The objective is to fill in all blank squares using only the digits 1-9 such that each row contains all the digits 1-9, each column also contains all the digits 1-9, and each of the 3 by 3 subsquares outlined in thicker lines also contains all digits 1-9. On the right is the solution. (Images are public domain from Wikipedia.)
• Figure 2: First example of a (partial) Sudoku model in Essence Prime