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        max_constraint_magnitude_bits = "1",
55        num_vars = "max_length * (alphabet_size + 1) + max_length * total_length",
56        num_constraints = "max_length + num_transitions + max_length * num_strings + max_length * total_length + num_transitions * sum_triangular_lengths",
57        num_nonzeros = "max_length * (alphabet_size + 1 + num_strings + 3 * total_length) + 2 * num_transitions * (1 + sum_triangular_lengths)",
58    }
59)]
60impl ReduceTo<ILP<bool>> for LongestCommonSubsequence {
61    type Result = ReductionLCSToILP;
62
63    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
64        let alphabet_size = self.alphabet_size();
65        let max_length = self.max_length();
66        let strings = self.strings();
67        let total_length = self.total_length();
68        let padding = alphabet_size; // padding symbol index
69        let num_symbols = alphabet_size + 1; // includes padding
70
71        let symbol_var_count = max_length * num_symbols;
72        let mut string_offsets = Vec::with_capacity(strings.len());
73        let mut running_offset = 0usize;
74        for string in strings {
75            string_offsets.push(running_offset);
76            running_offset += string.len();
77        }
78
79        let match_var = |string_index: usize, position: usize, char_index: usize| -> usize {
80            symbol_var_count + position * total_length + string_offsets[string_index] + char_index
81        };
82
83        let mut constraints = Vec::new();
84
85        // (1) Exactly one symbol (including padding) per witness position.
86        for position in 0..max_length {
87            let terms = (0..num_symbols)
88                .map(|symbol| (position * num_symbols + symbol, 1))
89                .collect();
90            constraints.push(LinearConstraint::eq(terms, 1));
91        }
92
93        // (2) Contiguity: once padding starts, it stays padding.
94        // x_(p+1, padding) >= x_(p, padding)
95        for position in 0..max_length.saturating_sub(1) {
96            constraints.push(LinearConstraint::ge(
97                vec![
98                    (position * num_symbols + padding, -1),
99                    ((position + 1) * num_symbols + padding, 1),
100                ],
101                0,
102            ));
103        }
104
105        // (3) For every string and witness position, the sum of match variables
106        // equals 1 when active and 0 when padding:
107        //   sum_j y_(r,p,j) + x_(p, padding) = 1
108        for (string_index, string) in strings.iter().enumerate() {
109            for position in 0..max_length {
110                let mut terms: Vec<(usize, i64)> = (0..string.len())
111                    .map(|char_index| (match_var(string_index, position, char_index), 1))
112                    .collect();
113                terms.push((position * num_symbols + padding, 1));
114                constraints.push(LinearConstraint::eq(terms, 1));
115            }
116        }
117
118        // (4) A chosen source position can only realize the selected witness symbol.
119        // y_(r, p, j) <= x_(p, string[j])
120        for (string_index, string) in strings.iter().enumerate() {
121            for position in 0..max_length {
122                for (char_index, &symbol) in string.iter().enumerate() {
123                    constraints.push(LinearConstraint::le(
124                        vec![
125                            (match_var(string_index, position, char_index), 1),
126                            (position * num_symbols + symbol, -1),
127                        ],
128                        0,
129                    ));
130                }
131            }
132        }
133
134        // (5) Consecutive active witness positions must map to strictly increasing
135        // source positions.
136        for (string_index, string) in strings.iter().enumerate() {
137            for position in 0..max_length.saturating_sub(1) {
138                for previous in 0..string.len() {
139                    for next in 0..=previous {
140                        constraints.push(LinearConstraint::le(
141                            vec![
142                                (match_var(string_index, position, previous), 1),
143                                (match_var(string_index, position + 1, next), 1),
144                            ],
145                            1,
146                        ));
147                    }
148                }
149            }
150        }
151
152        let num_vars = symbol_var_count + max_length * total_length;
153
154        // Objective: maximize number of non-padding positions.
155        // maximize sum_p sum_{a != padding} x_(p,a)
156        let objective: Vec<(usize, i64)> = (0..max_length)
157            .flat_map(|p| (0..alphabet_size).map(move |a| (p * num_symbols + a, 1)))
158            .collect();
159
160        let target = ILP::<bool>::new(num_vars, constraints, objective, ObjectiveSense::Maximize)
161            .map_err(<Self as ReduceTo<ILP<bool>>>::target_construction)?;
162
163        Ok(ReductionLCSToILP {
164            target,
165            alphabet_size,
166            max_length,
167        })
168    }
169}
170
171#[cfg(feature = "example-db")]
172pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
173    vec![crate::example_db::specs::RuleExampleSpec {
174        id: "longestcommonsubsequence_to_ilp",
175        build: || {
176            // Source: alphabet {0,1,2}, strings [0,1,2] and [1,0,2], max_length = 3
177            // Optimal LCS: [0,2] (length 2) or [1,2] (length 2)
178            // Config with padding: e.g. [0, 2, 3] (symbol 3 = padding)
179            let source = LongestCommonSubsequence::new(3, vec![vec![0, 1, 2], vec![1, 0, 2]]);
180            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
181        },
182    }]
183}
184
185#[cfg(test)]
186#[path = "../unit_tests/rules/longestcommonsubsequence_ilp.rs"]
187mod tests;
problemreductions/rules/longestcommonsubsequence_ilp.rs

problemreductions/rules/
longestcommonsubsequence_ilp.rs
