🐏 RamParILS

A parallel Rust rewrite of ParamILS — automated algorithm configuration via Iterated Local Search.

Used as the inner tuner in Grackle, a strategy portfolio invention system for automated reasoning solvers.

Current release: v0.3.0 (2026-10-29) · changelog · sources and issues on GitHub · installation

pip install ramparils                                          # Python extension
cargo install --git https://github.com/deeper4ai/ramparils --tag v0.3.0 --locked   # CLI

💡 What it does

Given a target algorithm with configurable parameters, RamParILS searches for the parameter setting that minimises runtime or a numeric solution cost on a set of training instances. It uses FocusedILS by default. RamParILS starts by scoring configurations on a configurable prefix of the training instances and increases that shared fidelity when the incumbent survives a challenge. Neighbours are submitted to a bounded worker pool, and the first fully evaluated improvement is accepted. Results can be stored in a persistent SQLite cache for reuse by compatible tuning runs.

Cache entries are keyed only by the active configuration and instance path. Use a separate cache when the algorithm command, cutoff, objective, solver version, wrapper behavior, or random seed changes. Reusing a cache across incompatible scenarios can silently return stale results.

📦 What’s new in 0.3.0

• Exact adaptive capping
• Wrapper --version check at startup (wrappers must implement it)
• runhash fingerprints and ramparils db runhashes
• futell: opt-in checkpoint-based early rejection
• instance_shuffle, on by default
• cache_disable scenario option
• Fixes in acceptance, logging and the example wrappers
• Agent skills for running a tuning campaign

Details for this and earlier releases are in the changelog.

🤖 LLM skills

The repository ships skills for LLM coding agents such as Claude Code, which walk an agent through a whole tuning campaign: building and verifying the parameter space, writing the wrapper, setting up the scenario, running and analysing RamParILS, and scoring the strategies found on a test benchmark with SolverPy — with an experiment diary and predictions written before each run. Copy skills/ into the agent’s skills directory (~/.claude/skills/ for Claude Code) and ask it, in plain words, to tune your solver. See LLM skills for the list, installation and usage.

🚀 Key differences from Ruby ParamILS

Parallel evaluation is the primary motivation for the rewrite. Actual speedup depends on worker count, neighbourhood width, current fidelity, solver runtimes, early acceptance, and cache hits. The persistent cache compounds this advantage across compatible Grackle tuning runs on overlapping problem sets.

The search in its basic form: θ is the current candidate, θ_base the point each perturbation starts from, and θ_inc the incumbent that the run returns. See Algorithm for what each box does and for the FocusedILS fidelity schedule.

🔗 Quick links

• Installation
• CLI usage
• Python API
• Algorithm
• Parameter file format
• Solver wrapper protocol
• LLM skills
• Changelog
• GitHub repository

🤝 Acknowledgements

This project is part of DEEPER and supported by the DEEPER grant from Renaissance Philanthropy.

⚙️ Installation

📦 Python extension (pip)

pip install ramparils

🦀 Command-line tool

Clone the repository and install the command-line tool:

git clone https://github.com/deeper4ai/ramparils.git
cd ramparils
cargo install --path . --locked

Or install a release straight from GitHub, without cloning:

cargo install --git https://github.com/deeper4ai/ramparils --tag v0.3.0 --locked

Either installs the ramparils binary into Cargo’s binary directory, normally ~/.cargo/bin. Make sure that directory is on PATH.

For a repository-local build instead:

cargo build --release --locked
./target/release/ramparils --help

Both methods require Rust 1.85+.

🛠️ Python extension (from source)

git clone https://github.com/deeper4ai/ramparils.git
cd ramparils
pip install maturin
maturin develop

maturin develop installs the extension into the active Python environment. Using a virtual environment is recommended.

✅ Verify

Verify the Python package:

python -c "import ramparils; help(ramparils.specialize)"

Verify a Cargo installation:

ramparils --help
ramparils db --help

The Python package requires Python 3.9 or newer. The command-line tool does not require Python.

Changelog

All notable changes to RamParILS are recorded here. The format follows Keep a Changelog, and the project uses semantic versioning.

Dates are commit dates. Entries were reconstructed from the git history, so they describe what changed rather than what was announced at the time.

Unreleased

0.3.0 — 2026-10-29

Exact capping, a wrapper startup check, runhash fingerprints and opt-in checkpoint early rejection.

Upgrading: every wrapper must now answer --version (see the solver protocol), instance_shuffle is on by default so existing scenarios evaluate instances in a different order, and capping uses a different rule, so the same scenario explores different configurations than under 0.2.0.

Highlights

• Exact adaptive capping. The cap now tests the cumulative sum against the budget beating the incumbent allows, so it never discards a configuration that would have been accepted, and one slow instance can no longer cap a configuration outright. Capped scores are logged as lower bounds, >2.698475 (312/473). bound_multiplier keeps its meaning. See Algorithm.
• Wrapper startup check and runhash. ramparils runs <algo> --version before the first evaluation and refuses to start unless the wrapper can reach its solver; the answer is logged, so a run records which solver build it used. Wrappers may also report a runhash, a fingerprint of the solver’s own work, exported by the new ramparils db runhashes to find parameters that change nothing. Wrappers without --version must add it. See Solver protocol.
• futell, an opt-in early rejection of losing neighbours from a checkpoint partway through their evaluation. Heuristic and off by default.
• instance_shuffle, on by default: the instance list is shuffled once, deterministically, before dispatch, so evaluation order changes for existing scenarios. Set instance_shuffle: false to keep the file’s order.
• cache_disable forces every evaluation to run, for checking whether cache hits skew a result.
• Fixes: an incomplete (capped) evaluation can no longer win an acceptance comparison and corrupt the incumbent; debug and error logs append instead of truncating on a rerun; the error log only appears when something crashed; the example wrappers report crashes as UNKNOWN with the full cutoff, never as a cheap cacheable result.
• Agent skills under skills/ for running a whole tuning campaign: domain, wrapper, scenario, analysis and evaluation with solverpy.

Added

• Agent skills under skills/ for running a tuning campaign: tune-solver (the loop, scenario settings, experiment diary), tune-solver-domain (building, verifying and compacting a parameter space), tune-solver-wrapper (the wrapper protocol, with a standard-library wrapper_template.py), tune-solver-analysis (log, error log and cache analysis, with greedy_cover.py and conf_to_strat.py) and tune-solver-eval (scoring strategies on a test benchmark with solverpy).

• cache_disable scenario option: when set, Scheduler::submit skips cache.get_batch() entirely and treats every task as a miss, so every instance actually runs regardless of what cache_db already holds. Writes are unaffected — cache.put()’s existing keep-existing-unless- upgrading-a-timeout policy (a genuine solved result is never clobbered by a later re-run’s differing number; only a timeout can be replaced) applies exactly as before. Added to let a cache-hit-heavy run be re-run with caching off as a clean A/B check for whether cache hits (whose “runtime” contributes to a virtual-worker simulation like futell’s checkpoint at a very different wall-clock cost than a real dispatch) are skewing something.

• futell: opt-in checkpoint-based early rejection of BLS neighbours, alongside the existing (exact) adaptive-capping prune. While a neighbour’s real per-instance results stream in, a simulated N-worker replay is checkpointed at futell_checkpoint × cutoff_time (futell_cores virtual workers, decoupled from real cores:), and the neighbour is rejected outright once that checkpoint is significantly worse than the incumbent’s own (futell_tolerance). Unlike capping this is a heuristic, not a proof — it can reject a configuration that would have gone on to win — so it defaults to off; a rejection is counted separately in the run summary’s new futell_rejected. A rejection (capping’s or future-telling’s) now also actually stops that neighbour’s own solver dispatch via the new Scheduler::cancel_neighbor — without it, a rejected neighbour’s already-queued instances kept running to completion in the background regardless, so early rejection bought no real wall-clock savings. The simulated replay assigns each real result to a virtual worker in the order results actually arrive, not a fixed instance order — an earlier fixed-order design could stall for a long time waiting on one slow straggler while much newer data sat unused. See docs/reference/algorithm.md#future-telling.

• instance_shuffle (default true) shuffles the instance list once, deterministically, before dispatch (instance_shuffle_seed for reproducibility) — decorrelates FocusedILS’s fidelity-growth prefix from any difficulty ordering already present in the instance file. This changes real evaluation order for every scenario that doesn’t explicitly set instance_shuffle: false, including ones that never touch futell — a deliberate default-behavior change, not only new opt-in surface area, though a deterministic one (a given scenario + seed still reproduces identically across reruns). Never affects which instance_id a path is assigned in the cache. futell: true with instance_shuffle: false prints a startup warning, not an error, since a pre-randomized instance file is a legitimate reason for the combination.

• An end-of-run ils: summary line reporting rounds / searched / gated / incumbents / evals / capped / futell_rejected. A gated round is one whose starting configuration was capped and which then accepted no move, so the bound hid its whole neighbourhood and it produced no search. Comparing two approaches on final score alone can hide that one of them was pruned out of most of its rounds.

• The changelog is published with the documentation, at deeper4ai.github.io/ramparils. docs/changelog.md is a one-line mdBook include of this file, so there is still one source of truth.

• The landing page carries the current release, an install one-liner pinned to the tag, a “What’s new” section and a link to the GitHub repository.

• A --version probe before the first evaluation. ramparils now runs <algo> --version at startup and refuses to start unless it exits 0 and its last stdout line is supports: … version …; the wrapper’s whole response is logged as its own block, separated from the run’s other startup stats. This is the fix for a real incident: a 24 h tuning run launched against a wrapper with no solver binary on PATH and no instance files in place ran to completion reporting nothing wrong, because the wrapper answered every evaluation with a well-formed but meaningless result line instead of failing to launch. A wrapper that can’t reach its solver prints a <solver> MISSING placeholder line in the version block but must still exit non-zero. examples/primo and examples/eprover both implement the convention; see docs/reference/protocol.md.

• A runhash fingerprint, threaded end to end. A wrapper’s result line may carry an optional fourth field: a hash of the solver’s own internal counters, independent of runtime, that lets two configurations be compared for having done byte-identical work. results.runhash is a new nullable cache column; a descent XORs it across every evaluated neighbour and logs it beside each incumbent/home base; ramparils db status exports it as a fourth column; and a new ramparils db runhashes writes ram-<hash> <runhash> <n> per strategy (the XOR of every non-null runhash for that hash, skipping instances with none rather than disqualifying the whole hash; n counts every attempted instance, so n == instances means fully evaluated). Given a cache and no sub-command, ramparils db now exports all four (solved, status, confs, runhashes). Two strategies sharing a runhash did identical internal work, which is the signal a structurally dead parameter needs and nothing else can catch.

• examples/eprover rewritten as a grackle-free wrapper via solverpy’s E, replacing the old grackle-dependent example. A deliberately small domain — core proof-search switches, term ordering, and up to 4 independently-tunable clause-selection heuristic slots with their own frequencies — rather than grackle’s full combinatorial space. Three scenarios (eprover-basic/-random/-focused) share one cache, differing only in search approach and fidelity schedule.

Changed

• Adaptive capping now tests the cumulative sum against a budget — partial_sum > bound_multiplier × incumbent_score × n_instances — instead of the running mean against bound_multiplier × incumbent_score. Costs never go down, so passing the budget proves the final mean exceeds the bound: capping becomes exact rather than heuristic and never discards a configuration that would have been accepted. It also fixes both ends of the old behaviour. Results arrive fastest-first, so the running mean was a lower bound that only converged at the end and most capped evaluations ran nearly the whole instance set; at the other extreme there was no minimum sample, and one instance above the bound capped a configuration outright. Now no cap is possible before bound_multiplier × incumbent_score / cutoff_time of the set. The meaning of bound_multiplier is unchanged, so no scenario file needs editing.
• A capped score is now logged as >2.698475 (312/473) rather than as a plain number. It is a mean over the instances that finished first — the fastest — so it understates the true score: the > marks it as a lower bound and the ratio says how much was actually seen, since a cap after 1 instance and a cap after 470 are not the same claim. Affects ils: bls local optimum, ils: bls improvement … (was …), ils: new home base and ils: restart: … score=. Two capped scores cover different, differently biased prefixes and must not be compared with each other.
• Adaptive capping is logged under debug rather than debug_wrapper. It is one line per evaluation, not one per solver call, and the event explaining why a neighbourhood yielded no improvement was invisible in an ordinary debug log.
• examples/primo/primo_wrapper.py migrated to solverpy’s Primo, which already supplies time/memory limits, SMT status parsing and the runhash fingerprint, replacing the wrapper’s own hand-rolled subprocess/ulimit plumbing. Drops the PRIMO environment-variable override in favour of solverpy’s own binary resolution — point a different build at PATH under the expected name instead. Also gains the --version/supports: protocol above and a --params dry-run flag that resolves a parameter set to a command line without running anything.
• future_telling/future_telling_checkpoint/future_telling_cores/ future_telling_tolerance renamed to futell/futell_checkpoint/ futell_cores/futell_tolerance, matching the ils::futell module name. The old spelling briefly parsed as an alias for scenarios already run against it; that alias is now removed — futell* is the only spelling Scenario, the Python bindings, and the run summary’s futell_rejected counter accept.

Fixed

• examples/llm2smt works again. Its wrapper had no --version branch, so the new startup probe made ramparils run refuse that example’s scenario. It now answers the probe (exiting non-zero when llm2smt is not on PATH), and reports a run with no status as UNKNOWN instead of an invented, cacheable error.
• One fast-failing instance collapsed futell’s whole checkpoint horizon. CheckpointTracker::record fed dispatch_rel + runtime to refresh as a stand-in for “now”, on the assumption that a completion can only be observed once its own finish time has really elapsed. That holds for a genuine solve, whose reported runtime is its measured duration — but not for an unsolved one, which reports cutoff_time however fast the process actually exited (the PAR1 contract, docs/reference/protocol.md; a segfault, a GaveUp or a memory-limit abort all report a full cutoff within milliseconds). A single such result therefore handed refresh a whole cutoff’s worth of time that never passed, and the pending-bucket test (now_rel > checkpoint_time, added with D11) wrote off every still-pending virtual worker as busy past the horizon in one shot. The checkpoint then matured on whatever handful of instances had finished by then instead of on a horizon’s worth of work — measured in production as a 5.0s horizon maturing after 0.41s of real wall clock, having seen 27 of 500 instances. Only a solved result’s finish is now taken as an elapsed-time bound; for an unsolved one only its dispatch is known to have happened. Latent since D11 (22518c9) and invisible whenever the first cutoff-reporting arrival happened to be a genuine timeout, which is why earlier futell runs matured at plausible-looking times.
• An incomplete evaluation could win an acceptance comparison and corrupt the incumbent. A capped/checkpoint-rejected evaluation’s score is a mean over whichever instances happened to finish first — an optimistic lower bound, not a real measurement — but nothing checked complete before comparing scores. A futell-capped restart/perturbation could out-score a real, fully-evaluated incumbent purely by having run on fewer, faster instances. try_promote_incumbent/accept_or_reject_home_base/ set_home_base now refuse an incomplete evaluation outright; inside a single descent, a gated/incomplete starting point can no longer block a genuine neighbour from being accepted either, since no real evaluation could ever be proven to dominate an untrustworthy one.
• futell’s checkpoint fallback could silently discard a pending real dispatch’s busy-time. CheckpointTracker::record’s fallback bucket selection (a completion with no matching record_dispatch, e.g. a cache hit) picked the globally least-busy virtual bucket without excluding buckets still occupied by a pending dispatch, unlike least_busy_free_bucket(). Landing on such a bucket overwrote its busy-until with the fallback job’s timeline, which the real pending dispatch’s own eventual record call would then overwrite right back — understating total simulated load and risking an early false-positive checkpoint maturity. Only reachable when concurrent real dispatches exceed futell_cores (oversubscription); every scenario run against this feature so far kept futell_cores == cores, so it was dormant in practice.
• Debug and error logs no longer truncate on a rerun. Both were opened with File::create, so a second ramparils run (or specialize() call) against the same paths silently discarded the previous run’s history. They now open in append mode, so a rerun’s output adds to the running history.
• The error log is created lazily, on the first crash, not at startup. It used to be created eagerly even when nothing ever crashed, so every clean run left a 0-byte file behind that looked exactly like “checked, nothing wrong” — indistinguishable from a real crash report that was never written.
• A wrapper crash is routed through UNKNOWN with PAR1 scoring, not an invented status. examples/primo/primo_wrapper.py used to report a crash as its own "error" status with the real (possibly near-instant) elapsed time; RamParILS doesn’t recognise "error" as special, so every crash was silently cached as a legitimate result and the error log — the one place a human would notice — stayed empty, while a fast-failing configuration could score better than a genuine solve. It now reuses RamParILS’s own UNKNOWN sentinel (logged, excluded from the cache) and always charges the full cutoff on any non-success line. Found via examples/eprover’s new wrapper, where the same two bugs let a batch of invalid parameter values silently score better than real solves on ~43% of evaluations; see docs/reference/protocol.md.

0.2.0 — 2026-08-19

The escape mechanism, the provenance stamping, a unified CLI and a reworked set of documents.

Upgrading: the CLI is not compatible with 0.1.x. ramparils run <scenario.yaml> replaces ramparils --scenariofile <scenario.yaml>, and the ramparils-db binary is now ramparils db. Scenario files, parameter files, caches and the Python API are unchanged, so only the invocation moves.

Highlights

• One command-line tool, two sub-commands. ramparils run scenario.yaml tunes; ramparils db cache.dbcache exports what a result cache holds. This replaces --scenariofile and the separate ramparils-db binary, so 0.2.0 is not CLI-compatible with 0.1.x — scenario files, parameter files, caches and the Python API are unchanged, only the invocation moves. See CLI.
• A search that can climb out of a local optimum. The acceptance criterion alone could only ever move downhill, so a strong local optimum ended the useful part of a run. Soft acceptance within a tolerance, stagnation-triggered restarts, a choice of restart target, and ParamILS’s random probes now address it — all off by default. See Algorithm.
• Provenance. ramparils --version and the header of every debug log carry the git revision the binary was built from, with a -dirty marker when the worktree was not clean. A version number alone never said which code ran.
• ramparils db confs recovers the configuration behind each strategy hash in a cache, so a .dbcache is no longer a pile of opaque hashes.

Added

• Escape mechanism for a frozen ILS home base. The acceptance criterion only ever replaced the home base with an at-least-as-good local optimum, so nothing in the loop could move the search uphill: once a strong local optimum was found, every later round perturbed the same point. Five new scenario fields address it, all defaulting to previous behaviour:

  • acceptance_tolerance — accept a worse local optimum as the home base while it stays within this relative margin of the incumbent (measured against the incumbent, not the home base, so the margin cannot compound);
  • restart_failures — restart after this many consecutive rejected local optima, which adapts to however many rounds a budget turns out to allow;
  • restart_probability — ParamILS’s p_restart;
  • restart_target (incumbent | random) and restart_strength — where a restart lands and how far it jumps. 0 resolves to 2 × perturbation_strength, and the resolved value is printed in the debug header;
  • random_probes — ParamILS’s R, previously unreachable because resolve_initial_config always returned a configuration. Defaults to 0: specializing a caller-supplied strategy should start from that strategy.

  Restarts and home-base replacements are logged distinctly (ils: restart:, ils: new home base: with a parameter diff), so a run dragged along by its escape mechanism can be told from a healthy one.

• Source revision in --version and in every debug-log header, stamped at build time by build.rs. A -dirty suffix marks an unclean worktree, and a build without git reads unknown rather than failing. The version alone never identified the code, since a tag covers every commit after it.

• docs/figures/basic-ils.svg, a diagram of BasicILS shown in the README, the documentation index and the algorithm reference, with its regenerable TikZ source beside it.

• A “Designing a space” section in the parameter-file reference: what a domain costs in every neighbourhood, why declaring conditionals is free and their absence is not, conditionals versus forbidden combinations, and why a guard is only explorable if it pays at its dependents’ default values.

• rust-version = "1.85" in Cargo.toml, matching the MSRV the documentation already claimed.

• rustfmt.toml (max_width = 120), and the whole tree reformatted to match. The code had been hand-formatted since the first commit, so cargo fmt --check — listed as a standard command in AGENTS.md and the README — had never passed. It passes now, and can be enforced in CI. 120 rather than rustfmt’s default 100 because the dominant pattern here is a debug_line(d, &format!(…)) call written to read like the log line it produces; the file records the measurements behind the choice.

• CHANGELOG.md, this file.

• examples/primo gained the flattening and SOI-minimization options (boolean_flatten_threshold, boolean_flatten_post_threshold, lra_soi_minimize, lra_soi_minimize_order) in its wrapper, and a revised 24-parameter space, params-primo-qflra.txt, carrying the measurement behind each choice. Its scenario now runs BasicILS with settings derived from a nine-run tuning campaign, and documents what to adjust first.

Changed

• BREAKING: one binary, two sub-commands. ramparils run <scenario.yaml> replaces ramparils --scenariofile <scenario.yaml>, and the separate ramparils-db binary is gone — its sub-commands are now ramparils db. There is no compatibility shim: the old forms are errors.

  db also changes shape. All three sub-commands are exports now, writing one file per strategy hash named ram-<hash> under --out-dir, which defaults to solverpy_db rather than the current directory, in a layout that mirrors solverpy’s database so an export can be dropped into an existing solverpy_db/. Each prints a one-line summary on stdout and uses stderr for errors only.

  • solved and status now record the full instance path the cache stored, not the basename, matching solverpy’s files.
  • strategies is renamed confs and writes files rather than a table on stdout: one per hash, holding the configuration as YAML (--json for the stored JSON). It is deliberately not solverpy’s strats/ — that holds a solver command line, this holds a parameter assignment, which only means anything against the parameter space it was tuned in. Note it records the active configuration, so it is a record of what ran rather than a complete one, and initial_config_file will reject it unless every parameter was active.
  • solved’s success-status set is now documented in --help.
  • given a cache and no sub-command, db runs all three: ramparils db results.dbcache is solved, status and confs in one go.

• A closed stdout no longer panics. Rust ignores SIGPIPE at startup, so println! panicked with a backtrace when the reader went away — piping any of this into head did it, including the old ramparils-db strategies, whose table output existed to be piped. main now restores the default disposition, so the process exits quietly with 141 as any Unix tool does.

• approach: random is now ParamILS’s pert_rand — a fresh random configuration each round with the acceptance criterion skipped, i.e. a random-restart baseline. It was previously a silent alias for basic, so any earlier run that set it was really running BasicILS.

• The adaptive-capping documentation now states the ceiling rule: under a PAR1 runtime objective capping cannot fire unless bound_multiplier × incumbent_score < cutoff_time, so a multiplier just below that ratio is indistinguishable from pruning: false.

• examples/primo/params-primo.txt was renamed to params-primo-qflra.txt.

Fixed

• examples/eprover/run.sh had been broken since 0.1.2: it passed --debug, --debug-log and --cachedb, which became scenario fields in that release, so the script could not have run. Those three settings moved into its scenario.yaml, where they belong.
• The SAPS example in the parameter-file reference did not parse: wp’s default 0.03 was absent from its domain, so anyone copying it hit default '0.03' not in domain.
• The Python API reference claimed specialize runs FocusedILS; it runs whichever variant scenario["approach"] selects.

0.1.3 — 2026-08-06

Added

• The cache records what each strategy hash means (strategies table, written the first time a configuration is evaluated, and added automatically when an older cache is opened). Without it a .dbcache is a pile of opaque hashes whose recovery depends on the space still being small enough to enumerate and on DefaultHasher being reproducible across compiler versions — which it is explicitly not. Exposed as ramparils-db strategies.
• Cutoff-aware result caching. Each result stores the cutoff it was measured under: a timeout satisfies only requests with an equal or shorter cutoff, and a completed run exceeding a shorter requested cutoff is returned as an in-memory synthetic timeout and never written back. Caches predating this are incompatible and must be replaced.
• Scenario initial configurations, inline via initial_config or in a file via initial_config_file, validated against the parameter space.
• examples/primo, and guarded_real_equality_lowering in its space.
• Strategy extraction from tuning logs for the llm2smt example.

Fixed

• FocusedILS compared scores taken at different fidelities. The incumbent was re-measured when the fidelity grew but the ILS home base was not, so the acceptance criterion compared a current score against a stale one taken on a shorter prefix. Because prefix means drift as the prefix grows, the stale bar was biased low and the only mechanism that could update it was the comparison it blocked — the home base froze for the rest of the run. Both retained states are now re-measured at every increase, and each increase is logged with both scores.
• An incomplete fidelity increase at the deadline no longer discards the incumbent’s score.
• Canceled solver workers are terminated rather than left running; solver process trees are terminated on interrupt; queued solver work is bounded.

0.1.2 — 2026-06-10

Added

• All tuning knobs unified into the scenario file. The CLI keeps only --scenariofile (and --version), which makes a run reproducible from one file.
• Configurable FocusedILS evaluation fidelity (initial_fidelity, fidelity_step).
• Iterative deepening (iterative_deepening, lambda_n, lambda_c, lambda_t): multiple ILS phases on an exponential schedule of instances, cutoff and cumulative deadline.
• ramparils-db with solved and status sub-commands.
• Structured debug logging: debug, debug_log, debug_wrapper, debug_solver, and error_log for crash reporting.
• The llm2smt and eprover examples, and eprover integration tests.
• Documentation moved to mdBook, with a scenario reference, an algorithm overview and a glossary.

Changed

• cache_db defaults to :memory:, so a run no longer leaves a stray database behind.
• Solver status is stored in the cache.

Fixed

• Improvement detection uses a strict <, so an equal-scoring challenger no longer replaces the incumbent endlessly.
• Failed and crashed runs are charged the penalty quality (10_000_000) and are not written to the persistent cache.
• The parameter parser accepts standalone conditions.

0.1.0 — 2026-04-10

First public release: a parallel Rust implementation of ParamILS with BasicILS and FocusedILS, parallel evaluation over (neighbour, instance) pairs, an SQLite result cache, a PyO3 extension exposing specialize, and the ParamILS-compatible parameter-file syntax.

⌨️ CLI

One binary with two sub-commands: run tunes, db exports a cache.

ramparils run path/to/scenario.yaml

All tuning options — instances, cutoff times, algorithm settings, cache location, debug flags — live in a single YAML scenario file. run takes the scenario path and nothing else: every knob is a field in the YAML, making scenarios self-contained, reproducible, and easy to share.

ramparils db results.dbcache             # all three at once

ramparils db solved  results.dbcache     # or one at a time
ramparils db status  results.dbcache
ramparils db confs   results.dbcache [--json]

db writes one file per strategy hash, named ram-<hash>, under --out-dir (default solverpy_db), in a layout that mirrors solverpy’s database:

Each prints a one-line summary on stdout; stderr carries errors only. Given a cache and no sub-command, db runs all three, so ramparils db results.dbcache is the usual invocation and the sub-commands are there for when you want one of them or --json.

A cache whose filename happens to be solved, status or confs is read as the sub-command instead; write ./status to disambiguate.

solved counts a result as solved when its status is one of Theorem, Unsatisfiable, Satisfiable, CounterSatisfiable, ContradictoryAxioms, sat or unsat — the union of TPTP’s and SMT-LIB’s success tokens, as solverpy uses. RamParILS itself stores the status verbatim and never interprets it when scoring, so a target algorithm reporting anything else is not recognised here and its instances are reported as unsolved.

confs/ is deliberately not solverpy’s strats/: a strategy file there holds a solver command line, a conf file here holds a parameter assignment, which only means anything against the parameter space it was tuned in. It records the active configuration — parameters whose guard was closed are absent, because that is what the cache keys on, and what collapses a guarded sub-space to a single entry. A conf file is therefore a record of what ran rather than a complete configuration, and initial_config_file will reject it unless every parameter in the space happened to be active.

$ ramparils --version
ramparils 0.3.0
git:   6d967a5
build: release, rustc 1.97.1 (8bab26f4f 2026-07-14), x86_64-unknown-linux-gnu

The revision is baked in at build time, and it matters more than the version: 0.3.0 covers every commit since that tag, so the version alone does not say which code ran. A -dirty suffix means the worktree had uncommitted changes and the revision therefore does not identify the build. Where the crate is built without git — an sdist, a source tarball — the revision reads unknown rather than failing the build. The same lines open every debug log:

[    0.00s] binary:  ramparils v0.3.0
[    0.00s] git:     6d967a5
[    0.00s] build:   release, rustc 1.97.1 (8bab26f4f 2026-07-14), x86_64-unknown-linux-gnu

🧭 Scenario file reference

# Required: use instance_file or instances
algo:          "ruby /path/to/solver_wrapper.rb"
paramfile:     "/path/to/solver.params"
instance_file: "data/train.txt"
# instances:   ["data/one.cnf", "data/two.cnf"]
initial_config:
  engine: quick
  threads: 4
# initial_config_file: "initial-config.yaml"  # alternative to initial_config
cutoff_time:   5.0
tuner_timeout: 300.0

# Optional — shown with defaults
run_obj:               runtime   # runtime | quality
overall_obj:           mean      # mean | median
approach:              focused   # focused | basic | random
perturbation_strength: 4
restart_probability:   0.0       # ParamILS p_restart; 0 = never
restart_failures: 0        # restart after k rejected local optima; 0 = never
restart_target:        incumbent # incumbent | random
restart_strength:      0         # 0 = 2 * perturbation_strength
acceptance_tolerance:  0.0       # accept within this margin of the incumbent
random_probes:         0         # ParamILS R; 0 = start from the given config only
initial_fidelity:      1
fidelity_step:         1
bound_multiplier:      10.0
pruning:               true
iterative_deepening:   false
lambda_n:              0.5
lambda_c:              0.5
lambda_t:              0.5
cores:                 0         # 0 = all available
num_run:               0
instance_shuffle:      true      # shuffle instances once before dispatch
instance_shuffle_seed: 0
futell:            false   # checkpoint-based early rejection of BLS neighbours
futell_checkpoint: 1.0     # horizon, as a multiple of cutoff_time
futell_cores:      ~       # virtual worker count; null = same as `cores`
futell_tolerance:  0.0
cache_db:              ":memory:"    # use a file path to persist across runs
cache_disable:         false    # true: never read a cache hit (writes still happen)
debug:                 false
debug_wrapper:         false
debug_solver:          false
debug_log:             ~         # path or null
error_log:             ~         # path or null

🔑 Required fields

Paths in the scenario, parameter file, and instance list are interpreted from the directory where ramparils is started, not from the scenario file’s directory. Use absolute paths or run from a documented working directory when the scenario must be portable.

Initial configuration

Use either initial_config for an inline YAML mapping or initial_config_file for a file containing the same mapping:

initial_config:
  engine: quick
  threads: 4
  use_preprocessing: true

initial_config_file: "initial-config.yaml"

The two fields are mutually exclusive. An explicit initial configuration must contain every parameter from the parameter file, including conditional parameters that are initially inactive. Parameter names and values are validated against the parameter space, and forbidden configurations are rejected. YAML string, numeric, and boolean scalar values are accepted.

When neither field is present, RamParILS retains its previous behavior and starts from the defaults in square brackets in the parameter file. initial_config_file is interpreted from the directory where ramparils is started.

🎯 Objective

🔍 Algorithm

FocusedILS uses the first N entries from the (shuffled, by default — see instance_shuffle below) instance list, not a random sample each round.

📈 Iterative deepening

Runs multiple ILS phases with an exponential schedule. Early phases use fewer instances and a shorter cutoff to rapidly explore the space; later phases refine the best region with the full budget. Useful when the training set is large or cutoff_time is long. See Iterative deepening.

⚙️ Execution

🔮 Future-telling

An opt-in, second, heuristic early-rejection prune for basic_local_search’s neighbour evaluation, alongside the existing (exact) adaptive-capping prune. While a neighbour’s real per-instance results stream in, a simulated N-worker replay of what has arrived so far predicts, from a checkpoint partway through, whether the neighbour is on track to beat the incumbent — and rejects it outright if it clearly is not. Unlike capping, this can reject a configuration that would have gone on to win; it is off by default for exactly that reason.

A rejected neighbour is counted in the end-of-run summary’s futell_rejected, separate from capped — capping is a proof (a capped score is always a valid lower bound); a checkpoint rejection is a statistical heuristic measured on one dataset, not a guarantee. If a run’s outcome looks suspicious, re-run it with futell: false to check whether the feature changed anything.

Cache entries are keyed by the active configuration and instance path, with the execution cutoff stored on each result. A timeout can satisfy only requests with an equal or shorter cutoff. A completed result that exceeds a shorter requested cutoff is returned as an in-memory synthetic timeout and is never written back. The algorithm command, objective, solver version, wrapper behavior, and random seed are not included. Use a separate cache if any of them change; otherwise stale results may be reused without warning.

Caches created before cutoff-aware results were introduced are incompatible and must be removed or replaced with a new cache file.

🩺 Debug

📤 Output

The complete best configuration is printed to stdout as an alphabetically ordered YAML mapping:

alpha: '1.256'
ps: '0.1'
rho: '0.5'
wp: '0.03'

Values are YAML strings so they preserve the parameter-file representation. Inactive conditional parameters are included, making the output directly usable as a future initial_config or initial_config_file.

When debug_log is configured, the final YAML mapping is also written there. Every improved incumbent is recorded in the log with hash=<hash> followed by its complete YAML configuration. The hash identifies the active configuration used by the evaluation cache.

🐍 Python API

import ramparils

The Python extension provides a single function, specialize, that runs ILS from an initial strategy and returns the best configuration found within the time budget. The variant is whatever scenario["approach"] selects — focused by default, basic to score every candidate on the whole instance set. It is a native Rust extension built with PyO3, so there is no subprocess overhead — the ILS loop, parallel evaluation, and SQLite cache all run in-process. All tuning options are passed as fields in the scenario dict, matching the YAML keys documented in the CLI reference.

🐏 specialize

ramparils.specialize(strategy, scenario) -> dict[str, str]

Specialize a strategy on a set of benchmark instances using ILS.

Runs Iterated Local Search starting from strategy, evaluating (configuration, instance) pairs in parallel, and returns the best configuration found within the time budget. Results may be cached in SQLite when cache_db names a file.

Cache entries are keyed only by the active configuration and instance path. Use a separate cache when the algorithm command, cutoff, objective, solver version, wrapper behavior, or random seed changes. Reusing an incompatible cache can silently return stale results.

📥 Arguments

strategy — dict[str, str]

Initial parameter configuration as {name: value} strings. Must contain every parameter defined in scenario["paramfile"]. Values are strings even for numeric parameters (e.g. "1.189").

scenario — dict

Tuning scenario. All keys match the YAML fields in the CLI reference.

Required keys:

At least one of the following must be supplied to specify instances:

If both are present, instances takes precedence. Relative paths are resolved from the Python process’s current working directory, not from the parameter or instance-list file.

Optional keys (all have defaults matching the CLI):

FocusedILS uses the first N entries from instances or instance_file while fidelity grows, after instance_shuffle (on by default) reorders the list once, deterministically.

📤 Returns

dict[str, str] — The best configuration found. Only active parameters are included (inactive conditional parameters are omitted).

⚠️ Raises

RuntimeError — If the scenario is invalid, the instance list is empty, the paramfile cannot be parsed, or the cache cannot be opened.

🧪 Example

import ramparils

result = ramparils.specialize(
    strategy={
        "alpha": "1.189",
        "rho":   "0.5",
        "ps":    "0.1",
        "wp":    "0.03",
    },
    scenario={
        # Required
        "algo":          "ruby /path/to/saps_wrapper.rb",
        "paramfile":     "/path/to/saps.params",
        "instances":     [
            "/path/to/instances/inst1.cnf",
            "/path/to/instances/inst2.cnf",
        ],
        "cutoff_time":   5.0,
        "tuner_timeout": 120.0,
        # Optional — defaults shown
        "cache_db":      "/tmp/ramparils_cache.db",
        "cores":         0,       # 0 = all available
        "approach":      "focused",
        "debug":         False,
    },
)

print("Best config found:")
for k, v in sorted(result.items()):
    print(f"  {k} = {v}")

See examples/saps_python.py for a runnable example.

🤖 LLM skills

RamParILS ships a set of skills for LLM coding agents: instruction files that teach an agent how to run a whole tuning campaign with RamParILS, from building the parameter space to scoring the strategies it finds. They are plain Markdown (one SKILL.md per directory, with a short front-matter description the agent uses to decide when to load it), in the skills/ directory of the repository.

They encode what our own tuning campaigns on ATP and SMT solvers taught us: which scenario settings work, which mistakes silently waste a run, and why the final configuration a run prints is not necessarily the best one.

📚 The skills

The four specialised skills also work on their own — for example, to review a parameter file or to score a set of strategies that were not tuned by RamParILS at all.

⚙️ Installing

Agents look for skills in a fixed directory. For Claude Code, that is ~/.claude/skills/ for skills available in every project, or .claude/skills/ inside one project:

git clone https://github.com/deeper4ai/ramparils.git
mkdir -p ~/.claude/skills
cp -r ramparils/skills/* ~/.claude/skills/

Copy them again after a git pull to pick up changes. Other agents that read the same SKILL.md format take the same directories, copied to wherever that agent looks for skills.

The skills refer to this documentation and to the worked examples in examples/ (examples/eprover/, examples/primo/). Keep the clone around and tell the agent where it is, or let it read them from GitHub and from this site.

💬 Using them

The agent loads a skill by itself when a request matches its description, so asking in plain words is usually enough:

Tune the E prover on the problems in bench/train.txt with RamParILS; the best
strategy we have so far is in strategies/best.txt.

Review params-mysolver.txt before we start a long run.

The run in runs/03 has finished. Analyse it and pick the strategies to
evaluate on bench/test.

To name a skill explicitly in Claude Code, type it as a command: /tune-solver, /tune-solver-analysis, and so on.

What to expect from a session started with tune-solver:

1. Questions first. The goal (deployment cutoff, single best strategy or a portfolio), the anchor strategy every evaluation is compared to, and the training and test benchmarks.
2. Files to review before anything long runs — the parameter file, the wrapper, the scenario — then a smoke run of a few minutes, with its log header and error log checked.
3. A prediction note written before the long run, and a diary entry after it that checks each prediction against the result.
4. After the run, not just the final configuration: every incumbent and a set of complementary strategies, converted to strategy files and scored on the test benchmark against the anchor.
5. A proposal for the next round: what to drop from or add to the domain, which configuration to start from, what to change in the scenario.

Long runs, remote machines and anything that costs real compute stay under your control: tell the agent what it may launch on its own, and where.

🧠 Algorithm

RamParILS implements Iterated Local Search (ILS) for automated algorithm configuration. The goal is to find the parameter setting of a target algorithm that minimises runtime or a numeric quality cost on a set of training instances. Both objective modes are minimisation; wrappers for maximisation problems must transform utility into a cost.

🔄 Iterated Local Search

ILS alternates between two phases: local search finds a local optimum in the configuration space, and perturbation escapes it by applying a random walk. Starting from an initial configuration (typically the parameter file’s declared defaults), local search explores the neighbourhood one parameter at a time, greedily accepting any neighbor that improves performance. When no improving neighbor exists, perturbation applies perturbation_strength random steps to escape the local optimum, and the cycle repeats until the tuner timeout expires.

The neighbourhood of a configuration is all configurations that differ in exactly one parameter. For a space with P parameters and average domain size D, each configuration has at most (D−1)×P neighbors. RamParILS submits neighbours to a bounded worker pool and accepts the first fully evaluated improvement. The wall-clock cost still depends on neighbourhood width, fidelity, worker count, cache hits, and solver runtimes.

The perturbation draws uniformly from the neighbourhood, not from the parameters, so a parameter with a large domain is perturbed more often than a boolean one: a five-valued parameter offers four of the neighbours a boolean offers one.

The figure is approach: basic, where every candidate is scored on the whole instance set; FocusedILS wraps the same loop in a growing prefix, described below.

Three configurations are in play at once, and keeping them apart is most of understanding the search. θ is the round’s candidate. θ_base is the point each perturbation starts from — the ILS home base. θ_inc is the incumbent: the best configuration seen, and what the run returns.

Note where each is written. The local search sets θ and, if the descent improved on it, θ_inc; the acceptance criterion sets θ_base. Only θ_base is perturbed, so the incumbent improving does not by itself move the search: once the home base stops moving, every later round samples the same ball around a fixed point. That asymmetry is the reason for the knobs in the next section, and the source of the failure they were added to fix.

🪂 Escaping a frozen home base

The acceptance criterion only ever replaces the home base with an at-least-as-good local optimum, so on its own it cannot move the search uphill: once a strong local optimum is found, every later round perturbs the same point and the run degenerates into repeated sampling from a fixed ball. Four optional knobs address this. All are off by default, so a run that does not set them behaves exactly as before they existed.

restart_target decides where a restart lands: incumbent perturbs the best configuration found so far by restart_strength steps (default 2 × perturbation_strength), while random draws a uniformly random configuration, which is what ParamILS does. Restarts are logged so they can be told apart from ordinary acceptance when a run is read back:

ils: restart: reason=stagnation target=incumbent strength=10 score=0.481578 instances=473 after 10 rejected local optima

⚖️ BasicILS vs FocusedILS

The approach field selects the ILS variant.

BasicILS (approach: basic) evaluates candidates on the complete training-instance set before comparing their aggregate scores.

FocusedILS (approach: focused, the default) uses progressive global fidelity. Candidates are compared by their aggregate score on the current prefix of the training-instance list. When the incumbent survives a challenge, the prefix grows by fidelity_step until all instances are used. A challenger must have a strictly lower score at the current fidelity to replace the current configuration.

RamParILS starts FocusedILS at initial_fidelity instances per configuration and increases that global fidelity by fidelity_step, up to the number of available instances. With W workers and fidelity F, the current scheduler can approximately evaluate ceil(W/F) different neighbors at once. Increasing F therefore uses more workers on instances of the same neighbor and reduces speculative work on neighbors that may become irrelevant after the first improving move.

Fidelity always uses the first F entries in the supplied instance list. The list is not shuffled, so its early prefixes should be reasonably representative of the complete training set.

A score is only meaningful relative to the prefix it was measured on — different fidelities are different objective functions, and comparing across them is meaningless. Two configurations outlive a fidelity increase: the incumbent, and the local optimum the next perturbation starts from (the ILS home base). Both are re-measured on the new prefix whenever the fidelity grows, so every comparison the ILS makes is between scores taken on the same instances. Each increase is logged as

ils: n_runs increased to 64/1753 incumbent_score=0.456619 home_base_score=0.456619

The home base is usually the incumbent, in which case the second measurement costs nothing.

Home-base replacements are logged too, one line each, with the parameter diff against the previous home base rather than a full configuration block — it can change every round:

ils: new home base: hash=bd4315273a9356dd score=0.025000 instances=4 changes: alpha: 3 -> 2; beta: a -> b

Replacements with no effective change (a differing value on a parameter whose guard is off) produce an empty diff and are not logged.

This matters more than it may appear. Prefix means drift as the prefix grows — typically upward, if the early instances are cheaper — while the acceptance criterion is monotone: the home base is only ever replaced by something that beats it. A home base left on an old, smaller prefix therefore holds an optimistically low bar that the only mechanism able to update it can no longer clear, and the perturbation centre freezes for the rest of the run. ParamILS avoids this by storing a score per fidelity level for every configuration and always comparing two states at their common level (isBetterWithLesserDetail in param_ils_2_3_run.rb); RamParILS keeps one score per state and re-measures instead.

Random (approach: random) is ParamILS’s pert_rand: it uses all instances from the start, but each round begins from a fresh uniformly random configuration and the acceptance criterion is skipped entirely, so nothing carries over between rounds except the incumbent. That makes it a random-restart baseline to measure an iterated local search against, not a tuning mode to prefer. Restarts are inert under it, since every round already restarts.

✂️ Adaptive capping

Adaptive capping (pruning, bound_multiplier) abandons an evaluation once the configuration has spent the entire budget that beating the incumbent would allow:

partial_sum > bound_multiplier × incumbent_score × n_instances

Costs never go down, so passing that budget proves the final mean exceeds the bound. Capping is therefore exact — it never discards a configuration that would have been accepted — and it fires at the earliest point where the proof exists.

Pick the multiplier against the objective’s ceiling, not in the abstract. Under a runtime objective no instance is charged more than cutoff_time, so with B = bound_multiplier × incumbent_score and C = cutoff_time, capping cannot fire at all unless B < C, and when it can, no cap is possible before B / C of the instance set — spending a budget of B·N takes at least that many instances. With an incumbent of 0.478 at a 1 s cutoff, multiplier 2.0 gives B/C = 0.96: nothing is pruned before 96% of the set, which is indistinguishable from pruning: false. The same 2.0 at a 10 s cutoff with an incumbent of 2.95 gives 0.59 and prunes normally. Express the intent as a fraction of the ceiling and the multiplier follows.

A capped score is a lower bound, not a score, and is logged as one:

ils: bls local optimum score=>2.698475 (312/473)

It is a mean over the instances that finished first — the fastest — so it understates the true mean. Never compare two capped scores with each other: each covers a different, differently biased prefix.

Under overall_obj: median the cap tests a statistic the run does not score — it always sums. Prefer pruning: false there.

A run ends with an account of what the search actually got to do:

ils: summary rounds=79 searched=8 gated=71 incumbents=2 evals=2612 capped=2489 future_telling_rejected=0

A gated round is one whose starting configuration was capped and which then accepted no move: the bound hid every neighbour, so the round produced no search. Worth reporting whenever two approaches are compared — the bound is relative to the incumbent, so it prunes a small perturbation and a fresh random draw at very different rates, and a final-score comparison alone hides that.

🔮 Future-telling

An opt-in (future_telling: true) second, heuristic prune, alongside capping: while a neighbour’s real per-instance results stream in, a simulated N-worker replay of what has arrived so far checkpoints its progress at future_telling_checkpoint × cutoff_time, and the neighbour is rejected outright once that checkpoint is significantly worse than the incumbent’s own.

The simulation is deliberately decoupled from real wall-clock time and real cores: — it replays per-instance results against future_telling_cores virtual workers (list-scheduling: each result goes to whichever virtual worker is currently least busy, in the order real results actually arrive), so the checkpoint’s sharpness is a free parameter independent of how many real workers this run happens to use. Note that a sharper signal (a larger future_telling_cores) is not free in wall time: every virtual worker has to individually accumulate future_telling_checkpoint × cutoff_time of assigned work before the checkpoint matures, and the supply of real results feeding that is capped by real cores: — doubling future_telling_cores roughly doubles how many real results are needed, and so how long maturity actually takes.

A checkpoint rejection is counted in the run summary’s future_telling_rejected, separate from capped (above) — unlike a capped score, a rejected neighbour leaves no “the good one might have been here” trace, so treat a suspicious-looking result as a reason to re-run with future_telling: false before trusting it.

📈 Iterative deepening

Iterative deepening (iterative_deepening: true) runs ILS in multiple phases with an exponential schedule rather than a single run. Early phases use a small fraction of the training instances and a short per-run cutoff — just enough to quickly filter the search space and find a good starting point. Later phases gradually increase the instance count, cutoff time, and per-phase budget, refining the best region found so far. The incumbent from each phase seeds the next, so early exploration and late refinement share information.

Three growth factors control the schedule:

All three default to 0.5, giving an approximate geometric doubling schedule. The timeout values are cumulative deadlines measured from the start of iterative deepening, not independent budgets added together. Each phase gets the time remaining before its deadline.

Iterative deepening is most useful when the training set is large (hundreds of instances) and the cutoff time is long (tens of seconds), making a full-budget single run prohibitively slow at the start.

🎛️ Parameter file format

Parameter files (.params) describe the configuration space: which parameters exist, their domains, defaults, conditional activation, and forbidden combinations.

RamParILS supports the discrete parameter syntax used by the original Ruby ParamILS implementation. Continuous ranges and other ParamILS variants are not supported; enumerate every allowed value explicitly.

🔢 Discrete parameters

name {val1, val2, val3, ...} [default]

Example:

alpha {1.01, 1.066, 1.126, 1.189, 1.256, 1.326, 1.4} [1.189]
rho   {0, 0.17, 0.5, 1}                               [0.5]

Values are always strings. Numeric values are parsed by the target algorithm.

The default must be a member of the domain. A file whose default is not listed is rejected at load time with the offending line, rather than silently starting somewhere unexpected:

Error: line 4: default '0.03' not in domain ["0.0", "0.01", "0.05", "0.1", "0.2"] for param 'wp'

🔀 Conditional parameters

A conditional parameter is only active (included in the command line) when its parent has a specific value:

child {val1, val2} [default] | parent in {allowed1, allowed2}

Example:

noise_type {random, walk} [random]
noise_param {0.0, 0.1, 0.5} [0.1] | noise_type in {walk}

noise_param is only passed to the algorithm when noise_type = walk. Otherwise it is omitted from the command line.

Conditions resolve transitively: a parameter whose parent is itself conditional is inactive whenever the parent is, so a chain a -> b -> c needs no restatement of a in c’s condition.

⛔ Forbidden combinations

A forbidden combination prevents specific joint assignments from being evaluated:

{param1=val1, param2=val2, ...}

Example:

{alpha=1.01, rho=0}

Any configuration where alpha=1.01 and rho=0 simultaneously is skipped during search.

💬 Comments

Lines starting with # and trailing #... are ignored:

# This is a comment
alpha {1.01, 1.189} [1.189]   # inline comment

🧩 Full example

# SAPS parameters
alpha {1.01, 1.066, 1.126, 1.189, 1.256, 1.326, 1.4} [1.189]
rho   {0, 0.17, 0.5, 1}                               [0.5]
ps    {0.0, 0.01, 0.05, 0.1, 0.2, 0.5}                [0.1]
wp    {0.0, 0.01, 0.03, 0.05, 0.1, 0.2}               [0.03]

# Forbidden: degenerate case
{alpha=1.01, rho=0}

🧠 Designing a space

The syntax above is the easy half. What follows is what a space costs to search, and it is the part that decides whether a tuning run finds anything.

A domain is a neighbourhood cost, paid every descent

The neighbourhood of a configuration is every configuration differing in exactly one parameter, so a parameter contributes |domain| - 1 neighbours to every step of every local search. A five-valued parameter costs four; a boolean costs one. Perturbation draws from that neighbourhood too, so the five-valued parameter is also perturbed four times as often — which looks like the search finding it important when it is only finding it sampled. Do not read “parameters changed by improving moves” as an importance ranking.

Trim a domain to the values that mean different things. Where a response is smooth and unimodal a coarse ladder loses nothing; where it is a spike or non-monotone, resolution is load-bearing and trimming can hide the optimum.

Declare conditionals — they are free, and their absence is not

The cache key is a hash of the active configuration. Declaring child | parent in {...} is therefore not documentation: it collapses every setting of an inactive child into one cache entry. Leave the condition out and the search evaluates all of them, gets identical scores, and reads the result as a plateau — the same symptom a dead parameter produces, and indistinguishable from it without looking at the target algorithm’s own statistics.

The rule that follows: any option that gates whether another option is read must be declared as that option’s parent. This includes gates that are not obviously conditional from the outside — an option that skips constructing a component silently disables every option that component consumes.

Conditionals, not forbidden clauses, for combinations that merely mean something else

A forbidden combination removes a configuration from the space. Use it when the combination is genuinely invalid or degenerate — when it duplicates another configuration reachable by a different route, for instance. Use a condition when the combination is legal and runs, but makes the child irrelevant. The two are not interchangeable: forbidding shrinks the space, conditioning shrinks the space and the number of evaluations.

Watch what is unreachable from the starting configuration

A parameter behind a guard that is off in the starting configuration cannot move until the search first flips that guard — and the guard is flipped alone, with its dependents wherever they happen to sit. If the guard does not pay at its dependents’ defaults, a first-improvement descent rejects it and the whole sub-space stays unreachable at any budget. Nothing in the search can recover from that, because while the guard is off the cache has collapsed every setting of the dependents to a single entry, so there is no information about them to learn from.

Practical consequences:

• prefer spaces in which everything is reachable from the starting configuration;
• when a guarded sub-space matters, evaluate it directly rather than hoping the search enters it — enumerating a small sub-cube offline is cheap and tells you whether it is bad or merely badly initialised;
• treat a parameter that is inactive at the default as far more expensive than its domain size suggests.

Verify that a parameter does anything at all

A parameter that parses, reaches the command line, and changes nothing is the most expensive mistake available here: it never errors, and the symptom — whole neighbourhoods scoring identically — reads as a plateau. Before adding an option to a space, run the target algorithm at two extreme values and confirm its own counters move. Structural checks cannot catch this: the parameter is active by all of them.

🔌 Solver wrapper protocol

RamParILS never talks to the target algorithm directly — every evaluation goes through a wrapper: a small executable that translates a -name value parameter list into the algorithm’s real command line, runs it, and reports back over stdout in a fixed text format. The wrapper is the only thing that needs to know how to invoke the algorithm; RamParILS itself only ever speaks this protocol.

Two real wrappers ship as worked examples and are the reference to copy from: examples/primo/primo_wrapper.py (the primo QF_LRA solver, via solverpy.solver.smt.primo) and examples/eprover/eprover_wrapper.py (the E prover, via solverpy.solver.atp.eprover). Both are Python and use SolverPy to run and parse the underlying solver, but nothing about the protocol requires either — a wrapper is any program the shell can run.

📥 Invocation

For each evaluation, RamParILS runs:

<algo> <instance> <cutoff_time> -param1 val1 -param2 val2 …

• <algo> — the command from the scenario’s algo field, e.g. "python3 primo_wrapper.py"
• <instance> — path to the instance file
• <cutoff_time> — per-run time limit in seconds
• -param val pairs — the active parameters (per the parameter file’s conditionals), in alphabetical order by name

The complete command is passed to sh -c. Scenario files and parameter values must therefore be trusted, and wrappers should avoid paths or values that need shell quoting.

Example, resolved from algo: "python3 primo_wrapper.py":

python3 primo_wrapper.py /data/QF_LRA/inst1.smt2 30.0 -lra_model_phase true -theory_phase polarity

📤 Result line

The wrapper must print one result line to stdout:

#%# RamParIls #%# <status>, <runtime>, <quality>[, <runhash>]

The line may appear anywhere in stdout; everything else on stdout and stderr is ignored (but still worth printing — it is what lands in the debug/error logs when a run needs debugging). RamParILS stores status for reporting but does not interpret it when scoring; it is the wrapper’s own contract with itself. If no valid result line is found at all, RamParILS synthesizes one: status UNKNOWN, runtime cutoff_time, quality 10000000. UNKNOWN results are excluded from the persistent cache and logged to the run’s error log — the wrapper can, and for real crashes should, emit this itself; see below.

Examples, by solver status vocabulary

A wrapper’s status values are whatever the underlying solver reports — RamParILS doesn’t constrain the vocabulary, only how the two special outcomes (success, UNKNOWN) are used. Two worked families, matching the two example wrappers:

SMT (primo_wrapper.py, via SolverPy’s smt status plugin) — success is sat / unsat; unknown is a real, cacheable non-success answer distinct from a crash:

#%# RamParIls #%# sat, 1.234500, 0.0, 3f9a1c7b2e6d4085
#%# RamParIls #%# unsat, 0.087200, 0.0, 9c1e0a2f7b6d5443
#%# RamParIls #%# unknown, 30.000000, 10000000.0
#%# RamParIls #%# UNKNOWN, 30.000000, 10000000.0

TPTP/SZS (eprover_wrapper.py, via SolverPy’s tptp status plugin) — success is Theorem / Unsatisfiable / Satisfiable / CounterSatisfiable / ContradictoryAxioms; ResourceOut, Timeout and GaveUp are real non-success answers:

#%# RamParIls #%# Theorem, 4.812000, 0.0, 812babf67d10cf3d
#%# RamParIls #%# Unsatisfiable, 0.930000, 0.0, e74b8847f11fb0e8
#%# RamParIls #%# ResourceOut, 30.000000, 10000000.0
#%# RamParIls #%# GaveUp, 30.000000, 10000000.0
#%# RamParIls #%# UNKNOWN, 30.000000, 10000000.0

Note what both families share: only a success line carries a runhash, and every non-success line — real or UNKNOWN — charges the full cutoff_time, never the solver’s actual elapsed time. Both are deliberate, not incidental; see the two subsections below.

⏱️ PAR1 — a failure must never look cheap

runtime on a non-success line must be cutoff_time, not whatever time the process actually took — including a crash that failed in milliseconds. This is the standard PAR1 (penalized average runtime, ×1) convention: a run scored on run_obj: runtime treats a lower number as better, so a wrapper that reports a crash’s true near-instant runtime makes crashing look like the best possible outcome, and the search climbs toward configurations that reliably fail fast instead of ones that actually solve instances.

if status in solver.success:
    runtime = result.get("runtime", cutoff)   # real elapsed time
else:
    runtime = cutoff                          # PAR1: always the full budget, however it failed

This was a real bug, not a hypothetical: an early version of eprover_wrapper.py reported real elapsed time unconditionally, and a batch of invalid parameter values (below) made ~43% of evaluations fail near-instantly — all scoring better than genuine solves.

🆘 UNKNOWN — a genuine crash is not a new status

When the wrapper itself cannot produce a real result — the solver binary is missing, an argument was rejected, an exception was raised before the solver could even start — report it as status UNKNOWN, reusing RamParILS’s own sentinel rather than inventing something like "error" or "CRASH". UNKNOWN is the only status RamParILS treats specially:

• it is written to the run’s error log (log_crash), which is otherwise the one place a human would notice something went wrong;
• it is excluded from the persistent cache — a wrapper-side crash is not a fact about the configuration and must not be remembered as one.

An invented status (say, "ERROR") gets neither: RamParILS doesn’t recognise it, so it is cached as an ordinary, cacheable, permanent-looking result, and nothing is logged anywhere. This is exactly the failure a real run hit: two stale parameter values made the solver exit non-zero on a large fraction of evaluations, and because the wrapper reported them under a made-up status, every one of those “crashes” was silently cached as a legitimate outcome and the error log — the only place that would have shown it — stayed empty for the whole run.

try:
    result = solver.solve(instance, strategy)
except (KeyError, OSError, ValueError) as error:
    print(f"wrapper error: {error}", file=sys.stderr)
    status, runtime, quality, runhash = "UNKNOWN", cutoff, FAILURE_QUALITY, ""
else:
    status = result.get("status", "UNKNOWN") if solver.valid(result) else "UNKNOWN"
    # ... success/PAR1 branch as above ...

A genuine solver-reported failure (ResourceOut, GaveUp, SMT’s unknown, …) is not UNKNOWN — it keeps its real status and stays cached, because it is a fact about that configuration on that instance, reproducible on a re-run. UNKNOWN means specifically “the wrapper could not get an answer,” not “the answer was negative.”

#️⃣ The optional runhash field

A fourth, optional field carries a runhash: an 8-byte (16 hex digit) fingerprint of the solver’s own internal work on this instance — a hash over a selected subset of the solver’s own result counters (RunHash in SolverPy), independent of wall-clock runtime. Two runs of the same solver build on the same instance that did byte-identical internal work produce the same runhash; a parameter that changed nothing observable produces the same runhash as the run without it, which is exactly the signal needed to catch a structurally dead parameter — one that parses, reaches the command line, and changes nothing, which otherwise shows up only as an unexplained plateau in the search (see Designing a space).

Rules for emitting it:

• only on a success line. A crashed or capped run has no solver counters to hash — hashing an empty/default selection would produce a fixed constant that reads as “identical behaviour” between runs that share nothing but having produced no data;
• 16 lowercase hex digits, no 0x prefix;
• omit the field entirely (not an empty value) when not applicable — the trailing comma and value are absent, not blank.

ramparils stores it per result (nullable, so old caches without it still open) and XORs it across a descent’s evaluated neighbours for a per-round fingerprint; ramparils db status and ramparils db runhashes export it for offline analysis (an external group-runhashes.py script groups strategies that produced the same runhash).

🆚 --version

Before the first evaluation, RamParILS runs <algo> --version and refuses to start unless it succeeds — this is the fix for a run that silently spent 24 hours tuning against a solver binary that was never on PATH, reporting nothing wrong because every evaluation quietly “timed out” instead of failing to launch. The wrapper must:

• exit 0 when it could reach the inner solver, non-zero otherwise;
• print its own version, then the inner solver’s own --version output verbatim — or, if the solver could not be reached, a <solver> MISSING placeholder line in its place, keeping the block’s shape the same either way so the trailing line is always supports:;
• end with a line supports: <feature> <feature> … — space-separated keywords naming what this wrapper implements. version itself must always be listed; RamParILS checks for it and refuses to start if it’s absent, so a wrapper that answers --version at all but omits the keyword is treated the same as one that doesn’t answer it.

RamParILS logs the whole --version block once, at startup, separated from the per-instance solver stats. This is what lets a run’s own log attribute its results to an exact solver build — primo --version prints primo 0.1.0 for every build ever made, so without this a build mismatch across two runs is invisible until someone compares scores and can’t explain the gap.

Reference implementation (primo_wrapper.py):

$ primo_wrapper.py --version
primo_wrapper.py 0.3.0
primo 0.1.0 (git b3c4188)
supports: version runhash params

With the solver unreachable — the wrapper still prints the full block, but exits non-zero, so RamParILS refuses to start rather than running for hours against a solver that was never there:

$ primo_wrapper.py --version; echo "exit: $?"
primo_wrapper.py 0.3.0
primo MISSING
supports: version runhash params
exit: 1

🧩 Full example — the crash/success branch

The essential shape, distilled from eprover_wrapper.py’s main():

try:
    result = solver.solve(instance, strategy)
except (KeyError, OSError, ValueError) as error:
    print(f"wrapper error: {error}", file=sys.stderr)
    status, runtime, quality, runhash = "UNKNOWN", cutoff, FAILURE_QUALITY, ""
else:
    valid = solver.valid(result)
    status = result.get("status", "UNKNOWN") if valid else "UNKNOWN"
    if status in solver.success:
        runtime = result.get("runtime", cutoff)
        quality = 0.0
        runhash = f", {result['runhash']:016x}"
    else:
        runtime = cutoff          # PAR1
        quality = FAILURE_QUALITY
        runhash = ""

print(f"#%# RamParIls #%# {status}, {runtime:.6f}, {quality:.1f}{runhash}")

Three rules, all visible in this shape and all covered above: a crash is UNKNOWN, not an invented status; every non-success line — crash or genuine failure alike — charges the full cutoff; and runhash is present if and only if status is a success.

💬 Design notes

• --params and dry-run inspection. Because --params resolves a parameter set to a command line without running anything, it’s the fastest way to sanity-check a parameter file against the actual wrapper: primo_wrapper.py --params -lra_model_phase true prints exactly what the solver will see, catching a typo’d flag name before it costs a single evaluation.
• Prefer reusing UNKNOWN over adding a wrapper-specific error status. It is not a stylistic preference — an invented status silently opts a whole failure class out of both the error log and cache exclusion, and the failure is invisible until a human notices the numbers don’t add up, which is what actually happened. Reach for a new status only when it’s a genuine outcome the solver itself reports.
• Verify a parameter’s domain against the real binary, not an inherited one. The 43%-error incident above was two stale values (valid in an older, different codebase’s domain, rejected by the version actually installed) — eprover -W none / -G none printed the accepted-values list as part of a “wrong argument” error, and diffing that against the parameter file’s domain found both. Cheap to check before trusting a domain copied from elsewhere.

📖 Glossary

Active parameter A parameter that is included in the solver invocation for a given configuration. Conditional parameters are only active when their parent parameter has the required value; inactive parameters are omitted from the command line entirely.

Adaptive capping (see also: pruning, capped score, gated round) Early stopping once a candidate has spent the whole budget beating the incumbent allows: partial_sum > bound_multiplier × incumbent_score × n_instances. Costs never go down, so this proves the final score exceeds the bound — capping never discards a configuration that would have been accepted. Controlled by the pruning and bound_multiplier scenario fields.

Capped score The value a capped evaluation yields: a mean over only the instances that finished before the cap fired. Those are the fastest, so it understates the true score — it is a lower bound, not a measurement. Logged with a leading > and the count it covers, >2.698475 (312/473). Two capped scores cover different, differently biased prefixes and must not be compared to each other.

Checkpoint (see also: future-telling) An early, simulated read of a neighbour’s progress, taken at future_telling_checkpoint × cutoff_time of virtual replay time across future_telling_cores virtual workers. Scored as a count: how many of the round’s instances are not yet confirmed solved (runtime < cutoff_time) by that horizon — lower is better, like every other score in RamParILS. Only computed once the round’s instance count exceeds future_telling_cores; below that, every virtual worker sits idle and the checkpoint can never mature before the real evaluation is already complete, so nothing is built at all.

Configuration A complete assignment of values to all parameters in the parameter space. Also called a strategy in the context of solver portfolios. Represented internally as {name → value} string maps.

Conditional parameter A parameter whose domain is only meaningful when a parent parameter has a specific value. Declared in the .params file as child {…} [default] | parent in {val}. Conditional parameters that are inactive are omitted from the solver command line.

Cutoff time (cutoff_time) The per-run time limit in seconds passed to the target algorithm. The solver wrapper is expected to respect this limit and report TIMEOUT if reached. Adaptive capping uses this as the ceiling for individual run runtimes.

Dominance (FocusedILS) In the current implementation, configuration θ₁ dominates θ₂ when it has been evaluated at at least the same fidelity and has a strictly lower aggregate score. Ties do not count as improvements — this is what lets the fidelity grow when the incumbent survives a tie instead of being replaced endlessly by equal-scoring challengers.

The acceptance criterion is the one exception: it resolves ties in favour of the challenger, so the ILS home base can cross plateaus and drift away from a basin it cannot improve on while the incumbent stays put. ParamILS spells the two variants dominates(θ₁, θ₂, equalIsBetter).

Home base (ILS) The local optimum the next perturbation starts from — ParamILS’s last_ils_state. Distinct from the incumbent: the incumbent is the best configuration found, the home base is where the search currently is. It is replaced by the new local optimum whenever that one is at least as good, and, like the incumbent, is re-measured whenever the fidelity grows. Replacements are logged as ils: new home base: with the parameter diff against the previous one. Only the home base is perturbed, so a home base that stops moving turns the ILS into repeated random restarts from a fixed ball however the incumbent behaves — which is what the log lets you check.

Fidelity The number of leading training instances used to score each configuration. FocusedILS starts at initial_fidelity and grows by fidelity_step when the incumbent survives a challenge. Instances are taken in list order, after instance_shuffle (on by default) reorders the list once at the start of the run. See also: instance shuffle.

Forbidden combination A joint assignment of parameter values that is excluded from the search. Declared in the .params file as {param1=val1, param2=val2}. Any configuration containing a forbidden combination is skipped during neighbourhood exploration.

Future-telling (see also: checkpoint, adaptive capping) An opt-in (future_telling: true), heuristic early rejection of a BLS neighbour: while its real per-instance results stream in, a simulated N-worker replay is checkpointed at future_telling_checkpoint × cutoff_time, and the neighbour is rejected outright once that checkpoint is significantly worse than the incumbent’s own. Unlike adaptive capping, this is not a proof — it can reject a configuration that would have gone on to win — which is why it defaults to off. See Algorithm.

Gated round A round whose starting configuration was capped and which then accepted no move: every neighbour that did not finish under the bound was invisible, so the round produced no search at all. Counted in the end-of-run ils: summary line. The rate differs sharply between a small perturbation and a fresh random draw, so it belongs beside any comparison of two approaches.

Incumbent The best configuration found so far during the ILS run. Updated whenever a new configuration has a strictly lower aggregate score at the required fidelity. The final incumbent is returned as the result.

Instance A benchmark problem on which the target algorithm is evaluated. Passed as a file path to the solver wrapper. RamParILS evaluates configurations across the training instance set to estimate generalisation performance.

Instance shuffle (instance_shuffle, instance_shuffle_seed) A one-time, deterministic reordering of the instance list, applied right after instance IDs are assigned and before anything else runs. On (true) by default, which changes real evaluation order for every scenario that doesn’t opt out — not just ones using future-telling. Decorrelates FocusedILS’s fidelity-growth prefix from any difficulty ordering already present in the instance file; never affects which instance ID a path is assigned.

Iterated Local Search (ILS) The search algorithm at the core of RamParILS. Alternates between local search (greedy improvement within the neighbourhood) and perturbation (random escape from a local optimum). See Algorithm for a full description.

Local optimum A configuration whose entire neighbourhood contains no strictly better configuration. ILS escapes local optima via perturbation rather than accepting them as the final answer.

Neighbourhood The set of all configurations that differ from the current configuration in exactly one parameter value. Local search explores the neighbourhood at each step, evaluating all neighbours in parallel.

Objective What the tuner is trying to optimise. run_obj: runtime minimises the mean (or median) solver runtime across instances; run_obj: quality minimises the mean (or median) numeric cost returned by the solver. See also: overall objective.

Overall objective (overall_obj) How per-instance results are aggregated into a single scalar for comparison. mean is sensitive to all instances including outliers; median is more robust but ignores magnitude differences. Note that adaptive capping always tests a running sum, so a median run prunes on a statistic it does not score — prefer pruning: false there.

Parameter space The set of all configurations defined by the .params file: parameter names, discrete domains, defaults, conditional activations, and forbidden combinations. RamParILS searches this space to find a good configuration.

Perturbation A random walk of perturbation_strength steps applied to the current local optimum to escape it and seed the next local search. Each step randomly changes one parameter to a uniformly sampled value from its domain. Larger values jump further in the space.

Pruning (see also: adaptive capping, capped score) Shorthand for adaptive capping: early termination once a candidate has spent its configured budget. Enabled by default (pruning: true).

Run objective (run_obj) What a single solver invocation measures: runtime (wall-clock seconds) or quality (a scalar cost returned by the solver). Both objectives are minimised.

Solver wrapper A script or executable that invokes the target algorithm with a given instance and parameter setting, then prints a result line in RamParILS format. See Solver protocol for the exact interface.

Strategy Synonym for configuration, commonly used in the context of automated reasoning solver portfolios (e.g., Grackle). A strategy is a complete parameter setting that defines the solver’s behaviour.

Strategy hash A compact fingerprint (64-bit integer) of the active configuration used as part of the cache key. It is computed from the sorted active param=value pairs, so inactive conditional values do not create duplicate cache entries. The hash is not guaranteed to remain portable across Rust versions.

Tuner timeout (tuner_timeout) The total wall-clock budget for the RamParILS run in seconds. Once elapsed, no new evaluations are started and the incumbent is returned. Distinct from cutoff_time, which limits individual solver runs.