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

    Fields

    No fields configured for issues without a type.

    Projects

    Status
    No status

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions