Background
Every #[reduction] declares an overhead — symbolic expressions documented as upper bounds on the target problem's size fields in terms of the source's. These formulas are hand-written, so they can be wrong. A formula that under-predicts has two costs: it misleads users reading pred path output, and it undermines the measured path search's symbolic pre-flight guard, which is only sound because formulas never under-predict. We want a way to calibrate each rule's declared overhead against what its reduction actually produces.
Objective (intentionally open)
Establish a mechanism to calibrate the declared overhead of each reduction rule against its real, measured output sizes, so mis-declared or under-predicting formulas are caught rather than trusted. The exact mechanism is not yet decided — this issue records the intent and the constraints it must satisfy, not a specific design.
Why this has to observe scaling, not a single point
The overhead is fundamentally an asymptotic scaling claim. Checking it on one small fixed instance can falsify gross errors (wrong field/variable, blatant under-prediction) but cannot verify the coefficient or the asymptotic order — a formula that is asymptotically too small can still pass at a tiny size and give false confidence. Any calibration that is worth trusting must observe how the measured size tracks the formula as instance size grows (e.g. the bound holding across a range of sizes, and the measured-vs-predicted ratio not diverging), rather than at a single canonical example.
Open questions (to resolve before implementing)
Status
Deferred. Not to be implemented until the calibration approach is decided.
Related
#107 (manual overhead/metadata review — this would mechanize part of it), and the measured Pareto search whose pre-flight guard this calibration underwrites.
Background
Every
#[reduction]declares anoverhead— symbolic expressions documented as upper bounds on the target problem's size fields in terms of the source's. These formulas are hand-written, so they can be wrong. A formula that under-predicts has two costs: it misleads users readingpred pathoutput, and it undermines the measured path search's symbolic pre-flight guard, which is only sound because formulas never under-predict. We want a way to calibrate each rule's declared overhead against what its reduction actually produces.Objective (intentionally open)
Establish a mechanism to calibrate the declared overhead of each reduction rule against its real, measured output sizes, so mis-declared or under-predicting formulas are caught rather than trusted. The exact mechanism is not yet decided — this issue records the intent and the constraints it must satisfy, not a specific design.
Why this has to observe scaling, not a single point
The overhead is fundamentally an asymptotic scaling claim. Checking it on one small fixed instance can falsify gross errors (wrong field/variable, blatant under-prediction) but cannot verify the coefficient or the asymptotic order — a formula that is asymptotically too small can still pass at a tiny size and give false confidence. Any calibration that is worth trusting must observe how the measured size tracks the formula as instance size grows (e.g. the bound holding across a range of sizes, and the measured-vs-predicted ratio not diverging), rather than at a single canonical example.
Open questions (to resolve before implementing)
src/example_db).Status
Deferred. Not to be implemented until the calibration approach is decided.
Related
#107 (manual overhead/metadata review — this would mechanize part of it), and the measured Pareto search whose pre-flight guard this calibration underwrites.