diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index 9980c4afe..d5909d575 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -15832,7 +15832,7 @@ The following reductions to Integer Linear Programming are straightforward formu #reduction-rule("BiconnectivityAugmentation", "ILP")[ Select candidate edges under the total budget and certify connectivity of both the original augmented graph and every vertex-deleted graph using bounded integral flow witnesses. ][ - _Construction._ Let $n$ be the vertex count, $m$ the number of base edges, and $p$ the number of candidate edges. Candidate $j$ has cost $w_j$, and the budget is $B$. Use `ILP` with an empty minimization objective and every variable bounded to $[0,1]$ through `IntegerVariable::binary()`. + _Construction._ Let $n$ be the vertex count, $m$ the number of base edges, and $p$ the number of candidate edges. Candidate $j$ has cost $w_j$, and the budget is $B$. Use `ILP` with an empty minimization objective and every variable bounded to $[0,1]$ through `IntegerVariable::binary()`. Selection variable $y_j$ has index $j$. Connectivity scenarios are $q in {0, dots, n}$: $q= 1$ be the smallest integer such that $abs(w_j) < 2^h$ for every candidate and $abs(B) < 2^h$. The source parameter `max_numeric_magnitude_bits` equals $h$. The budget row copies these values, and all other constraint and variable-bound magnitudes are at most one. Thus the target's `max_constraint_magnitude_bits` equals $h$, including signed budgets and empty candidate lists. ] #reduction-rule("BoundedComponentSpanningForest", "ILP")[ @@ -15922,7 +15924,7 @@ The following reductions to Integer Linear Programming are straightforward formu #reduction-rule("StrongConnectivityAugmentation", "ILP")[ Select candidate arcs under the budget and certify strong connectivity by sending flow both from a root to every vertex and back again. ][ - _Construction._ Let the base arcs be $A = {a_0, dots, a_(m-1)}$ with $a_i = (u_i, v_i)$, let the candidate arcs be $C = {c_0, dots, c_(p-1)}$ with $c_j = (s_j, t_j)$, and, when $n = |V| >= 1$, fix the root to be vertex $r = 0$. If $n <= 1$, return the empty feasible ILP. Use `ILP` with variables ordered as + _Construction._ Let the base arcs be $A = {a_0, dots, a_(m-1)}$ with $a_i = (u_i, v_i)$, let the candidate arcs be $C = {c_0, dots, c_(p-1)}$ with $c_j = (s_j, t_j)$, and, when $n = |V| >= 1$, fix the root to be vertex $r = 0$. Retain the budget constraint even when $n <= 1$. Use `ILP` with variables ordered as $(y_j)_j, (f^t_i)_(t,i), (bar(f)^t_j)_(t,j), (g^t_i)_(t,i), (bar(g)^t_j)_(t,j)$, where $f^t$ is the forward root-to-$t$ flow on base arcs, $bar(f)^t$ is the forward flow on candidate arcs, $g^t$ is the backward $t$-to-root flow on base arcs, and $bar(g)^t$ is the backward flow on candidate arcs. The indices are @@ -15964,6 +15966,8 @@ The following reductions to Integer Linear Programming are straightforward formu _Correctness._ ($arrow.r.double$) A strongly connected augmentation provides both directions of reachability between the root and every other vertex, hence all required flows. ($arrow.l.double$) If those flows exist for every vertex, then every vertex is reachable from the root and can reach the root, so the augmented digraph is strongly connected. _Solution extraction._ Output the binary candidate-arc selection vector $(y_a)$. + + _Numeric magnitude._ The source parameter `max_numeric_magnitude_bits` is the smallest $h >= 1$ for which every candidate weight and the budget are strictly below $2^h$. The budget row copies these values and the remaining constraint and variable-bound magnitudes are at most one, so the target's `max_constraint_magnitude_bits` equals $h$. ] // Matrix/encoding @@ -17828,6 +17832,8 @@ The following table shows concrete target-variable counts for example instances, _Correctness._ For $n < 3$, both instances are infeasible. For $n >= 3$, a source Hamiltonian circuit selects $n$ weight-1 edges forming a biconnected cycle of cost $n$. Conversely, a feasible target is connected and every vertex has degree at least two: a degree-zero vertex contradicts connectivity, and a degree-one vertex would be separated from the other surviving vertices by deleting its neighbor. The degree sum therefore forces at least $n$ selected edges. Positive costs and budget $n$ force exactly $n$ edges, all of cost 1. Every degree is exactly two, so connectivity makes these edges a single spanning cycle of the source. All partial selected-weight sums are at most the final sum for feasible targets; evaluation therefore preserves the budget test with exact integer arithmetic. _Solution extraction._ Validate the target certificate and require its evaluation to be `Or(true)` before decoding. Walk the selected cycle from vertex 0 to recover the circuit order. The negative sentinel has no feasible certificate. The target has at most $n+3$ vertices, no initial edges, and at most $n(n-1)/2$ candidates. + + _Numeric magnitude._ Candidate costs are at most two and the budget is $n$; for $n<3$, the fixed target has budget zero and no candidates. Thus the target's `max_numeric_magnitude_bits` is at most $n+1$, using only the source vertex count. ] #let hc_sca = load-example("HamiltonianCircuit", "StrongConnectivityAugmentation") @@ -17859,11 +17865,13 @@ The following table shows concrete target-variable counts for example instances, )[ Start with the empty digraph on $n$ vertices. Weight-1 candidate arcs correspond to edges of $G$; weight-2 arcs for non-edges. A budget-$n$ augmentation that achieves strong connectivity must select exactly $n$ weight-1 arcs forming a directed Hamiltonian cycle. ][ - _Construction._ Given $G = (V, E)$ with $n = |V|$. Build $D = (V, emptyset)$. For every ordered pair $(u, v)$ with $u != v$: candidate arc with weight 1 if ${u,v} in E$, else weight 2. Budget $B = n$. + _Construction._ Given $G = (V, E)$ with $n = |V|$. If $n<3$, output two isolated vertices, no candidate arcs, and budget zero; both source and target are infeasible. Otherwise build $D = (V, emptyset)$. For every ordered pair $(u, v)$ with $u != v$: candidate arc with weight 1 if ${u,v} in E$, else weight 2. Budget $B = n$. _Correctness._ ($arrow.r.double$) A Hamiltonian circuit gives $n$ directed arcs of weight 1 forming a strongly-connected cycle. ($arrow.l.double$) Strong connectivity needs $>= n$ arcs; budget $n$ forces all weight 1, hence all from $E$, forming a single $n$-cycle. _Solution extraction._ Follow unique successors from vertex 0 to recover the Hamiltonian permutation. + + _Numeric magnitude._ Candidate costs are at most two and the budget is $n$; the fixed target for $n<3$ has budget zero and no candidates. The target's `max_numeric_magnitude_bits` is therefore at most $n+1$. ] #let hc_sc = load-example("HamiltonianCircuit", "DecisionStackerCrane") diff --git a/src/models/graph/biconnectivity_augmentation.rs b/src/models/graph/biconnectivity_augmentation.rs index ce58f773f..391240d3b 100644 --- a/src/models/graph/biconnectivity_augmentation.rs +++ b/src/models/graph/biconnectivity_augmentation.rs @@ -181,6 +181,16 @@ impl BiconnectivityAugmentation { &self.budget } + /// Smallest h >= 1 bounding candidate-weight and budget magnitudes strictly by 2^h. + pub fn max_numeric_magnitude_bits(&self) -> u64 { + crate::types::max_numeric_magnitude_bits( + self.potential_weights + .iter() + .map(|(_, _, weight)| weight.to_sum()) + .chain(std::iter::once(self.budget.clone())), + ) + } + /// Get the number of vertices in the underlying graph. pub fn num_vertices(&self) -> usize { self.graph.num_vertices() @@ -251,6 +261,7 @@ where type Value = crate::types::Or; crate::problem_parameters![ + ("max_numeric_magnitude_bits", max_numeric_magnitude_bits), ("num_edges", num_edges), ("num_potential_edges", num_potential_edges), ("num_vertices", num_vertices), diff --git a/src/models/graph/strong_connectivity_augmentation.rs b/src/models/graph/strong_connectivity_augmentation.rs index 83c2c6cdf..5fbe8e943 100644 --- a/src/models/graph/strong_connectivity_augmentation.rs +++ b/src/models/graph/strong_connectivity_augmentation.rs @@ -124,6 +124,16 @@ impl StrongConnectivityAugmentation { &self.bound } + /// Smallest h >= 1 bounding candidate-weight and budget magnitudes strictly by 2^h. + pub fn max_numeric_magnitude_bits(&self) -> u64 { + crate::types::max_numeric_magnitude_bits( + self.candidate_arcs + .iter() + .map(|(_, _, weight)| weight.to_sum()) + .chain(std::iter::once(self.bound.clone())), + ) + } + /// Get the number of vertices in the base graph. pub fn num_vertices(&self) -> usize { self.graph.num_vertices() @@ -187,6 +197,7 @@ where type Value = crate::types::Or; crate::problem_parameters![ + ("max_numeric_magnitude_bits", max_numeric_magnitude_bits), ("num_arcs", num_arcs), ("num_potential_arcs", num_potential_arcs), ("num_vertices", num_vertices), diff --git a/src/rules/biconnectivityaugmentation_ilp.rs b/src/rules/biconnectivityaugmentation_ilp.rs index 5a90ee7b5..09f9ef368 100644 --- a/src/rules/biconnectivityaugmentation_ilp.rs +++ b/src/rules/biconnectivityaugmentation_ilp.rs @@ -75,16 +75,16 @@ impl ReductionResult for ReductionBiconnAugToILP { #[crate::aggregate_reduction(ilp_feasibility)] impl crate::rules::AggregateReductionResult for ReductionBiconnAugToILP {} -#[reduction( - transform = upper_bound { +#[reduction(transform = { + exact { + max_constraint_magnitude_bits = "max_numeric_magnitude_bits", + }, + upper_bound { num_vars = "num_potential_edges + 2 * num_vertices * (num_vertices + 1) * (num_edges + num_potential_edges)", num_constraints = "1 + num_vertices * (num_vertices + 1) * (2 * num_edges + 4 * num_potential_edges + num_vertices)", num_nonzeros = "(num_potential_edges + 2 * num_vertices * (num_vertices + 1) * (num_edges + num_potential_edges)) * (1 + num_vertices * (num_vertices + 1) * (2 * num_edges + 4 * num_potential_edges + num_vertices))", }, - unavailable = { - max_constraint_magnitude_bits = "candidate edge weights and the budget are not registered source parameters", - }, -)] +})] impl ReduceTo> for BiconnectivityAugmentation { type Result = ReductionBiconnAugToILP; diff --git a/src/rules/hamiltoniancircuit_biconnectivityaugmentation.rs b/src/rules/hamiltoniancircuit_biconnectivityaugmentation.rs index 654ee26f5..8a5b16a46 100644 --- a/src/rules/hamiltoniancircuit_biconnectivityaugmentation.rs +++ b/src/rules/hamiltoniancircuit_biconnectivityaugmentation.rs @@ -124,6 +124,7 @@ impl crate::rules::AggregateReductionResult #[reduction( transform = upper_bound { + max_numeric_magnitude_bits = "num_vertices + 1", num_vertices = "num_vertices + 3", num_edges = "0", num_potential_edges = "num_vertices * (num_vertices - 1) / 2", diff --git a/src/rules/hamiltoniancircuit_strongconnectivityaugmentation.rs b/src/rules/hamiltoniancircuit_strongconnectivityaugmentation.rs index 089159a34..cc621ea80 100644 --- a/src/rules/hamiltoniancircuit_strongconnectivityaugmentation.rs +++ b/src/rules/hamiltoniancircuit_strongconnectivityaugmentation.rs @@ -87,6 +87,7 @@ impl crate::rules::AggregateReductionResult #[reduction( transform = upper_bound { + max_numeric_magnitude_bits = "num_vertices + 1", num_vertices = "num_vertices + 2", num_arcs = "0", num_potential_arcs = "num_vertices * (num_vertices - 1)", diff --git a/src/rules/strongconnectivityaugmentation_ilp.rs b/src/rules/strongconnectivityaugmentation_ilp.rs index 8a76cd23e..ecbfed4a9 100644 --- a/src/rules/strongconnectivityaugmentation_ilp.rs +++ b/src/rules/strongconnectivityaugmentation_ilp.rs @@ -44,16 +44,16 @@ impl ReductionResult for ReductionSCAToILP { #[crate::aggregate_reduction(ilp_feasibility)] impl crate::rules::AggregateReductionResult for ReductionSCAToILP {} -#[reduction( - transform = upper_bound { +#[reduction(transform = { + exact { + max_constraint_magnitude_bits = "max_numeric_magnitude_bits", + }, + upper_bound { num_vars = "num_potential_arcs + 2 * num_vertices * (num_arcs + num_potential_arcs)", num_constraints = "1 + num_potential_arcs + 2 * num_arcs + 2 * num_vertices * num_potential_arcs + 2 * num_vertices * num_vertices", num_nonzeros = "(num_potential_arcs + 2 * num_vertices * (num_arcs + num_potential_arcs)) * (1 + num_potential_arcs + 2 * num_arcs + 2 * num_vertices * num_potential_arcs + 2 * num_vertices * num_vertices)", }, - unavailable = { - max_constraint_magnitude_bits = "candidate arc weights and the budget are not registered source parameters", - }, -)] +})] impl ReduceTo> for StrongConnectivityAugmentation { type Result = ReductionSCAToILP; diff --git a/src/unit_tests/reduction_graph.rs b/src/unit_tests/reduction_graph.rs index 298c2c5e9..032f525d6 100644 --- a/src/unit_tests/reduction_graph.rs +++ b/src/unit_tests/reduction_graph.rs @@ -1589,3 +1589,68 @@ fn incoming_flow_predictions_compose_to_qubo_and_recover_witnesses() { ); } } + +fn check_augmentation_predictions_through_qubo() { + let graph = ReductionGraph::new(); + let path = ReductionPath { + steps: [ + ( + HamiltonianCircuit::::NAME, + HamiltonianCircuit::::variant(), + ), + (A::NAME, A::variant()), + (ILP::::NAME, ILP::::variant()), + (QUBO::::NAME, QUBO::::variant()), + ] + .into_iter() + .map(|(name, variant)| ReductionStep { + name: name.into(), + variant: ReductionGraph::variant_to_map(&variant), + }) + .collect(), + }; + let transform = graph + .compose_path_parameter_transform(&path) + .unwrap() + .unwrap(); + for source_graph in [ + SimpleGraph::empty(0), + SimpleGraph::empty(1), + SimpleGraph::path(2), + SimpleGraph::cycle(3), + SimpleGraph::path(3), + ] { + let source = HamiltonianCircuit::new(source_graph); + let predicted = transform.evaluate(&source.parameters()).unwrap(); + let chain = graph.reduce_along_path(&path, &source).unwrap().unwrap(); + let target = chain.target_problem::>(); + for (field, actual) in target.parameters().iter() { + assert!(predicted.get(field).expect("composed augmentation bound") >= actual); + } + let expected = BruteForce::new().solve(&source).unwrap().is_some(); + let solution = crate::solvers::ILPSolver::new().solve(target).unwrap(); + let recovered = chain.extract_solution::, _>(&solution); + if expected { + assert!(source.evaluate(&recovered.unwrap()).unwrap().0); + } else { + assert!( + recovered.is_err(), + "infeasible augmentation cannot certify a circuit" + ); + } + } +} + +#[test] +fn biconnectivity_augmentation_predictions_compose_and_recover_through_qubo() { + check_augmentation_predictions_through_qubo::< + crate::models::graph::BiconnectivityAugmentation, + >(); +} + +#[test] +fn strong_connectivity_augmentation_predictions_compose_and_recover_through_qubo() { + check_augmentation_predictions_through_qubo::< + crate::models::graph::StrongConnectivityAugmentation, + >(); +} diff --git a/src/unit_tests/symbolic_parameter_contracts.rs b/src/unit_tests/symbolic_parameter_contracts.rs index 1c506a4e1..e7e0ee35a 100644 --- a/src/unit_tests/symbolic_parameter_contracts.rs +++ b/src/unit_tests/symbolic_parameter_contracts.rs @@ -440,3 +440,59 @@ fn exact_parameter_formulas_cover_sparse_and_boundary_instances() { .iter() .any(|field| field.field == "num_edges")); } + +#[test] +fn augmentation_magnitude_predictions_cover_weights_and_budgets() { + use crate::models::algebraic::ILP; + use crate::models::graph::{BiconnectivityAugmentation, StrongConnectivityAugmentation}; + use crate::topology::DirectedGraph; + + fn check>>(source: S, bits: u64) { + assert_eq!( + source.parameters().get("max_numeric_magnitude_bits"), + Some(bits) + ); + check_reduced_parameters::<_, ILP>( + source, + &["max_constraint_magnitude_bits"], + ParameterRelation::Exact, + ); + } + for (weight, budget, bits) in [ + (0, 0, 1), + (1, 8, 4), + (8, 1, 4), + (7, 1, 3), + (-8, 1, 4), + (1, -8, 4), + (i64::MIN, 0, 64), + (0, i64::MIN, 64), + (i64::MAX, 0, 63), + (1, i64::MAX, 63), + ] { + check( + BiconnectivityAugmentation::new(SimpleGraph::empty(2), vec![(0, 1, weight)], budget), + bits, + ); + if weight > 0 && budget >= 0 { + check( + StrongConnectivityAugmentation::new( + DirectedGraph::empty(2), + vec![(0, 1, weight)], + budget, + ), + bits, + ); + } + } + for (budget, bits) in [(0, 1), (8, 4), (i64::MAX, 63)] { + check( + BiconnectivityAugmentation::<_, i64>::new(SimpleGraph::empty(0), vec![], budget), + bits, + ); + check( + StrongConnectivityAugmentation::::new(DirectedGraph::empty(0), vec![], budget), + bits, + ); + } +}