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_witness(
30            self.target_problem(),
31            target_solution,
32            |value| value.value.is_some(),
33            "target ILP assignment is infeasible",
34        )?;
35
36        crate::rules::ilp_helpers::one_hot_decode_rows(
37            target_solution,
38            self.num_rows,
39            self.bound_k,
40            0,
41        )
42    }
43}
44
45#[crate::aggregate_reduction(ilp_feasibility)]
46impl crate::rules::AggregateReductionResult for ReductionSMCToILP {}
47
48// Assignments contribute r*k terms. Each unordered row pair and pair
49// of columns emits at most k two-term collision rows; empty columns add none.
50#[reduction(transform = upper_bound {
51    max_constraint_magnitude_bits = "1",
52    num_vars = "num_rows * bound_k",
53    num_constraints = "num_rows + num_rows * (num_rows - 1) * num_cols^2 * bound_k / 2",
54    num_nonzeros = "num_rows * bound_k + num_rows * (num_rows - 1) * num_cols^2 * bound_k",
55})]
56impl ReduceTo<ILP<bool>> for SparseMatrixCompression {
57    type Result = ReductionSMCToILP;
58
59    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
60        let m = self.num_rows();
61        let n = self.num_cols();
62        let k = self.bound_k();
63
64        // Variable layout:
65        // x_{r,g}: m*K binary variables at [0, m*K)
66        //   x_{r*K + g} = 1 iff row r uses shift g (zero-based)
67        let num_vars = m * k;
68        let mut constraints = Vec::new();
69
70        // Each row assigned exactly one shift
71        for r in 0..m {
72            let terms: Vec<(usize, i64)> = (0..k).map(|g| (r * k + g, 1)).collect();
73            constraints.push(LinearConstraint::eq(terms, 1));
74        }
75
76        // Collision constraints:
77        // x_{r,g} + x_{s,h} <= 1 whenever A_{r,i} = A_{s,j} = 1 and i + g = j + h
78        // (for different rows r != s, or same row r = s but different columns i != j)
79        for r in 0..m {
80            for s in (r + 1)..m {
81                for i in 0..n {
82                    if !self.matrix()[r][i] {
83                        continue;
84                    }
85                    for j in 0..n {
86                        if !self.matrix()[s][j] {
87                            continue;
88                        }
89                        // Collision when i + g = j + h, i.e., g - h = j - i
90                        for g in 0..k {
91                            // h = g + i - j (must be in [0, k))
92                            let gi = g + i;
93                            if gi < j {
94                                continue;
95                            }
96                            let h = gi - j;
97                            if h >= k {
98                                continue;
99                            }
100                            constraints.push(LinearConstraint::le(
101                                vec![(r * k + g, 1), (s * k + h, 1)],
102                                1,
103                            ));
104                        }
105                    }
106                }
107            }
108        }
109
110        let target = ILP::new(num_vars, constraints, vec![], ObjectiveSense::Minimize)
111            .map_err(Self::target_construction)?;
112        Ok(ReductionSMCToILP {
113            target,
114            num_rows: m,
115            bound_k: k,
116        })
117    }
118}
119
120#[cfg(feature = "example-db")]
121pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
122    use crate::export::SolutionPair;
123    vec![crate::example_db::specs::RuleExampleSpec {
124        id: "sparsematrixcompression_to_ilp",
125        build: || {
126            let source = SparseMatrixCompression::new(
127                vec![
128                    vec![true, false, false, true],
129                    vec![false, true, false, false],
130                    vec![false, false, true, false],
131                    vec![true, false, false, false],
132                ],
133                2,
134            );
135            let reduction: ReductionSMCToILP =
136                ReduceTo::<ILP<bool>>::reduce_to(&source).expect("reduction should succeed");
137            let ilp_solver = crate::solvers::ILPSolver::new();
138            let target_config = ilp_solver
139                .solve(reduction.target_problem())
140                .expect("ILP should be solvable");
141            let extracted = reduction.extract_solution(&target_config).unwrap();
142            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
143                source,
144                SolutionPair {
145                    source_config: serde_json::json!(extracted),
146                    target_config: serde_json::to_value(target_config)
147                        .expect("solution serialization must succeed"),
148                },
149            )
150        },
151    }]
152}
153
154#[cfg(test)]
155#[path = "../unit_tests/rules/sparsematrixcompression_ilp.rs"]
156mod tests;
problemreductions/rules/sparsematrixcompression_ilp.rs

problemreductions/rules/
sparsematrixcompression_ilp.rs
