problemreductions/rules/
bmf_ilp.rs

1//! Exact Boolean factorization with coverage indicators only for true entries.
2
3use crate::models::algebraic::{LinearConstraint, ObjectiveSense, BMF, ILP};
4use crate::reduction;
5use crate::rules::traits::{ReduceTo, ReductionResult};
6
7#[derive(Debug, Clone)]
8pub struct ReductionBMFToILP {
9    target: ILP<bool>,
10    m: usize,
11    n: usize,
12    k: usize,
13}
14
15impl ReductionResult for ReductionBMFToILP {
16    type Source = BMF;
17    type Target = ILP<bool>;
18
19    fn target_problem(&self) -> &ILP<bool> {
20        &self.target
21    }
22
23    fn extract_solution(
24        &self,
25        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
26    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
27        crate::rules::traits::validate_target_witness(
28            self.target_problem(),
29            target_solution,
30            |v| v.value.is_some(),
31            "target ILP assignment does not reconstruct the Boolean matrix",
32        )?;
33
34        let b = (0..self.m)
35            .map(|i| {
36                (0..self.k)
37                    .map(|r| target_solution[i * self.k + r] == 1)
38                    .collect()
39            })
40            .collect();
41        let c_offset = self.m * self.k;
42        let c = (0..self.k)
43            .map(|r| {
44                (0..self.n)
45                    .map(|j| target_solution[c_offset + r * self.n + j] == 1)
46                    .collect()
47            })
48            .collect();
49        Ok((b, c))
50    }
51}
52
53#[reduction(transform = {
54    exact { max_constraint_magnitude_bits = "1", },
55    upper_bound {
56        num_vars = "rows * rank + rank * cols + rows * rank * cols",
57        num_constraints = "(2 * rank + 1) * rows * cols + rank * (rows + cols)",
58        num_nonzeros = "5 * rows * rank * cols + rank * (rows + cols)",
59    },
60})]
61impl ReduceTo<ILP<bool>> for BMF {
62    type Result = ReductionBMFToILP;
63
64    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
65        let m = self.rows();
66        let n = self.cols();
67        let k = self.rank();
68        let overflow = || {
69            crate::rules::ReductionError::integer_overflow::<Self, ILP<bool>>(
70                "counting Boolean factorization variables",
71            )
72        };
73        let c_offset = m.checked_mul(k).ok_or_else(overflow)?;
74        let factor_count = k
75            .checked_mul(n)
76            .and_then(|v| v.checked_add(c_offset))
77            .ok_or_else(overflow)?;
78        <Self as ReduceTo<ILP<bool>>>::exact_i64(factor_count, "bounding Boolean factor size")?;
79        // Pairwise incompatible edges must use distinct factors. Name those
80        // factors first: permuting B columns and C rows preserves every cover
81        // and its objective. Anchor endpoints then exclude non-neighbors.
82        let matrix = self.matrix();
83        let row_degrees: Vec<_> = matrix
84            .iter()
85            .map(|row| row.iter().filter(|&&v| v).count())
86            .collect();
87        let col_degrees: Vec<_> = (0..n)
88            .map(|j| matrix.iter().filter(|row| row[j]).count())
89            .collect();
90        let mut edges: Vec<_> = matrix
91            .iter()
92            .enumerate()
93            .flat_map(|(i, row)| {
94                row.iter()
95                    .enumerate()
96                    .filter_map(move |(j, &v)| v.then_some((i, j)))
97            })
98            .collect();
99        edges.sort_by_key(|&(i, j)| (row_degrees[i], col_degrees[j]));
100        let mut anchors: Vec<(usize, usize)> = Vec::new();
101        for (i, j) in edges {
102            if anchors.len() == k {
103                break;
104            }
105            if anchors.iter().all(|&(u, v)| !matrix[i][v] || !matrix[u][j]) {
106                anchors.push((i, j));
107            }
108        }
109        let mut fixed = vec![None; factor_count];
110        for (r, &(u, v)) in anchors.iter().enumerate() {
111            for i in 0..m {
112                if !matrix[i][v] {
113                    fixed[i * k + r] = Some(0);
114                }
115            }
116            for j in 0..n {
117                if !matrix[u][j] {
118                    fixed[c_offset + r * n + j] = Some(0);
119                }
120            }
121            fixed[u * k + r] = Some(1);
122            fixed[c_offset + r * n + v] = Some(1);
123        }
124        let mut next = factor_count;
125        let mut constraints: Vec<_> = fixed
126            .iter()
127            .enumerate()
128            .filter_map(|(index, &value)| {
129                value.map(|value| LinearConstraint::eq(vec![(index, 1)], value))
130            })
131            .collect();
132        for (i, row) in self.matrix().iter().enumerate() {
133            for (j, &value) in row.iter().enumerate() {
134                if value {
135                    if (0..k).any(|r| {
136                        fixed[i * k + r] == Some(1) && fixed[c_offset + r * n + j] == Some(1)
137                    }) {
138                        continue;
139                    }
140                    let mut coverage = Vec::new();
141                    for r in 0..k {
142                        if fixed[i * k + r] == Some(0) || fixed[c_offset + r * n + j] == Some(0) {
143                            continue;
144                        }
145                        let bit = next;
146                        next = next.checked_add(1).ok_or_else(overflow)?;
147                        constraints.push(LinearConstraint::le(vec![(bit, 1), (i * k + r, -1)], 0));
148                        constraints.push(LinearConstraint::le(
149                            vec![(bit, 1), (c_offset + r * n + j, -1)],
150                            0,
151                        ));
152                        coverage.push((bit, 1));
153                    }
154                    constraints.push(LinearConstraint::ge(coverage, 1));
155                } else {
156                    for r in 0..k {
157                        if fixed[i * k + r] == Some(0) || fixed[c_offset + r * n + j] == Some(0) {
158                            continue;
159                        }
160                        constraints.push(LinearConstraint::le(
161                            vec![(i * k + r, 1), (c_offset + r * n + j, 1)],
162                            1,
163                        ));
164                    }
165                }
166            }
167        }
168        let objective = (0..factor_count).map(|i| (i, 1)).collect();
169        let target = ILP::new(next, constraints, objective, ObjectiveSense::Minimize)
170            .map_err(<Self as ReduceTo<ILP<bool>>>::target_construction)?;
171        Ok(ReductionBMFToILP { target, m, n, k })
172    }
173}
174
175#[cfg(feature = "example-db")]
176pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
177    vec![crate::example_db::specs::RuleExampleSpec {
178        id: "bmf_to_ilp",
179        build: || {
180            // 2x2 identity matrix, rank 2
181            let source = BMF::new(vec![vec![true, false], vec![false, true]], 2);
182            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
183        },
184    }]
185}
186
187#[cfg(test)]
188#[path = "../unit_tests/rules/bmf_ilp.rs"]
189mod tests;
problemreductions/rules/bmf_ilp.rs

problemreductions/rules/
bmf_ilp.rs
