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

problemreductions/rules/
shortestcommonsupersequence_ilp.rs
