problemreductions/rules/

stringtostringcorrection_ilp.rs

//! Reduction from StringToStringCorrection to ILP (Integer Linear Programming).
//!
//! A time-expanded ILP with state variables z_{t,p,i} tracking token positions,
//! emptiness bits e_{t,p}, and operation selectors (delete, swap, no-op) at
//! each of K stages.

use crate::models::algebraic::{LinearConstraint, ObjectiveSense, ILP};
use crate::models::misc::StringToStringCorrection;
use crate::reduction;
use crate::rules::traits::{ReduceTo, ReductionResult};

/// Result of reducing StringToStringCorrection to ILP.
#[derive(Debug, Clone)]
pub struct ReductionSTSCToILP {
    target: ILP<bool>,
    n: usize,
    bound: usize,
}

// Index helper functions (free functions to avoid `Self::` ambiguity in trait impls).
fn idx_z(n: usize, t: usize, p: usize, i: usize) -> usize {
    t * n * n + p * n + i
}

fn idx_e(n: usize, k: usize, t: usize, p: usize) -> usize {
    (k + 1) * n * n + t * n + p
}

fn idx_d(n: usize, k: usize, t: usize, j: usize) -> usize {
    (k + 1) * (n * n + n) + (t - 1) * n + j
}

fn idx_s(n: usize, k: usize, t: usize, j: usize) -> usize {
    let nm1 = n.saturating_sub(1);
    (k + 1) * (n * n + n) + k * n + (t - 1) * nm1 + j
}

fn idx_nu(n: usize, k: usize, t: usize) -> usize {
    let nm1 = n.saturating_sub(1);
    (k + 1) * (n * n + n) + k * n + k * nm1 + (t - 1)
}

fn total_vars(n: usize, k: usize) -> usize {
    let nm1 = n.saturating_sub(1);
    (k + 1) * n * n + (k + 1) * n + k * n + k * nm1 + k
}

impl ReductionResult for ReductionSTSCToILP {
    type Source = StringToStringCorrection;
    type Target = ILP<bool>;

    fn target_problem(&self) -> &ILP<bool> {
        &self.target
    }

    /// Extract operation sequence from ILP solution.
    fn extract_solution(
        &self,
        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
        crate::rules::traits::validate_target_solution(self.target_problem(), target_solution)?;

        Ok({
            let n = self.n;
            let k = self.bound;
            let noop_code = 2 * n;

            if n == 0 {
                return Ok(vec![noop_code; k]);
            }

            let nm1 = n.saturating_sub(1);
            let mut ops = Vec::with_capacity(k);

            for t in 1..=k {
                // current length at step t-1
                let current_len = (0..n)
                    .filter(|&p| target_solution[idx_e(n, k, t - 1, p)] == 0)
                    .count();

                let mut selected = Vec::new();
                if target_solution[idx_nu(n, k, t)] == 1 {
                    selected.push(noop_code);
                }
                selected.extend((0..n).filter(|&j| target_solution[idx_d(n, k, t, j)] == 1));
                selected.extend(
                    (0..nm1)
                        .filter(|&j| target_solution[idx_s(n, k, t, j)] == 1)
                        .map(|j| current_len + j),
                );
                match selected.as_slice() {
                    [operation] => ops.push(*operation),
                    [] => {
                        return Err(crate::rules::ExtractionError::invalid(format!(
                            "edit step {t} has no selected operation"
                        )))
                    }
                    _ => {
                        return Err(crate::rules::ExtractionError::invalid(format!(
                            "edit step {t} has multiple selected operations"
                        )))
                    }
                }
            }
            ops
        })
    }
}

#[reduction(
    transform = upper_bound {
        num_vars = "(bound + 1) * source_length^2 + (bound + 1) * source_length + 2 * bound * source_length + bound",
        num_constraints = "4 * bound * source_length^3 + 2 * bound * source_length^2 + source_length^2 + 6 * bound * source_length + 5 * source_length + bound",
    },
    unavailable = {
        num_nonzeros = "the exact target parameter is not represented by this reduction's symbolic transform",
    }
)]
impl ReduceTo<ILP<bool>> for StringToStringCorrection {
    type Result = ReductionSTSCToILP;

    #[allow(clippy::needless_range_loop)]
    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
        let n = self.source_length();
        let m = self.target_length();
        let k = self.bound();
        let source = self.source();
        let target = self.target();

        // If infeasible by length check, return trivially infeasible ILP
        if m > n || m < n.saturating_sub(k) {
            return Ok(ReductionSTSCToILP {
                target: ILP::new(
                    0,
                    vec![LinearConstraint::le(vec![], -1)],
                    vec![],
                    ObjectiveSense::Minimize,
                )
                .map_err(Self::target_construction)?,
                n,
                bound: k,
            });
        }

        // n == 0 edge case: source and target both empty, all no-ops
        if n == 0 {
            let nv = k;
            let mut constraints = Vec::new();
            for t in 1..=k {
                constraints.push(LinearConstraint::eq(vec![(t - 1, 1)], 1));
            }
            return Ok(ReductionSTSCToILP {
                target: ILP::new(nv, constraints, vec![], ObjectiveSense::Minimize)
                    .map_err(Self::target_construction)?,
                n,
                bound: k,
            });
        }

        let nm1 = n.saturating_sub(1);
        let nv = total_vars(n, k);

        let mut constraints = Vec::new();

        // === State validity ===

        // e_{t,p} + Σ_i z_{t,p,i} = 1  ∀ t,p
        for t in 0..=k {
            for p in 0..n {
                let mut terms = vec![(idx_e(n, k, t, p), 1)];
                for i in 0..n {
                    terms.push((idx_z(n, t, p, i), 1));
                }
                constraints.push(LinearConstraint::eq(terms, 1));
            }
        }

        // Σ_p z_{t,p,i} <= 1  ∀ t,i
        for t in 0..=k {
            for i in 0..n {
                let terms: Vec<(usize, i64)> = (0..n).map(|p| (idx_z(n, t, p, i), 1)).collect();
                constraints.push(LinearConstraint::le(terms, 1));
            }
        }

        // e_{t,p} <= e_{t,p+1}  ∀ t, p < n-1
        for t in 0..=k {
            for p in 0..nm1 {
                constraints.push(LinearConstraint::le(
                    vec![(idx_e(n, k, t, p), 1), (idx_e(n, k, t, p + 1), -1)],
                    0,
                ));
            }
        }

        // === Initial state ===
        for p in 0..n {
            constraints.push(LinearConstraint::eq(vec![(idx_z(n, 0, p, p), 1)], 1));
            for i in 0..n {
                if i != p {
                    constraints.push(LinearConstraint::eq(vec![(idx_z(n, 0, p, i), 1)], 0));
                }
            }
            constraints.push(LinearConstraint::eq(vec![(idx_e(n, k, 0, p), 1)], 0));
        }

        // === Operation choice ===
        for t in 1..=k {
            let mut terms = Vec::new();
            for j in 0..n {
                terms.push((idx_d(n, k, t, j), 1));
            }
            for j in 0..nm1 {
                terms.push((idx_s(n, k, t, j), 1));
            }
            terms.push((idx_nu(n, k, t), 1));
            constraints.push(LinearConstraint::eq(terms, 1));
        }

        // Legality
        for t in 1..=k {
            for j in 0..n {
                constraints.push(LinearConstraint::le(
                    vec![(idx_d(n, k, t, j), 1), (idx_e(n, k, t - 1, j), 1)],
                    1,
                ));
            }
            for j in 0..nm1 {
                constraints.push(LinearConstraint::le(
                    vec![(idx_s(n, k, t, j), 1), (idx_e(n, k, t - 1, j), 1)],
                    1,
                ));
                constraints.push(LinearConstraint::le(
                    vec![(idx_s(n, k, t, j), 1), (idx_e(n, k, t - 1, j + 1), 1)],
                    1,
                ));
            }
        }

        // === State-update (M=1 big-M) ===
        for t in 1..=k {
            for p in 0..n {
                for i in 0..n {
                    // No-op
                    constraints.push(LinearConstraint::le(
                        vec![
                            (idx_z(n, t, p, i), 1),
                            (idx_z(n, t - 1, p, i), -1),
                            (idx_nu(n, k, t), 1),
                        ],
                        1,
                    ));
                    constraints.push(LinearConstraint::le(
                        vec![
                            (idx_z(n, t - 1, p, i), 1),
                            (idx_z(n, t, p, i), -1),
                            (idx_nu(n, k, t), 1),
                        ],
                        1,
                    ));

                    // Delete at position j
                    for j in 0..n {
                        if p < j {
                            // Before deleted position: unchanged
                            constraints.push(LinearConstraint::le(
                                vec![
                                    (idx_z(n, t, p, i), 1),
                                    (idx_z(n, t - 1, p, i), -1),
                                    (idx_d(n, k, t, j), 1),
                                ],
                                1,
                            ));
                            constraints.push(LinearConstraint::le(
                                vec![
                                    (idx_z(n, t - 1, p, i), 1),
                                    (idx_z(n, t, p, i), -1),
                                    (idx_d(n, k, t, j), 1),
                                ],
                                1,
                            ));
                        } else if p + 1 < n {
                            // j <= p < n-1: shift from p+1
                            constraints.push(LinearConstraint::le(
                                vec![
                                    (idx_z(n, t, p, i), 1),
                                    (idx_z(n, t - 1, p + 1, i), -1),
                                    (idx_d(n, k, t, j), 1),
                                ],
                                1,
                            ));
                            constraints.push(LinearConstraint::le(
                                vec![
                                    (idx_z(n, t - 1, p + 1, i), 1),
                                    (idx_z(n, t, p, i), -1),
                                    (idx_d(n, k, t, j), 1),
                                ],
                                1,
                            ));
                        } else {
                            // p == n-1: last slot must be empty
                            constraints.push(LinearConstraint::le(
                                vec![(idx_z(n, t, n - 1, i), 1), (idx_d(n, k, t, j), 1)],
                                1,
                            ));
                        }
                    }

                    // Swap at position j
                    for j in 0..nm1 {
                        if p != j && p != j + 1 {
                            constraints.push(LinearConstraint::le(
                                vec![
                                    (idx_z(n, t, p, i), 1),
                                    (idx_z(n, t - 1, p, i), -1),
                                    (idx_s(n, k, t, j), 1),
                                ],
                                1,
                            ));
                            constraints.push(LinearConstraint::le(
                                vec![
                                    (idx_z(n, t - 1, p, i), 1),
                                    (idx_z(n, t, p, i), -1),
                                    (idx_s(n, k, t, j), 1),
                                ],
                                1,
                            ));
                        } else if p == j {
                            constraints.push(LinearConstraint::le(
                                vec![
                                    (idx_z(n, t, j, i), 1),
                                    (idx_z(n, t - 1, j + 1, i), -1),
                                    (idx_s(n, k, t, j), 1),
                                ],
                                1,
                            ));
                            constraints.push(LinearConstraint::le(
                                vec![
                                    (idx_z(n, t - 1, j + 1, i), 1),
                                    (idx_z(n, t, j, i), -1),
                                    (idx_s(n, k, t, j), 1),
                                ],
                                1,
                            ));
                        } else {
                            // p == j+1
                            constraints.push(LinearConstraint::le(
                                vec![
                                    (idx_z(n, t, j + 1, i), 1),
                                    (idx_z(n, t - 1, j, i), -1),
                                    (idx_s(n, k, t, j), 1),
                                ],
                                1,
                            ));
                            constraints.push(LinearConstraint::le(
                                vec![
                                    (idx_z(n, t - 1, j, i), 1),
                                    (idx_z(n, t, j + 1, i), -1),
                                    (idx_s(n, k, t, j), 1),
                                ],
                                1,
                            ));
                        }
                    }
                }
            }
        }

        // === Final state equals target ===
        for p in 0..m {
            let terms: Vec<(usize, i64)> = (0..n)
                .filter(|&i| source[i] == target[p])
                .map(|i| (idx_z(n, k, p, i), 1))
                .collect();
            constraints.push(LinearConstraint::eq(terms, 1));
        }
        for p in m..n {
            constraints.push(LinearConstraint::eq(vec![(idx_e(n, k, k, p), 1)], 1));
        }

        let target_ilp = ILP::new(nv, constraints, vec![], ObjectiveSense::Minimize)
            .map_err(Self::target_construction)?;
        Ok(ReductionSTSCToILP {
            target: target_ilp,
            n,
            bound: k,
        })
    }
}

#[cfg(feature = "example-db")]
pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
    use crate::export::SolutionPair;
    vec![crate::example_db::specs::RuleExampleSpec {
        id: "stringtostringcorrection_to_ilp",
        build: || {
            // source=[0,1,0], target=[1,0], bound=1 (delete position 0)
            let source = StringToStringCorrection::new(2, vec![0, 1, 0], vec![1, 0], 1);
            let reduction: ReductionSTSCToILP =
                ReduceTo::<ILP<bool>>::reduce_to(&source).expect("reduction should succeed");
            let target_config = {
                let ilp_solver = crate::solvers::ILPSolver::new();
                ilp_solver
                    .solve(reduction.target_problem())
                    .expect("ILP should be solvable")
            };
            let source_config = reduction.extract_solution(&target_config).unwrap();
            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
                source,
                SolutionPair {
                    source_config: serde_json::to_value(source_config)
                        .expect("solution serialization must succeed"),
                    target_config: serde_json::to_value(target_config)
                        .expect("solution serialization must succeed"),
                },
            )
        },
    }]
}

#[cfg(test)]
#[path = "../unit_tests/rules/stringtostringcorrection_ilp.rs"]
mod tests;