problemreductions/rules/
longestcommonsubsequence_ilp.rs

1//! Reduction from LongestCommonSubsequence to ILP (Integer Linear Programming).
2//!
3//! The source problem is the optimization version of LCS. The ILP builds a
4//! binary model that maximizes the number of active (non-padding) positions:
5//! - `x_(p,a)` selects symbol `a` at witness position `p` (including padding)
6//! - `y_(r,p,j)` selects the matching position `j` in source string `r`
7//!
8//! The constraints enforce exactly one symbol per position (including the
9//! padding symbol), contiguity of padding, conditional matching for active
10//! positions, and character consistency. The objective maximizes the number of
11//! non-padding positions.
12
13use crate::models::algebraic::{LinearConstraint, ObjectiveSense, ILP};
14use crate::models::misc::LongestCommonSubsequence;
15use crate::reduction;
16use crate::rules::traits::{ReduceTo, ReductionResult};
17
18/// Result of reducing LongestCommonSubsequence to ILP.
19#[derive(Debug, Clone)]
20pub struct ReductionLCSToILP {
21    target: ILP<bool>,
22    alphabet_size: usize,
23    max_length: usize,
24}
25
26impl ReductionResult for ReductionLCSToILP {
27    type Source = LongestCommonSubsequence;
28    type Target = ILP<bool>;
29
30    fn target_problem(&self) -> &ILP<bool> {
31        &self.target
32    }
33
34    fn extract_solution(
35        &self,
36        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
37    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
38        crate::rules::traits::validate_target_solution(self.target_problem(), target_solution)?;
39
40        Ok(crate::rules::ilp_helpers::one_hot_decode_rows(
41            target_solution,
42            self.max_length,
43            self.alphabet_size + 1,
44            0,
45        )?
46        .into_iter()
47        .map(|symbol| (symbol < self.alphabet_size).then_some(symbol))
48        .collect())
49    }
50}
51
52#[reduction(
53    transform = exact {
54        num_vars = "max_length * (alphabet_size + 1) + max_length * total_length",
55        num_constraints = "max_length + num_transitions + max_length * num_strings + max_length * total_length + num_transitions * sum_triangular_lengths",
56    },
57    unavailable = {
58        num_nonzeros = "the exact target parameter is not represented by this reduction's symbolic transform",
59    }
60)]
61impl ReduceTo<ILP<bool>> for LongestCommonSubsequence {
62    type Result = ReductionLCSToILP;
63
64    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
65        let alphabet_size = self.alphabet_size();
66        let max_length = self.max_length();
67        let strings = self.strings();
68        let total_length = self.total_length();
69        let padding = alphabet_size; // padding symbol index
70        let num_symbols = alphabet_size + 1; // includes padding
71
72        let symbol_var_count = max_length * num_symbols;
73        let mut string_offsets = Vec::with_capacity(strings.len());
74        let mut running_offset = 0usize;
75        for string in strings {
76            string_offsets.push(running_offset);
77            running_offset += string.len();
78        }
79
80        let match_var = |string_index: usize, position: usize, char_index: usize| -> usize {
81            symbol_var_count + position * total_length + string_offsets[string_index] + char_index
82        };
83
84        let mut constraints = Vec::new();
85
86        // (1) Exactly one symbol (including padding) per witness position.
87        for position in 0..max_length {
88            let terms = (0..num_symbols)
89                .map(|symbol| (position * num_symbols + symbol, 1))
90                .collect();
91            constraints.push(LinearConstraint::eq(terms, 1));
92        }
93
94        // (2) Contiguity: once padding starts, it stays padding.
95        // x_(p+1, padding) >= x_(p, padding)
96        for position in 0..max_length.saturating_sub(1) {
97            constraints.push(LinearConstraint::ge(
98                vec![
99                    (position * num_symbols + padding, -1),
100                    ((position + 1) * num_symbols + padding, 1),
101                ],
102                0,
103            ));
104        }
105
106        // (3) For every string and witness position, the sum of match variables
107        // equals 1 when active and 0 when padding:
108        //   sum_j y_(r,p,j) + x_(p, padding) = 1
109        for (string_index, string) in strings.iter().enumerate() {
110            for position in 0..max_length {
111                let mut terms: Vec<(usize, i64)> = (0..string.len())
112                    .map(|char_index| (match_var(string_index, position, char_index), 1))
113                    .collect();
114                terms.push((position * num_symbols + padding, 1));
115                constraints.push(LinearConstraint::eq(terms, 1));
116            }
117        }
118
119        // (4) A chosen source position can only realize the selected witness symbol.
120        // y_(r, p, j) <= x_(p, string[j])
121        for (string_index, string) in strings.iter().enumerate() {
122            for position in 0..max_length {
123                for (char_index, &symbol) in string.iter().enumerate() {
124                    constraints.push(LinearConstraint::le(
125                        vec![
126                            (match_var(string_index, position, char_index), 1),
127                            (position * num_symbols + symbol, -1),
128                        ],
129                        0,
130                    ));
131                }
132            }
133        }
134
135        // (5) Consecutive active witness positions must map to strictly increasing
136        // source positions.
137        for (string_index, string) in strings.iter().enumerate() {
138            for position in 0..max_length.saturating_sub(1) {
139                for previous in 0..string.len() {
140                    for next in 0..=previous {
141                        constraints.push(LinearConstraint::le(
142                            vec![
143                                (match_var(string_index, position, previous), 1),
144                                (match_var(string_index, position + 1, next), 1),
145                            ],
146                            1,
147                        ));
148                    }
149                }
150            }
151        }
152
153        let num_vars = symbol_var_count + max_length * total_length;
154
155        // Objective: maximize number of non-padding positions.
156        // maximize sum_p sum_{a != padding} x_(p,a)
157        let objective: Vec<(usize, i64)> = (0..max_length)
158            .flat_map(|p| (0..alphabet_size).map(move |a| (p * num_symbols + a, 1)))
159            .collect();
160
161        let target = ILP::<bool>::new(num_vars, constraints, objective, ObjectiveSense::Maximize)
162            .map_err(<Self as ReduceTo<ILP<bool>>>::target_construction)?;
163
164        Ok(ReductionLCSToILP {
165            target,
166            alphabet_size,
167            max_length,
168        })
169    }
170}
171
172#[cfg(feature = "example-db")]
173pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
174    vec![crate::example_db::specs::RuleExampleSpec {
175        id: "longestcommonsubsequence_to_ilp",
176        build: || {
177            // Source: alphabet {0,1,2}, strings [0,1,2] and [1,0,2], max_length = 3
178            // Optimal LCS: [0,2] (length 2) or [1,2] (length 2)
179            // Config with padding: e.g. [0, 2, 3] (symbol 3 = padding)
180            let source = LongestCommonSubsequence::new(3, vec![vec![0, 1, 2], vec![1, 0, 2]]);
181            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
182        },
183    }]
184}
185
186#[cfg(test)]
187#[path = "../unit_tests/rules/longestcommonsubsequence_ilp.rs"]
188mod tests;
problemreductions/rules/longestcommonsubsequence_ilp.rs

problemreductions/rules/
longestcommonsubsequence_ilp.rs
