problemreductions/rules/
sparsematrixcompression_ilp.rs

1//! Reduction from SparseMatrixCompression to ILP.
2//!
3//! Assign each row one shift value and forbid any pair of shifted 1-entries
4//! from colliding in the storage vector.
5
6use crate::models::algebraic::{LinearConstraint, ObjectiveSense, SparseMatrixCompression, ILP};
7use crate::reduction;
8use crate::rules::traits::{ReduceTo, ReductionResult};
9
10#[derive(Debug, Clone)]
11pub struct ReductionSMCToILP {
12    target: ILP<bool>,
13    num_rows: usize,
14    bound_k: usize,
15}
16
17impl ReductionResult for ReductionSMCToILP {
18    type Source = SparseMatrixCompression;
19    type Target = ILP<bool>;
20
21    fn target_problem(&self) -> &ILP<bool> {
22        &self.target
23    }
24
25    fn extract_solution(
26        &self,
27        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
28    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
29        crate::rules::traits::validate_target_solution(self.target_problem(), target_solution)?;
30
31        crate::rules::ilp_helpers::one_hot_decode_rows(
32            target_solution,
33            self.num_rows,
34            self.bound_k,
35            0,
36        )
37    }
38}
39
40#[reduction(
41    transform = upper_bound {
42        num_vars = "num_rows * bound_k",
43        num_constraints = "num_rows + num_rows * num_rows * bound_k * bound_k",
44    },
45    unavailable = {
46        num_nonzeros = "the exact target parameter is not represented by this reduction's symbolic transform",
47    }
48)]
49impl ReduceTo<ILP<bool>> for SparseMatrixCompression {
50    type Result = ReductionSMCToILP;
51
52    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
53        let m = self.num_rows();
54        let n = self.num_cols();
55        let k = self.bound_k();
56
57        // Variable layout:
58        // x_{r,g}: m*K binary variables at [0, m*K)
59        //   x_{r*K + g} = 1 iff row r uses shift g (zero-based)
60        let num_vars = m * k;
61        let mut constraints = Vec::new();
62
63        // Each row assigned exactly one shift
64        for r in 0..m {
65            let terms: Vec<(usize, i64)> = (0..k).map(|g| (r * k + g, 1)).collect();
66            constraints.push(LinearConstraint::eq(terms, 1));
67        }
68
69        // Collision constraints:
70        // x_{r,g} + x_{s,h} <= 1 whenever A_{r,i} = A_{s,j} = 1 and i + g = j + h
71        // (for different rows r != s, or same row r = s but different columns i != j)
72        for r in 0..m {
73            for s in (r + 1)..m {
74                for i in 0..n {
75                    if !self.matrix()[r][i] {
76                        continue;
77                    }
78                    for j in 0..n {
79                        if !self.matrix()[s][j] {
80                            continue;
81                        }
82                        // Collision when i + g = j + h, i.e., g - h = j - i
83                        for g in 0..k {
84                            // h = g + i - j (must be in [0, k))
85                            let gi = g + i;
86                            if gi < j {
87                                continue;
88                            }
89                            let h = gi - j;
90                            if h >= k {
91                                continue;
92                            }
93                            constraints.push(LinearConstraint::le(
94                                vec![(r * k + g, 1), (s * k + h, 1)],
95                                1,
96                            ));
97                        }
98                    }
99                }
100            }
101        }
102
103        let target = ILP::new(num_vars, constraints, vec![], ObjectiveSense::Minimize)
104            .map_err(Self::target_construction)?;
105        Ok(ReductionSMCToILP {
106            target,
107            num_rows: m,
108            bound_k: k,
109        })
110    }
111}
112
113#[cfg(feature = "example-db")]
114pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
115    use crate::export::SolutionPair;
116    vec![crate::example_db::specs::RuleExampleSpec {
117        id: "sparsematrixcompression_to_ilp",
118        build: || {
119            let source = SparseMatrixCompression::new(
120                vec![
121                    vec![true, false, false, true],
122                    vec![false, true, false, false],
123                    vec![false, false, true, false],
124                    vec![true, false, false, false],
125                ],
126                2,
127            );
128            let reduction: ReductionSMCToILP =
129                ReduceTo::<ILP<bool>>::reduce_to(&source).expect("reduction should succeed");
130            let ilp_solver = crate::solvers::ILPSolver::new();
131            let target_config = ilp_solver
132                .solve(reduction.target_problem())
133                .expect("ILP should be solvable");
134            let extracted = reduction.extract_solution(&target_config).unwrap();
135            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
136                source,
137                SolutionPair {
138                    source_config: serde_json::json!(extracted),
139                    target_config: serde_json::to_value(target_config)
140                        .expect("solution serialization must succeed"),
141                },
142            )
143        },
144    }]
145}
146
147#[cfg(test)]
148#[path = "../unit_tests/rules/sparsematrixcompression_ilp.rs"]
149mod tests;
problemreductions/rules/sparsematrixcompression_ilp.rs

problemreductions/rules/
sparsematrixcompression_ilp.rs
