solver-support 0.2.2

0.2.2 — keep the whole Savile Row .info, and report the effective registry

Two additions, both about not throwing away information the pipeline already
had. Additive: no existing field changes name or meaning.

Installation

pip install --upgrade solver-support

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

Added

• The whole of each horizon's Savile Row .info file, recorded verbatim on
  the phase under solver_stats['savilerow_info'] (#1). Previously two fields
  were renamed out of it and everything else discarded, so a consumer wanting the
  encoding size, the search-effort counters, or the outcome flags had to re-parse
  the files — which depends on the run's output directory rather than its
  summary, and so stops working once those files are cleaned up. The two renamed
  times, savilerow_time and solver_time, are unchanged.
• ModelRegistry.effective_config(resolved=False) and
  dump_config(resolved=False, header=True), reporting the configuration
  actually in force — the deep merge of the bundled config and any user override
  — plus config_sources, the files that produced it. Intended for a
  consumer's show-registry-style command. resolved=True writes out defaults a
  builder supplies for an absent key, notably a savilerow solver's implicit
  backend: sat, which is the one setting nothing in the config file states.

Notes

savilerow_info is nested, not flattened, because solver_stats is the
core's normalised cross-solver vocabulary while these are one solver's own keys
in its own spelling. It is verbatim, not curated, because the backends
disagree about which keys exist: measured on one model, Minion alone emits
SolverSetupTime / SolverSolveTime / SolverSolutionsFound, the FlatZinc
backends alone SolverTotalWallTime, kissat alone SATVars / SATClauses, and
SolverNodes is absent only from OR-Tools. Four backends give four different key
sets, so any allow-list would already be wrong. The full table is in
docs/timing-model.md.

dump_config is a view, not a config generator. Comments are not preserved,
and user overrides are deep-merged — so adopting a whole dump as an override
would pin every key at today's value and silently shadow later changes. The
emitted header says so. A partial override, carrying only the keys being changed,
is the supported shape.

SolverSatisfiable is not yet promoted to a first-class field. It is the
strongest candidate — every backend emits it, and it separates a refuted horizon
from one that gave up — but its name must not suggest problem-level unsat, which
a bounded model cannot prove.

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

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

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

solver-support 0.1.1

0.1.1 — first public release

A generic, domain-agnostic pipeline for running constraint-modelling and
planning solvers: Conjure / Savile Row (with SAT and CP backends), Fast
Downward, SymK, ENHSP, and UPF-constructed models. It handles the mechanics
every such run needs — building solver command lines from a model registry,
spawning subprocesses with timeouts and clean teardown, naming the per-run
files, parsing solver output into a uniform timing and cost-layer model, and
driving the horizon loop.

It carries no notion of any problem domain. The package ships unwired: a
bare import solver_support resolves no model registry and interprets no
objective, because it has no way to guess either. A consumer registers its
scoring, registry paths, warning logger and UPF planner CLI once, before first
use — see docs/injection-api.md.

Installation

pip install solver-support

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

Highlights

• Four injection seams, each with a module-level default, a setter, and a
  wrapper that reads the current value at call time — so wiring may happen any
  time before first use, and the core never imports its consumer.
• A uniform timing model across very different backends. Savile Row's
  horizon scan and the planners' cost-bound sweeps are squeezed into one shape,
  with the layer arithmetic shared, so cross-solver comparisons are fair by
  construction. See docs/timing-model.md.
• A subprocess runner that distinguishes the three ways a run can fail —
  timeout, interrupt, and a solver that ran and failed — tears down the whole
  process tree on a kill, and records each outcome in the run summary. An
  expected timeout is not logged as an error. See docs/solver-runner.md.
• Consumer-owned summary fields live in an extra bag, flattened into the
  saved JSON, so a domain datum can ride along without the record growing that
  domain's vocabulary.

Notes

Alpha: in day-to-day use by two consumers and covered by its own suite (223
tests), but the API may still shift between 0.x releases.

Python 3.9 support is deliberate — it is the system Python on macOS — and is
verified by building and running the suite on /usr/bin/python3, not merely
declared.

Co-Authored-By: Claude Opus 5 (1M context) noreply@anthropic.com