Tuning an existing configuration#
Start from a qualified baseline and a hypothesis: which mechanism should change, on which inputs, and what observation would reject it? The policy reference identifies option dependencies.
Check the parameter’s actual callers and effective route. Compare counters at two admissible values before adding it to a search space.
Keep training and evaluation inputs separate. Record the space, seed, objective, limits and optimizer version; budget both optimizer overhead and solver calls.
Use the existing irace or SMAC wrappers only for their supported spaces. A QF_UF parameter file is not an LRA configuration.
Re-evaluate the selected configuration against the unchanged baseline on the stated full evaluation set. Report family losses and unique solves as well as aggregate solved/PAR2 and paired times.
Run fresh configuration-specific fuzzing and separate SAT-model checks before accepting a default or headline performance claim.
Both wrappers check timeouts and process exit status before accepting an answer.
A timeout, signal termination, or nonzero exit costs twice the timeout (PAR2),
even if the process printed sat or unsat first. A normally completed wrong
answer retains the larger wrong-answer penalty. SMAC records stdout, stderr
and exit status in its target and validation CSV files. Set PRIMO_TUNE_LOG
for irace to retain exit status and a JSON-escaped output comment after each
run record. Timeout records use synthetic exit code 124; other runs retain
the observed process return code. Historical tuning records are unchanged; exclude abnormal exits
when interpreting older scores.
The B-014 repair has mocked-process regressions for post-answer errors, signal termination, timeouts and normally completed wrong answers. These tests do not qualify a solver configuration or replace the SLURM evaluation gates.
An inactive parameter consumes search budget without testing a mechanism. An average loss can still justify a portfolio lead if unique solves compensate for its scheduling cost, but it does not justify a new default. Record the accepted or rejected decision and all provenance through the experiment workflow.
The historical parameter inventory and complementarity investigation retain previous motivations and negative results. Recheck their preconditions instead of treating the old candidate list as a current recommendation.
Deferred tuning note: Boolean post-flattening#
Low priority; a potential tuning point, not a demonstrated migration
bottleneck. On the single QF_LIA input
nec-smt/large/getoption_group/prp-67-50.smt2, baseline and migrated-driver
profiles had nearly identical cost distributions and search counters. Disabling
Boolean post-flattening reduced clauses from 32.1 million to 4.6 million and
instrumented wall duration from about 54 to 30 seconds, while increasing SAT
conflicts. Both binaries returned unsat.
This is a case-specific lead about Boolean expansion. The GDB durations are not benchmark measurements, and the experiment does not establish a material migration regression or a worthwhile corpus-wide improvement. Record it for possible later tuning; no default change or follow-up experiment is scheduled. If revisited, first test whether an expansion-sensitive flattening policy helps a representative family without losing the benefits of flattening elsewhere. The profiling record retains the commands, jobs, counts and limitations. This prioritization does not alter the recorded migration acceptance results.