problemreductions/rules/
consecutiveblockminimization_ilp.rs1use crate::models::algebraic::{
7 ConsecutiveBlockMinimization, LinearConstraint, ObjectiveSense, ILP,
8};
9use crate::reduction;
10use crate::rules::ilp_helpers::{one_hot_assignment_constraints, one_hot_decode};
11use crate::rules::traits::{ReduceTo, ReductionResult};
12
13#[derive(Debug, Clone)]
14pub struct ReductionCBMToILP {
15 target: ILP<bool>,
16 num_cols: usize,
17}
18
19impl ReductionResult for ReductionCBMToILP {
20 type Source = ConsecutiveBlockMinimization;
21 type Target = ILP<bool>;
22
23 fn target_problem(&self) -> &ILP<bool> {
24 &self.target
25 }
26
27 fn extract_solution(
28 &self,
29 target_solution: &<Self::Target as crate::traits::Problem>::Solution,
30 ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
31 crate::rules::traits::validate_target_witness(
32 self.target_problem(),
33 target_solution,
34 |value| value.value.is_some(),
35 "target ILP assignment is infeasible",
36 )?;
37
38 one_hot_decode(target_solution, self.num_cols, self.num_cols, 0)
39 }
40}
41
42#[crate::aggregate_reduction(ilp_feasibility)]
43impl crate::rules::AggregateReductionResult for ReductionCBMToILP {}
44
45#[reduction(
46 transform = upper_bound {
47 max_constraint_magnitude_bits = "num_rows * num_cols + 1",
48 num_vars = "num_cols * num_cols + num_rows * num_cols + num_rows * num_cols",
49 num_constraints = "num_cols + num_cols + num_rows * num_cols + num_rows + num_rows * num_cols + 1",
50 num_nonzeros = "(num_cols * num_cols + num_rows * num_cols + num_rows * num_cols) * (num_cols + num_cols + num_rows * num_cols + num_rows + num_rows * num_cols + 1)",
51 },
52)]
53impl ReduceTo<ILP<bool>> for ConsecutiveBlockMinimization {
54 type Result = ReductionCBMToILP;
55
56 fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
57 let m = self.num_rows();
58 let n = self.num_cols();
59
60 let x_offset = 0;
68 let a_offset = n * n;
69 let b_offset = n * n + m * n;
70 let num_vars = n * n + 2 * m * n;
71
72 let mut constraints = Vec::new();
73
74 constraints.extend(one_hot_assignment_constraints(n, n, x_offset));
76
77 for r in 0..m {
79 for p in 0..n {
80 let a_idx = a_offset + r * n + p;
81 let mut terms = vec![(a_idx, 1)];
83 for c in 0..n {
84 if self.matrix()[r][c] {
85 terms.push((x_offset + c * n + p, -1));
86 }
87 }
88 constraints.push(LinearConstraint::eq(terms, 0));
89 }
90 }
91
92 for r in 0..m {
94 if n == 0 {
95 break;
96 }
97 let b_idx = b_offset + r * n;
99 let a_idx = a_offset + r * n;
100 constraints.push(LinearConstraint::eq(vec![(b_idx, 1), (a_idx, -1)], 0));
101
102 for p in 1..n {
104 let b_idx = b_offset + r * n + p;
105 let a_cur = a_offset + r * n + p;
106 let a_prev = a_offset + r * n + (p - 1);
107 constraints.push(LinearConstraint::ge(
108 vec![(b_idx, 1), (a_cur, -1), (a_prev, 1)],
109 0,
110 ));
111 }
112 }
113
114 let mut bound_terms = Vec::new();
116 for r in 0..m {
117 for p in 0..n {
118 bound_terms.push((b_offset + r * n + p, 1));
119 }
120 }
121 let max_blocks = Self::exact_i64(bound_terms.len(), "encoding the block-count bound")?;
124 constraints.push(LinearConstraint::le(
125 bound_terms,
126 self.bound().clamp(-1, max_blocks),
127 ));
128
129 let target = ILP::new(num_vars, constraints, vec![], ObjectiveSense::Minimize)
130 .map_err(Self::target_construction)?;
131 Ok(ReductionCBMToILP {
132 target,
133 num_cols: n,
134 })
135 }
136}
137
138#[cfg(feature = "example-db")]
139pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
140 vec![crate::example_db::specs::RuleExampleSpec {
141 id: "consecutiveblockminimization_to_ilp",
142 build: || {
143 let source = ConsecutiveBlockMinimization::new(
145 vec![vec![true, false, true], vec![false, true, true]],
146 2,
147 );
148 crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
149 },
150 }]
151}
152
153#[cfg(test)]
154#[path = "../unit_tests/rules/consecutiveblockminimization_ilp.rs"]
155mod tests;