Skip to main content

problemreductions/rules/
consecutiveblockminimization_ilp.rs

1//! Reduction from ConsecutiveBlockMinimization to ILP.
2//!
3//! Permute columns with a one-hot assignment and count row-wise block starts
4//! by detecting each 0-to-1 transition after permutation.
5
6use 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        // Variable layout:
61        // x_{c,p}: n*n variables at indices [0, n*n)
62        //   x_{c*n + p} = 1 iff column c goes to position p
63        // a_{r,p}: m*n variables at indices [n*n, n*n + m*n)
64        //   value seen by row r at position p
65        // b_{r,p}: m*n variables at indices [n*n + m*n, n*n + 2*m*n)
66        //   block-start indicator
67        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        // One-hot assignment: each column to exactly one position, each position to exactly one column
75        constraints.extend(one_hot_assignment_constraints(n, n, x_offset));
76
77        // a_{r,p} = sum_c A_{r,c} * x_{c,p} for all r, p
78        for r in 0..m {
79            for p in 0..n {
80                let a_idx = a_offset + r * n + p;
81                // a_{r,p} - sum_c A_{r,c} * x_{c,p} = 0
82                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        // Block-start indicators
93        for r in 0..m {
94            if n == 0 {
95                break;
96            }
97            // b_{r,0} = a_{r,0}
98            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            // b_{r,p} >= a_{r,p} - a_{r,p-1} for p > 0
103            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        // sum_{r,p} b_{r,p} <= K
115        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        // The sum is nonnegative and at most the number of Boolean indicators.
122        // All negative thresholds are equivalent to -1 (infeasible).
123        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            // 2x3 matrix, bound=2
144            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;