problemreductions/rules/
shortestcommonsupersequence_ilp.rs

1//! Reduction from ShortestCommonSupersequence to ILP (Integer Linear Programming).
2//!
3//! One-hot symbol variables x_{p,a} for each position p and symbol a, plus
4//! matching variables m_{s,j,p} indicating that the j-th character of string s
5//! is matched to position p. Monotonicity forces strictly increasing match
6//! positions per string.
7
8use crate::models::algebraic::{LinearConstraint, ObjectiveSense, ILP};
9use crate::models::misc::ShortestCommonSupersequence;
10use crate::reduction;
11use crate::rules::traits::{ReduceTo, ReductionResult};
12
13#[derive(Debug, Clone)]
14pub struct ReductionSCSToILP {
15    target: ILP<bool>,
16    max_length: usize,
17    alphabet_size: usize,
18}
19
20impl ReductionResult for ReductionSCSToILP {
21    type Source = ShortestCommonSupersequence;
22    type Target = ILP<bool>;
23
24    fn target_problem(&self) -> &ILP<bool> {
25        &self.target
26    }
27
28    /// At each position p, output the unique symbol a with x_{p,a} = 1.
29    /// Uses alphabet_size + 1 symbols (last = padding).
30    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
31        let b = self.max_length;
32        let k = self.alphabet_size + 1; // includes padding symbol
33        (0..b)
34            .map(|p| {
35                (0..k)
36                    .find(|&a| target_solution[p * k + a] == 1)
37                    .unwrap_or(0)
38            })
39            .collect()
40    }
41}
42
43#[reduction(
44    overhead = {
45        num_vars = "max_length * (alphabet_size + 1) + total_length * max_length",
46        num_constraints = "max_length + total_length + total_length * max_length + total_length + max_length",
47    }
48)]
49impl ReduceTo<ILP<bool>> for ShortestCommonSupersequence {
50    type Result = ReductionSCSToILP;
51
52    fn reduce_to(&self) -> Self::Result {
53        let b = self.max_length();
54        let alpha = self.alphabet_size();
55        let k = alpha + 1; // alphabet + padding symbol
56        let strings = self.strings();
57        let pad = alpha; // padding symbol index
58
59        // Variable layout:
60        //   x_{p,a}: position p carries symbol a, index p*k + a  for p in 0..b, a in 0..k
61        //   m_{s,j,p}: j-th char of string s matched to position p
62        //     We flatten (s,j) into a global character index.
63        let x_count = b * k;
64
65        // Build global char index: for string s, char j, the global index is sum of lengths before s + j
66        let mut char_offsets = Vec::with_capacity(strings.len());
67        let mut total_chars = 0usize;
68        for s_str in strings {
69            char_offsets.push(total_chars);
70            total_chars += s_str.len();
71        }
72
73        // m_{global_char, p}: index x_count + global_char * b + p
74        let m_offset = x_count;
75        let num_vars = x_count + total_chars * b;
76
77        let mut constraints = Vec::new();
78
79        // 1. One-hot symbol at each position: Σ_a x_{p,a} = 1  ∀ p
80        for p in 0..b {
81            let terms: Vec<(usize, f64)> = (0..k).map(|a| (p * k + a, 1.0)).collect();
82            constraints.push(LinearConstraint::eq(terms, 1.0));
83        }
84
85        // 2. Each character matched to exactly one position: Σ_p m_{gc,p} = 1
86        for gc in 0..total_chars {
87            let terms: Vec<(usize, f64)> = (0..b).map(|p| (m_offset + gc * b + p, 1.0)).collect();
88            constraints.push(LinearConstraint::eq(terms, 1.0));
89        }
90
91        // 3. Symbol consistency: m_{gc,p} <= x_{p,a} where a is the symbol at gc
92        for (s_idx, s_str) in strings.iter().enumerate() {
93            for (j, &sym) in s_str.iter().enumerate() {
94                let gc = char_offsets[s_idx] + j;
95                for p in 0..b {
96                    // m_{gc,p} <= x_{p,sym}
97                    constraints.push(LinearConstraint::le(
98                        vec![(m_offset + gc * b + p, 1.0), (p * k + sym, -1.0)],
99                        0.0,
100                    ));
101                }
102            }
103        }
104
105        // 4. Monotonicity: matching positions strictly increase within each string.
106        //    For consecutive chars j and j+1 of string s:
107        //    Σ_p p * m_{gc_j,p} < Σ_p p * m_{gc_{j+1},p}
108        //    i.e., Σ_p p * m_{gc_{j+1},p} - Σ_p p * m_{gc_j,p} >= 1
109        for (s_idx, s_str) in strings.iter().enumerate() {
110            for j in 0..s_str.len().saturating_sub(1) {
111                let gc_j = char_offsets[s_idx] + j;
112                let gc_next = char_offsets[s_idx] + j + 1;
113                let mut terms = Vec::new();
114                for p in 0..b {
115                    terms.push((m_offset + gc_next * b + p, p as f64));
116                    terms.push((m_offset + gc_j * b + p, -(p as f64)));
117                }
118                constraints.push(LinearConstraint::ge(terms, 1.0));
119            }
120        }
121
122        // 5. Contiguous padding: if position p is padding, then p+1 must also be padding.
123        //    x_{p,pad} <= x_{p+1,pad}  for p in 0..b-1
124        for p in 0..b.saturating_sub(1) {
125            constraints.push(LinearConstraint::le(
126                vec![(p * k + pad, 1.0), ((p + 1) * k + pad, -1.0)],
127                0.0,
128            ));
129        }
130
131        // Objective: minimize non-padding positions = maximize padding positions
132        let objective: Vec<(usize, f64)> = (0..b).map(|p| (p * k + pad, 1.0)).collect();
133        let target = ILP::new(num_vars, constraints, objective, ObjectiveSense::Maximize);
134        ReductionSCSToILP {
135            target,
136            max_length: b,
137            alphabet_size: alpha,
138        }
139    }
140}
141
142#[cfg(feature = "example-db")]
143pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
144    use crate::export::SolutionPair;
145    vec![crate::example_db::specs::RuleExampleSpec {
146        id: "shortestcommonsupersequence_to_ilp",
147        build: || {
148            // Alphabet {0,1}, strings [0,1] and [1,0]
149            let source = ShortestCommonSupersequence::new(2, vec![vec![0, 1], vec![1, 0]]);
150            let reduction: ReductionSCSToILP = ReduceTo::<ILP<bool>>::reduce_to(&source);
151            let target_config = {
152                let ilp_solver = crate::solvers::ILPSolver::new();
153                ilp_solver
154                    .solve(reduction.target_problem())
155                    .expect("ILP should be solvable")
156            };
157            let source_config = reduction.extract_solution(&target_config);
158            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
159                source,
160                SolutionPair {
161                    source_config,
162                    target_config,
163                },
164            )
165        },
166    }]
167}
168
169#[cfg(test)]
170#[path = "../unit_tests/rules/shortestcommonsupersequence_ilp.rs"]
171mod tests;
problemreductions/rules/shortestcommonsupersequence_ilp.rs

problemreductions/rules/
shortestcommonsupersequence_ilp.rs
