🐏 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.2.0 (2026-08-19) · changelog · sources and issues on GitHub · installation

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

📦 What’s new in 0.2.0

• 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.

Full detail, including the earlier releases, is in the changelog.

💡 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.

🚀 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
• 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

This 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

Added

• An end-of-run ils: summary line reporting rounds / searched / gated / incumbents / evals / capped. 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.

Fixed

• 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.

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.2.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.2.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.2.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
cache_db:              ":memory:"    # use a file path to persist across runs
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 instance_file, not a random sample. Order the file deliberately or shuffle it before a run when early prefixes should represent the full training set.

📈 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

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. Put a representative ordering in the list; RamParILS does not shuffle it automatically.

📤 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.

🧠 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

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.

📈 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 (work26/expericon/scripts/group-runhashes.py 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.

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 and are not shuffled.

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.

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.

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.