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(
31        &self,
32        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
33    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
34        crate::rules::traits::validate_target_solution(self.target_problem(), target_solution)?;
35
36        Ok(crate::rules::ilp_helpers::one_hot_decode_rows(
37            target_solution,
38            self.max_length,
39            self.alphabet_size + 1,
40            0,
41        )?
42        .into_iter()
43        .map(|symbol| (symbol < self.alphabet_size).then_some(symbol))
44        .collect())
45    }
46}
47
48#[reduction(
49    transform = upper_bound {
50        num_vars = "max_length * (alphabet_size + 1) + total_length * max_length",
51        num_constraints = "max_length + total_length + total_length * max_length + total_length + max_length",
52    },
53    unavailable = {
54        num_nonzeros = "the exact target parameter is not represented by this reduction's symbolic transform",
55    }
56)]
57impl ReduceTo<ILP<bool>> for ShortestCommonSupersequence {
58    type Result = ReductionSCSToILP;
59
60    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
61        let b = self.max_length();
62        let alpha = self.alphabet_size();
63        let k = alpha + 1; // alphabet + padding symbol
64        let strings = self.strings();
65        let pad = alpha; // padding symbol index
66
67        // Variable layout:
68        //   x_{p,a}: position p carries symbol a, index p*k + a  for p in 0..b, a in 0..k
69        //   m_{s,j,p}: j-th char of string s matched to position p
70        //     We flatten (s,j) into a global character index.
71        let x_count = b * k;
72
73        // Build global char index: for string s, char j, the global index is sum of lengths before s + j
74        let mut char_offsets = Vec::with_capacity(strings.len());
75        let mut total_chars = 0usize;
76        for s_str in strings {
77            char_offsets.push(total_chars);
78            total_chars += s_str.len();
79        }
80
81        // m_{global_char, p}: index x_count + global_char * b + p
82        let m_offset = x_count;
83        let num_vars = x_count + total_chars * b;
84
85        let mut constraints = Vec::new();
86
87        // 1. One-hot symbol at each position: Σ_a x_{p,a} = 1  ∀ p
88        for p in 0..b {
89            let terms: Vec<(usize, i64)> = (0..k).map(|a| (p * k + a, 1)).collect();
90            constraints.push(LinearConstraint::eq(terms, 1));
91        }
92
93        // 2. Each character matched to exactly one position: Σ_p m_{gc,p} = 1
94        for gc in 0..total_chars {
95            let terms: Vec<(usize, i64)> = (0..b).map(|p| (m_offset + gc * b + p, 1)).collect();
96            constraints.push(LinearConstraint::eq(terms, 1));
97        }
98
99        // 3. Symbol consistency: m_{gc,p} <= x_{p,a} where a is the symbol at gc
100        for (s_idx, s_str) in strings.iter().enumerate() {
101            for (j, &sym) in s_str.iter().enumerate() {
102                let gc = char_offsets[s_idx] + j;
103                for p in 0..b {
104                    // m_{gc,p} <= x_{p,sym}
105                    constraints.push(LinearConstraint::le(
106                        vec![(m_offset + gc * b + p, 1), (p * k + sym, -1)],
107                        0,
108                    ));
109                }
110            }
111        }
112
113        // 4. Monotonicity: matching positions strictly increase within each string.
114        //    For consecutive chars j and j+1 of string s:
115        //    Σ_p p * m_{gc_j,p} < Σ_p p * m_{gc_{j+1},p}
116        //    i.e., Σ_p p * m_{gc_{j+1},p} - Σ_p p * m_{gc_j,p} >= 1
117        for (s_idx, s_str) in strings.iter().enumerate() {
118            for j in 0..s_str.len().saturating_sub(1) {
119                let gc_j = char_offsets[s_idx] + j;
120                let gc_next = char_offsets[s_idx] + j + 1;
121                let mut terms = Vec::new();
122                for p in 0..b {
123                    let p_i64 = Self::exact_i64(p, "encoding a sequence position")?;
124                    terms.push((m_offset + gc_next * b + p, p_i64));
125                    terms.push((m_offset + gc_j * b + p, -p_i64));
126                }
127                constraints.push(LinearConstraint::ge(terms, 1));
128            }
129        }
130
131        // 5. Contiguous padding: if position p is padding, then p+1 must also be padding.
132        //    x_{p,pad} <= x_{p+1,pad}  for p in 0..b-1
133        for p in 0..b.saturating_sub(1) {
134            constraints.push(LinearConstraint::le(
135                vec![(p * k + pad, 1), ((p + 1) * k + pad, -1)],
136                0,
137            ));
138        }
139
140        // Objective: minimize non-padding positions = maximize padding positions
141        let objective: Vec<(usize, i64)> = (0..b).map(|p| (p * k + pad, 1)).collect();
142        let target = ILP::new(num_vars, constraints, objective, ObjectiveSense::Maximize)
143            .map_err(Self::target_construction)?;
144        Ok(ReductionSCSToILP {
145            target,
146            max_length: b,
147            alphabet_size: alpha,
148        })
149    }
150}
151
152#[cfg(feature = "example-db")]
153pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
154    use crate::export::SolutionPair;
155    vec![crate::example_db::specs::RuleExampleSpec {
156        id: "shortestcommonsupersequence_to_ilp",
157        build: || {
158            // Alphabet {0,1}, strings [0,1] and [1,0]
159            let source = ShortestCommonSupersequence::new(2, vec![vec![0, 1], vec![1, 0]]);
160            let reduction: ReductionSCSToILP =
161                ReduceTo::<ILP<bool>>::reduce_to(&source).expect("reduction should succeed");
162            let target_config = {
163                let ilp_solver = crate::solvers::ILPSolver::new();
164                ilp_solver
165                    .solve(reduction.target_problem())
166                    .expect("ILP should be solvable")
167            };
168            let source_config = reduction.extract_solution(&target_config).unwrap();
169            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
170                source,
171                SolutionPair {
172                    source_config: serde_json::to_value(source_config)
173                        .expect("solution serialization must succeed"),
174                    target_config: serde_json::to_value(target_config)
175                        .expect("solution serialization must succeed"),
176                },
177            )
178        },
179    }]
180}
181
182#[cfg(test)]
183#[path = "../unit_tests/rules/shortestcommonsupersequence_ilp.rs"]
184mod tests;
problemreductions/rules/shortestcommonsupersequence_ilp.rs

problemreductions/rules/
shortestcommonsupersequence_ilp.rs
