Skip to content

Commit 015b1c6

Browse files
isPANNclaude
andcommitted
Fix ILP i32->bool cast overhead: use size-field name num_vars, not getter alias (#1080)
Root cause of the `pred path MinimumFeedbackVertexSet ILP` bug (asymptotic `num_vars` composed to `O(num_variables)` instead of `O(num_vertices)`): the `ILP<i32> → ILP<bool>` binary-encoding cast declared its overhead as `num_vars = "31 * num_variables"`. ILP's size field is named `num_vars`; `num_variables()` is only a getter *alias* for it. The `#[reduction]` macro validates overhead variables against getter *methods*, so the alias compiled, and both instance-mode sizing (`evaluate_output_size` calls the getter) and raw-overhead Big-O rendering resolve it — the mistake was invisible there. But asymptotic growth composition (`GrowthLabel::extend`) threads size-field *names*: the label key at the ILP node is `num_vars`, so the variable `num_variables` was unmapped and leaked through unchanged as `num_vars = O(num_variables)`. The path's arrow display had also masked this by collapsing the hidden `ILP/i32 → ILP/bool` cast step. Fix: `31 * num_variables` → `31 * num_vars` (semantically identical — 31 bits per integer variable — and numerically unchanged, since both getters return `num_vars`). Effects: `MFVS → ILP` now composes `num_vars = O(num_vertices)`. `MVC → ILP` drops from 3 to 2 front paths — the corrected feedback-vertex-set route (`num_constraints = O(num_edges + num_vertices), num_vars = O(num_vertices)`) is now correctly Pareto-dominated by the direct route and pruned. Test: `test_asymptotic_front_uses_only_source_variables_mfvs_ilp` pins `num_vars = O(num_vertices)` and asserts every composed field's growth references only MinimumFeedbackVertexSet's own size variables — a general "source-variables-only" invariant on the front label. Note: this is one instance of a getter-alias-vs-field-name mismatch. A separate, broader class of leaks remains in other reductions (e.g. `ClosestVectorProblem`'s `num_encoding_bits` and `CircuitSAT`'s `tseitin_num_vars`/`tseitin_num_clauses`, which surface in KSat→QUBO); those are genuine field-name inconsistencies between a node's incoming and outgoing reductions, outside the growth-composition logic, and are left for separate scoping. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01EgxSbn5gwizTBkC22eyWXR
1 parent ad2c050 commit 015b1c6

2 files changed

Lines changed: 72 additions & 1 deletion

File tree

src/rules/ilp_i32_ilp_bool.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -264,7 +264,7 @@ impl ReductionResult for ReductionIntILPToBinaryILP {
264264
}
265265

266266
#[reduction(overhead = {
267-
num_vars = "31 * num_variables",
267+
num_vars = "31 * num_vars",
268268
num_constraints = "num_constraints",
269269
})]
270270
impl ReduceTo<ILP<bool>> for ILP<i32> {

src/unit_tests/rules/pareto.rs

Lines changed: 71 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -714,3 +714,74 @@ fn test_asymptotic_front_dedups_by_growth_vector() {
714714
front.len()
715715
);
716716
}
717+
718+
/// A composed front label must express every size field's growth purely in the
719+
/// **source problem's** own size variables — never in a downstream getter alias or an
720+
/// intermediate node's field name.
721+
///
722+
/// Regression for the `MinimumFeedbackVertexSet → ILP` bug: the `ILP<i32> → ILP<bool>`
723+
/// binary-encoding cast declared its overhead as `num_vars = "31 * num_variables"`,
724+
/// referencing the getter *alias* `num_variables()` instead of ILP's size-field *name*
725+
/// `num_vars`. Instance mode and raw-overhead rendering both resolve the getter, so the
726+
/// mistake was invisible there — but growth composition threads field *names*, so the
727+
/// alias was unmapped and leaked through as `num_vars = O(num_variables)` instead of
728+
/// the correct `O(num_vertices)`.
729+
#[test]
730+
fn test_asymptotic_front_uses_only_source_variables_mfvs_ilp() {
731+
let graph = ReductionGraph::new();
732+
let src_v = graph
733+
.default_variant_for("MinimumFeedbackVertexSet")
734+
.or_else(|| {
735+
graph
736+
.variants_for("MinimumFeedbackVertexSet")
737+
.into_iter()
738+
.next()
739+
})
740+
.expect("MinimumFeedbackVertexSet registered");
741+
let dst_v = graph
742+
.default_variant_for("ILP")
743+
.or_else(|| graph.variants_for("ILP").into_iter().next())
744+
.expect("ILP registered");
745+
746+
let front = graph.asymptotic_front(
747+
"MinimumFeedbackVertexSet",
748+
&src_v,
749+
"ILP",
750+
&dst_v,
751+
ReductionMode::Witness,
752+
);
753+
754+
// The direct route (MFVS → ILP/i32 → ILP/bool; the ILP variants collapse in the
755+
// deduplicated node-name view) is the one exercised by the fixed cast.
756+
let (_, label) = front
757+
.iter()
758+
.find(|(p, _)| p.type_names() == ["MinimumFeedbackVertexSet", "ILP"])
759+
.expect("direct MinimumFeedbackVertexSet -> ILP path");
760+
761+
// The size fields of MinimumFeedbackVertexSet — the only variables any composed
762+
// growth is allowed to mention.
763+
let allowed = ["num_arcs", "num_vertices"];
764+
for (field, growth) in label.fields() {
765+
let expr = growth
766+
.to_expr()
767+
.unwrap_or_else(|| panic!("field {field} should have a bounded growth"));
768+
for var in expr.variables() {
769+
assert!(
770+
allowed.contains(&var),
771+
"field `{field}` growth O({expr}) references `{var}`, which is not a \
772+
MinimumFeedbackVertexSet source variable {allowed:?}",
773+
);
774+
}
775+
}
776+
777+
// The previously-buggy field, pinned to the correct source-variable Big-O.
778+
let num_vars = label
779+
.fields()
780+
.get("num_vars")
781+
.expect("ILP has a num_vars size field");
782+
assert_eq!(
783+
num_vars.to_expr().unwrap().to_string(),
784+
"num_vertices",
785+
"ILP num_vars must compose to O(num_vertices), not the getter alias num_variables"
786+
);
787+
}

0 commit comments

Comments
 (0)