Skip to content

Normalize size-field names across reductions so composed asymptotic Big-O is always in source variables #1085

Description

@isPANN

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:

  1. every variable referenced in the overhead is a declared size field of the source problem, and
  2. 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

  1. 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_*.
  2. 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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    Status
    No status

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions