solver-support 0.2.1

0.2.1 — five Savile Row backends

Everything since 0.1.1. Savile Row can now be driven through five backends
instead of two, each described by a single row in the core and selected by one
key in a solver config.

Additive throughout: a solver config with no backend: key still selects the SAT
arm and builds exactly the command line 0.1.1 built, and Minion's argv is
unchanged. Both properties are pinned by tests.

Installation

pip install --upgrade solver-support

Python 3.9 or newer. Runtime dependencies are psutil and PyYAML only.

Added

• OR-Tools CP-SAT, Gecode and Chuffed as Savile Row backends, alongside the
  existing SAT and Minion arms. Savile Row emits FlatZinc for each and runs the
  binary itself, so none of them needs a new solver driver — only a backend:
  key in a solver config and a matching <backend>_args tune preset. The same
  Essence Prime model reaches every backend through the same translation, which
  is what makes a backend comparison mean anything.
• solver_bin, an optional config key naming the solver binary, emitted
  through whichever flag that backend uses (-fzn-bin, -gecode-bin,
  -chuffed-bin, -minion-bin, -satsolver-bin). Left unset, Savile Row's own
  default applies, so one machine's build stays out of a shared registry.
• solver_timeout_option, an optional config key overriding how a backend's
  own time limit is spelled, for a build whose flag differs.
• ModelRegistry.records_intermediate_objectives(solver), reporting whether
  a solver's backend writes the intermediate-objective file.
• tests/test_command_builders.py, covering backend dispatch: 223 tests at 0.1.1,
  275 now.

Changed

• A backend the core does not know is now an error, not a silent fallback to
  the SAT arm. Previously a config naming, say, or-tools (the hyphenated form
  of Savile Row's own flag) whose presets also carried sat_args would build a
  working SAT command line — a run that succeeded while measuring a different
  solver than the one asked for.
• No .obj file is named for a backend that will not write one. Only the SAT
  arm records intermediate objectives, so on any other backend the horizon loop
  no longer names and clears a file that never appears. This was already true of
  Minion before the FlatZinc backends existed.

Notes

Each backend is described by one row in
CommandBuilderMixin.SAVILEROW_BACKENDS — its binary flag, its own timeout flag
and unit, and whether it records intermediate objectives. The arg-set key is
derived as <backend>_args rather than tabulated. Adding a further backend is a
one-row change.

Two asymmetries between backends are worth knowing about, both documented in
docs/timing-model.md:

• Gecode and Chuffed take their time limit in milliseconds, and neither says
  so in its flag name. The core scales for them. A consumer overriding
  solver_timeout_option changes the flag's name only — the unit belongs to the
  solver, not to the spelling.
• Only the SAT arm records intermediate objectives, since it is the one setup
  where Savile Row rather than the solver runs the optimisation loop. On any
  other backend the horizon scan's continue-scan reads the objective out of the
  solution through the injected extractor instead. A consumer that wires only the
  objective-file route will find continue-scan stops at the first solving horizon
  on those backends; wire set_raw_objective_from_solution for optimisation
  models.

Verified end to end rather than only in unit tests: all four non-SAT backends
solve through the real savilerow, fzn-cp-sat, fzn-gecode, fzn-chuffed and
minion binaries. The suite passes on Python 3.9.6.

0.1.2 and 0.2.0 were spent in development and never released; 0.1.1 is the
immediate predecessor of this release.

Alpha: the API may still shift between 0.x releases.

Co-Authored-By: Claude Opus 5 noreply@anthropic.com