Background
The asymptotic Pareto path search (#1080) composes each reduction's overhead in the growth domain, threading size-field names. When a reduction's overhead references a variable that is not a declared size field produced by the node's incoming reductions (typically a derived getter used as an overhead variable), that variable is unmapped and leaks into the composed Big-O as a spurious free symbol. pred path then prints non-source-variable bounds.
The narrow instance of this — the ILP num_variables() getter alias vs the num_vars field name — was already fixed in #1080 (commit 015b1c6e). This issue tracks the remaining, broader class.
Evidence (current main + #1080 branch)
pred path KSatisfiability QUBO (no --size) prints Big-O containing tseitin_num_vars, tseitin_num_clauses, num_encoding_bits — none of which are KSatisfiability's declared size variables (num_vars, num_clauses, num_literals).
Root causes (field-name inconsistency between a node's incoming and outgoing reductions):
- CircuitSAT:
src/rules/circuit_sat.rs (CircuitSAT → Satisfiability) overhead reads num_vars = "tseitin_num_vars" (a derived getter tseitin_num_vars()), and num_clauses = "tseitin_num_clauses". But the incoming SAT → CircuitSAT declares CircuitSAT's size as {num_variables, num_assignments}. Two disjoint naming schemes for the same node ⇒ tseitin_* are never produced by an incoming edge ⇒ they leak.
- ClosestVectorProblem:
src/rules/closestvectorproblem_qubo.rs (CVP → QUBO) reads a derived getter num_encoding_bits; incoming src/rules/subsetsum_closestvectorproblem.rs (SubsetSum → CVP) outputs only {ambient_dimension, num_basis_vectors} ⇒ num_encoding_bits leaks.
size_field_names(name) (src/rules/graph.rs) unions input_variable_names() across all reductions touching a node, so a node's field-name set is further polluted by inconsistent neighbors (e.g. KSatisfiability picks up register_sufficiency_padding, simultaneous_incongruences_num_incongruences).
This is not a bug in the growth-composition logic (it composes faithfully) — it is a data-quality inconsistency in the overhead declarations.
Objective
Normalize each problem's size-field naming so that, for every registered reduction:
- every variable referenced in the overhead is a declared size field of the source problem, and
- any derived quantity used in an overhead (e.g.
tseitin_num_vars, num_encoding_bits) is expressed in terms of the source's declared size fields.
Then composed asymptotic Big-O is always in the source problem's variables.
Verification
pred path KSatisfiability QUBO (no --size) prints, for each QUBO size field, an O(...) referencing only KSatisfiability's declared size variables (num_vars, num_clauses, num_literals) — no tseitin_*, num_encoding_bits, register_sufficiency_padding, simultaneous_incongruences_*.
- Generalize the existing
test_asymptotic_front_uses_only_source_variables_mfvs_ilp into a broad invariant test: for a representative set of source → target pairs, every composed front field's growth references only the source problem's declared size fields.
Negative control: on current main, pred path KSatisfiability QUBO output contains tseitin_num_vars (a non-source variable) — proving the leak exists before the fix.
Out of scope
Overhead formula/coefficient correctness (calibration) — that is a separate milestone issue. This issue is purely about size-field name consistency so composition stays in source variables.
Background
The asymptotic Pareto path search (#1080) composes each reduction's overhead in the growth domain, threading size-field names. When a reduction's overhead references a variable that is not a declared size field produced by the node's incoming reductions (typically a derived getter used as an overhead variable), that variable is unmapped and leaks into the composed Big-O as a spurious free symbol.
pred paththen prints non-source-variable bounds.The narrow instance of this — the ILP
num_variables()getter alias vs thenum_varsfield name — was already fixed in #1080 (commit015b1c6e). This issue tracks the remaining, broader class.Evidence (current
main+ #1080 branch)pred path KSatisfiability QUBO(no--size) prints Big-O containingtseitin_num_vars,tseitin_num_clauses,num_encoding_bits— none of which are KSatisfiability's declared size variables (num_vars,num_clauses,num_literals).Root causes (field-name inconsistency between a node's incoming and outgoing reductions):
src/rules/circuit_sat.rs(CircuitSAT → Satisfiability) overhead readsnum_vars = "tseitin_num_vars"(a derived gettertseitin_num_vars()), andnum_clauses = "tseitin_num_clauses". But the incomingSAT → CircuitSATdeclares CircuitSAT's size as{num_variables, num_assignments}. Two disjoint naming schemes for the same node ⇒tseitin_*are never produced by an incoming edge ⇒ they leak.src/rules/closestvectorproblem_qubo.rs(CVP → QUBO) reads a derived getternum_encoding_bits; incomingsrc/rules/subsetsum_closestvectorproblem.rs(SubsetSum → CVP) outputs only{ambient_dimension, num_basis_vectors}⇒num_encoding_bitsleaks.size_field_names(name)(src/rules/graph.rs) unionsinput_variable_names()across all reductions touching a node, so a node's field-name set is further polluted by inconsistent neighbors (e.g.KSatisfiabilitypicks upregister_sufficiency_padding,simultaneous_incongruences_num_incongruences).This is not a bug in the growth-composition logic (it composes faithfully) — it is a data-quality inconsistency in the overhead declarations.
Objective
Normalize each problem's size-field naming so that, for every registered reduction:
tseitin_num_vars,num_encoding_bits) is expressed in terms of the source's declared size fields.Then composed asymptotic Big-O is always in the source problem's variables.
Verification
pred path KSatisfiability QUBO(no--size) prints, for each QUBO size field, anO(...)referencing only KSatisfiability's declared size variables (num_vars,num_clauses,num_literals) — notseitin_*,num_encoding_bits,register_sufficiency_padding,simultaneous_incongruences_*.test_asymptotic_front_uses_only_source_variables_mfvs_ilpinto a broad invariant test: for a representative set ofsource → targetpairs, every composed front field's growth references only the source problem's declared size fields.Negative control: on current
main,pred path KSatisfiability QUBOoutput containstseitin_num_vars(a non-source variable) — proving the leak exists before the fix.Out of scope
Overhead formula/coefficient correctness (calibration) — that is a separate milestone issue. This issue is purely about size-field name consistency so composition stays in source variables.