From 47a51b36c6b774da1ce5abb844b6bab78c47ed8d Mon Sep 17 00:00:00 2001
From: Xiwei Pan <90967972+isPANN@users.noreply.github.com>
Date: Sat, 10 Oct 2026 08:33:42 -0700
Subject: [PATCH 1/5] Replace LCS to MIS expansion with polynomial choice
 encoding

---
 docs/paper/reductions.typ                     |  25 +-
 problemreductions-cli/tests/cli_tests.rs      | 117 +++++-
 src/models/misc/longest_common_subsequence.rs |  15 +-
 ...commonsubsequence_maximumindependentset.rs | 344 ++++++++++--------
 ...mumvertexcover_longestcommonsubsequence.rs |   4 +-
 ...commonsubsequence_maximumindependentset.rs | 233 ++++++------
 6 files changed, 429 insertions(+), 309 deletions(-)

diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ
index 44256b45b..c65801b08 100644
--- a/docs/paper/reductions.typ
+++ b/docs/paper/reductions.typ
@@ -14036,9 +14036,12 @@ The following reductions to Integer Linear Programming are straightforward formu
 
 #let lcs_mis = load-example("LongestCommonSubsequence", "MaximumIndependentSet")
 #let lcs_mis_sol = lcs_mis.solutions.at(0)
+#let lcs_mis_length = lcs_mis_sol.source_config.filter(x => x != none).len()
+#let lcs_mis_slots = lcs_mis_sol.source_config.len()
+#let lcs_mis_baseline = 2 * lcs_mis_slots * (lcs_mis.source.instance.strings.len() + 1)
 #reduction-rule("LongestCommonSubsequence", "MaximumIndependentSet",
   example: true,
-  example-caption: [LCS of two strings over a 3-symbol alphabet],
+  example-caption: [Polynomial choice encoding of two strings over a 3-symbol alphabet],
   extra: [
     #pred-commands(
       "pred create --example " + rule-spec(lcs_mis) + " -o lcs.json",
@@ -14046,22 +14049,24 @@ The following reductions to Integer Linear Programming are straightforward formu
       "pred solve bundle.json",
       "pred evaluate lcs.json --config " + cli-config(lcs_mis_sol.source_config),
     )
-    Source LCS: config $(#fmt-values(lcs_mis_sol.source_config))$ \
-    Target MIS: $S = {#lcs_mis_sol.target_config.enumerate().filter(((i, x)) => x).map(((i, x)) => str(i)).join(", ")}$ (size #lcs_mis_sol.target_config.filter(x => x).len()) \
-    MIS size $=$ LCS length $= #lcs_mis_sol.target_config.filter(x => x).len()$ #sym.checkmark
+    The strings #fmt-values(lcs_mis.source.instance.strings.at(0)) and #fmt-values(lcs_mis.source.instance.strings.at(1)) have #lcs_mis_slots slots. There are #lcs_mis.source.instance.strings.len() strings and #lcs_mis.target.instance.graph.num_vertices vertices in the target. Source witness $(#fmt-values(lcs_mis_sol.source_config))$ selects #lcs_mis_length active symbol clusters; filling every group gives MIS size $= #lcs_mis_baseline + #lcs_mis_length = #lcs_mis_sol.target_config.filter(x => x).len()$.
   ],
 )[
-  A match-node construction transforms a $k$-string LCS instance into a Maximum Independent Set problem on a conflict graph. Each vertex represents a $k$-tuple of positions (one per string) that all share the same character, and edges connect pairs that cannot coexist in any valid common subsequence. The MIS of this graph equals the LCS length.
+  Symbol and embedding choice groups give a polynomial-size unweighted conflict graph. With $k$ strings, minimum length $L$, total length $T$, and $A$ distinct symbols occurring in the input, the graph has exactly $L(3A+2+2(T+k))$ vertices and at most the square of this count in edges. Its maximum independent set has size $2L(k+1)$ plus the LCS length. Since $A <= T$, unused declared alphabet symbols cannot inflate the graph.
 ][
-  _Construction._ Given $k$ strings $s_1, dots, s_k$ over alphabet $Sigma$ (size $|Sigma|$):
+  _Construction._ Let $s_1, dots, s_k$ be the input strings and $L = min_i |s_i|$, with $L=0$ for no strings. Let $Sigma'$ be the set of symbols occurring in these strings, $A=|Sigma'|$, $T=sum_i |s_i|$, and $G=L(k+1)$.
 
-  _Vertices:_ For each character $c in Sigma$, create a vertex for every $k$-tuple $(p_1, dots, p_k)$ where $s_i [p_i] = c$ for all $i$. The total vertex count equals $sum_(c in Sigma) product_(i=1)^k "count"(c, s_i)$.
+  For every slot $p in {0, dots, L-1}$ create a symbol group $X_p$ with choices $Sigma' union {bot}$, where $bot$ means padding. For every string $r$ and slot $p$, create an embedding group $Y_(r,p)$ with choices $0, dots, |s_r|-1$ and padding. Replace each active symbol choice by three mutually nonadjacent vertices, and every embedding or padding choice by two mutually nonadjacent vertices. All vertices of a choice have identical external neighbours.
 
-  _Edges:_ Two vertices $u = (a_1, dots, a_k)$ and $v = (b_1, dots, b_k)$ are connected if they _conflict_ --- they cannot both appear in a valid common subsequence. A conflict occurs when the position differences are not consistently ordered: $not (forall i: a_i < b_i)$ and $not (forall i: a_i > b_i)$.
+  For every incompatible pair of choices, add all edges between their clusters. Choices conflict when: (1) they are distinct choices in the same group; (2) they belong to symbol groups at $p<q$, with padding at $p$ and an active symbol at $q$; (3) they belong to $X_p$ and $Y_(r,p)$ and disagree, where padding agrees only with padding and symbol $a$ agrees with position $j$ precisely when $s_r[j]=a$; or (4) they belong to embedding groups for the same string at $p<q$, with padding followed by an active position, or active positions $j,j'$ with $j >= j'$. Check all slot pairs, including nonadjacent slots. There are no other edges.
 
-  _Correctness._ ($arrow.r.double$) A common subsequence of length $ell$ selects $ell$ match nodes whose positions are strictly increasing in every string, so no two are adjacent --- forming an independent set of size $ell$. ($arrow.l.double$) An independent set of size $ell$ consists of $ell$ mutually non-conflicting match nodes, meaning their positions are consistently ordered across all strings. Sorting by any string's position yields a valid common subsequence of length $ell$.
+  _Correctness._ ($arrow.r.double$) Any common subsequence of length $ell$ selects its symbols in the first $ell$ slots and increasing embedding positions in every string, followed by padding. Taking every vertex of each selected choice cluster gives an independent set of size $2G+ell$.
 
-  _Solution extraction._ Sort the selected vertices by position in $s_1$. Read off the characters to obtain the common subsequence, then pad to `max_length` with the padding symbol.
+  ($arrow.l.double$) A maximum independent set fills every cluster it touches: any omitted vertex of that cluster can be added. It touches at most one choice per group. Suppose $d_X$ symbol groups and $d_Y$ embedding groups are missing, and $q$ active symbol choices are selected. Discard each active slot lacking an embedding group; this removes at most $d_Y$ letters. The remaining letters match strictly increasing positions in every string, so $q <= "LCS" + d_Y$. Its size is at most
+  $2(G-d_X-d_Y)+q <= 2G+"LCS"-2d_X-d_Y.$
+  Missing any group makes this strictly smaller than the full encoding of an optimal common subsequence. Therefore every optimum fills all groups, its symbols form a valid padded common subsequence, and its size is exactly $2G+"LCS"$. If $L=0$, both optima are zero and the graph is empty.
+
+  _Solution extraction._ Validate independence, reject partial clusters or missing groups, then read the original symbol labels selected in $X_0, dots, X_(L-1)$. Every optimum passes these checks. A complete nonoptimal encoding also decodes to a valid source witness. The metadata parameter `num_distinct_symbols` supplies $A$; construction uses $O(V^2+T log(T+1)+k)$ time and extraction $O(V+E)$ time including validation.
 ]
 
 #let cs_ilp_str = load-example(
diff --git a/problemreductions-cli/tests/cli_tests.rs b/problemreductions-cli/tests/cli_tests.rs
index 8013f5077..8d8cc42e4 100644
--- a/problemreductions-cli/tests/cli_tests.rs
+++ b/problemreductions-cli/tests/cli_tests.rs
@@ -5611,7 +5611,7 @@ fn test_path_preserves_exact_variables_and_bounded_quadratic_terms() {
 }
 
 #[test]
-fn test_path_overall_preserves_unavailable_fields_alongside_exact_fields() {
+fn test_path_vertex_cover_to_lcs_has_complete_parameter_formulas() {
     let output = pred()
         .args([
             "path",
@@ -5628,22 +5628,111 @@ fn test_path_overall_preserves_unavailable_fields_alongside_exact_fields() {
     let fields = envelope["paths"][0]["overall_parameters"]["fields"]
         .as_array()
         .unwrap();
-    let relations = fields
+    let alphabet = fields
         .iter()
-        .map(|field| {
-            (
-                field["field"].as_str().unwrap(),
-                field["relation"].as_str().unwrap(),
-            )
-        })
-        .collect::<std::collections::BTreeMap<_, _>>();
-    assert_eq!(relations["alphabet_size"], "exact");
-    assert_eq!(relations["cross_frequency_product"], "unavailable");
-    let unavailable = fields
+        .find(|field| field["field"] == "alphabet_size")
+        .unwrap();
+    assert_eq!(alphabet["relation"], "exact");
+    assert!(fields
+        .iter()
+        .all(|field| field["relation"] != "unavailable"));
+}
+
+#[test]
+fn test_vertex_cover_via_lcs_to_mis_solves_and_recovers_optimum() {
+    let dir =
+        std::env::temp_dir().join(format!("pred_vertex_cover_lcs_mis_{}", std::process::id()));
+    std::fs::create_dir_all(&dir).unwrap();
+    let source = dir.join("source.json");
+    let route = dir.join("route.json");
+    let bundle = dir.join("bundle.json");
+    let created = pred()
+        .args([
+            "create",
+            "MinimumVertexCover/SimpleGraph/One",
+            "--graph",
+            "0-1,1-2",
+            "-o",
+            source.to_str().unwrap(),
+        ])
+        .output()
+        .unwrap();
+    assert!(
+        created.status.success(),
+        "{}",
+        String::from_utf8_lossy(&created.stderr)
+    );
+    write_named_route(
+        "MinimumVertexCover/SimpleGraph/One",
+        "MaximumIndependentSet/SimpleGraph/One",
+        &[
+            "MinimumVertexCover",
+            "LongestCommonSubsequence",
+            "MaximumIndependentSet",
+        ],
+        &route,
+    );
+    let selected: serde_json::Value =
+        serde_json::from_slice(&std::fs::read(&route).unwrap()).unwrap();
+    assert!(selected["overall_parameters"]["fields"]
+        .as_array()
+        .unwrap()
         .iter()
-        .find(|field| field["relation"] == "unavailable")
+        .all(|field| field["relation"] != "unavailable"));
+    let reduced = pred()
+        .args([
+            "reduce",
+            source.to_str().unwrap(),
+            "--via",
+            route.to_str().unwrap(),
+            "-o",
+            bundle.to_str().unwrap(),
+        ])
+        .output()
+        .unwrap();
+    assert!(
+        reduced.status.success(),
+        "{}",
+        String::from_utf8_lossy(&reduced.stderr)
+    );
+    let data: serde_json::Value = serde_json::from_slice(&std::fs::read(&bundle).unwrap()).unwrap();
+    // L=3, A=3, k=3, T=11: V=3*(9+2+28)=117.
+    assert_eq!(data["target"]["data"]["graph"]["num_vertices"], 117);
+    let solved = pred()
+        .args([
+            "solve",
+            bundle.to_str().unwrap(),
+            "--solver",
+            "ilp",
+            "--json",
+        ])
+        .output()
         .unwrap();
-    assert!(!unavailable["reason"].as_str().unwrap().is_empty());
+    assert!(
+        solved.status.success(),
+        "{}",
+        String::from_utf8_lossy(&solved.stderr)
+    );
+    let result: serde_json::Value = serde_json::from_slice(&solved.stdout).unwrap();
+    assert_eq!(result["evaluation"], "Min(1)");
+    let evaluated = pred()
+        .args([
+            "evaluate",
+            source.to_str().unwrap(),
+            "--config",
+            &result["solution"].to_string(),
+            "--json",
+        ])
+        .output()
+        .unwrap();
+    assert!(
+        evaluated.status.success(),
+        "{}",
+        String::from_utf8_lossy(&evaluated.stderr)
+    );
+    let value: serde_json::Value = serde_json::from_slice(&evaluated.stdout).unwrap();
+    assert_eq!(value["result"], "Min(1)");
+    std::fs::remove_dir_all(dir).unwrap();
 }
 
 #[test]
diff --git a/src/models/misc/longest_common_subsequence.rs b/src/models/misc/longest_common_subsequence.rs
index 1f28fda78..7145d55df 100644
--- a/src/models/misc/longest_common_subsequence.rs
+++ b/src/models/misc/longest_common_subsequence.rs
@@ -167,6 +167,15 @@ impl LongestCommonSubsequence {
             .sum()
     }
 
+    /// Returns the number of distinct symbols occurring in the input strings.
+    pub fn num_distinct_symbols(&self) -> usize {
+        self.strings
+            .iter()
+            .flatten()
+            .collect::<std::collections::BTreeSet<_>>()
+            .len()
+    }
+
     /// Returns the number of adjacent position transitions.
     pub fn num_transitions(&self) -> usize {
         self.max_length.saturating_sub(1)
@@ -178,8 +187,8 @@ impl LongestCommonSubsequence {
     /// Formally: Σ_{c ∈ 0..alphabet_size} Π_{i=1..k} count(c, strings\[i\])
     /// where count(c, s) is the number of occurrences of symbol c in string s.
     ///
-    /// This equals the exact number of match-node vertices in the LCS → MaxIS
-    /// reduction graph.
+    /// This statistic describes the legacy match-tuple expansion, not the
+    /// polynomial-size choice graph used by the LCS → MaxIS reduction.
     pub fn cross_frequency_product(&self) -> usize {
         (0..self.alphabet_size)
             .map(|c| {
@@ -215,9 +224,9 @@ impl Problem for LongestCommonSubsequence {
 
     crate::problem_parameters![
         ("alphabet_size", alphabet_size),
-        ("cross_frequency_product", cross_frequency_product),
         ("max_length", max_length),
         ("num_strings", num_strings),
+        ("num_distinct_symbols", num_distinct_symbols),
         ("num_transitions", num_transitions),
         ("sum_triangular_lengths", sum_triangular_lengths),
         ("total_length", total_length),
diff --git a/src/rules/longestcommonsubsequence_maximumindependentset.rs b/src/rules/longestcommonsubsequence_maximumindependentset.rs
index be5454a14..17e74d7dd 100644
--- a/src/rules/longestcommonsubsequence_maximumindependentset.rs
+++ b/src/rules/longestcommonsubsequence_maximumindependentset.rs
@@ -1,14 +1,9 @@
-//! Reduction from LongestCommonSubsequence to MaximumIndependentSet.
+//! Polynomial-size LCS reduction using symbol and embedding choice groups.
 //!
-//! Constructs a conflict graph where vertices are match-node k-tuples
-//! (positions in each string that share the same character) and edges
-//! connect conflicting tuples that cannot both appear in a valid common
-//! subsequence. A maximum independent set in this graph corresponds to
-//! a longest common subsequence.
-//!
-//! Reference: Santini, Blum, Djukanovic et al. (2021),
-//! "Solving Longest Common Subsequence Problems via a Transformation
-//! to the Maximum Clique Problem," Computers & Operations Research.
+//! Each choice is an independent cluster: two vertices for a position or padding,
+//! three for an active symbol. Conflicts enforce one choice per group, matching
+//! characters, increasing positions, and a padding suffix. Every optimum fills
+//! all groups; its size is 2 * max_length * (num_strings + 1) plus the LCS length.
 
 use crate::models::graph::MaximumIndependentSet;
 use crate::models::misc::LongestCommonSubsequence;
@@ -16,21 +11,23 @@ use crate::reduction;
 use crate::rules::traits::{ReduceTo, ReductionResult};
 use crate::topology::SimpleGraph;
 use crate::types::One;
+use std::ops::Range;
 
-/// Result of reducing LongestCommonSubsequence to MaximumIndependentSet.
-///
-/// Each vertex in the target graph corresponds to a match-node k-tuple
-/// `(p_1, ..., p_k)` where all strings have the same character at their
-/// respective positions.
+#[derive(Debug, Clone)]
+struct Choice {
+    group: usize,
+    slot: usize,
+    string: Option<usize>,
+    value: Option<usize>,
+    vertices: Range<usize>,
+}
+
+/// Stores the choice clusters needed to decode a complete independent set.
 #[derive(Debug, Clone)]
 pub struct ReductionLCSToIS {
-    /// The target MaximumIndependentSet problem.
     target: MaximumIndependentSet<SimpleGraph, One>,
-    /// Match-node k-tuples: `match_nodes[v]` gives the position tuple for vertex v.
-    match_nodes: Vec<Vec<usize>>,
-    /// Character for each match node.
-    match_chars: Vec<usize>,
-    /// Maximum possible subsequence length in the source problem.
+    choices: Vec<Choice>,
+    num_groups: usize,
     max_length: usize,
 }
 
@@ -42,185 +39,212 @@ impl ReductionResult for ReductionLCSToIS {
         &self.target
     }
 
-    /// Extract an LCS solution from a MaximumIndependentSet solution.
-    ///
-    /// Selected vertices correspond to match nodes. Sort by position in
-    /// the first string to get the subsequence order, then pad to `max_length`.
     fn extract_solution(
         &self,
-        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
+        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({
-            // Collect selected match nodes with their characters
-            let mut selected: Vec<(usize, usize)> = target_solution
+        crate::rules::traits::validate_target_witness(
+            self.target_problem(),
+            solution,
+            |value| value.0.is_some(),
+            "selected vertices do not form an independent set",
+        )?;
+        let mut selected_groups = vec![false; self.num_groups];
+        let mut decoded = vec![None; self.max_length];
+        for choice in &self.choices {
+            let selected = solution[choice.vertices.clone()]
                 .iter()
-                .enumerate()
-                .filter(|(_, &v)| v)
-                .map(|(i, _)| (self.match_nodes[i][0], self.match_chars[i]))
-                .collect();
-            // Sort by position in the first string
-            selected.sort_by_key(|&(pos, _)| pos);
-
-            // Build config: characters followed by padding
-            let mut config = Vec::with_capacity(self.max_length);
-            for &(_, ch) in &selected {
-                config.push(Some(ch));
+                .filter(|&&bit| bit)
+                .count();
+            if selected == 0 {
+                continue;
             }
-            // Pad with alphabet_size (the padding symbol)
-            while config.len() < self.max_length {
-                config.push(None);
+            if selected != choice.vertices.len() {
+                return Err(crate::rules::ExtractionError::invalid(
+                    "selected choice cluster is incomplete",
+                ));
             }
-            config
-        })
+            selected_groups[choice.group] = true;
+            if choice.group < self.max_length {
+                decoded[choice.group] = choice.value;
+            }
+        }
+        if let Some(group) = selected_groups.iter().position(|&selected| !selected) {
+            return Err(crate::rules::ExtractionError::invalid(format!(
+                "choice group {group} has no selected choice"
+            )));
+        }
+        Ok(decoded)
     }
 }
 
 #[reduction(
-    transform = upper_bound {
-        num_vertices = "cross_frequency_product",
-        num_edges = "cross_frequency_product^2",
+    transform = {
+        exact {
+            num_vertices = "max_length * (3 * num_distinct_symbols + 2 + 2 * (total_length + num_strings))",
+        },
+        upper_bound {
+            num_edges = "(max_length * (3 * num_distinct_symbols + 2 + 2 * (total_length + num_strings)))^2",
+        },
     }
 )]
 impl ReduceTo<MaximumIndependentSet<SimpleGraph, One>> for LongestCommonSubsequence {
     type Result = ReductionLCSToIS;
 
     fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
-        let strings = self.strings();
-        let k = self.num_strings();
-
-        // Step 1: Build match nodes.
-        // For each character c, find all k-tuples of positions where every
-        // string has character c at its respective position.
-        let mut match_nodes: Vec<Vec<usize>> = Vec::new();
-        let mut match_chars: Vec<usize> = Vec::new();
-
-        for c in 0..self.alphabet_size() {
-            // For each string, collect positions where character c appears
-            let positions_per_string: Vec<Vec<usize>> = strings
+        let overflow = || {
+            crate::rules::ReductionError::integer_overflow::<
+                Self,
+                MaximumIndependentSet<SimpleGraph, One>,
+            >("counting choice vertices")
+        };
+        let total_length = self
+            .strings()
+            .iter()
+            .try_fold(0usize, |total, string| total.checked_add(string.len()))
+            .ok_or_else(overflow)?;
+        let symbols = self
+            .strings()
+            .iter()
+            .flatten()
+            .copied()
+            .collect::<std::collections::BTreeSet<_>>()
+            .into_iter()
+            .collect::<Vec<_>>();
+        let per_slot = symbols
+            .len()
+            .checked_mul(3)
+            .and_then(|value| value.checked_add(2))
+            .and_then(|value| {
+                total_length
+                    .checked_add(self.num_strings())?
+                    .checked_mul(2)?
+                    .checked_add(value)
+            })
+            .ok_or_else(overflow)?;
+        let num_vertices = self
+            .max_length()
+            .checked_mul(per_slot)
+            .ok_or_else(overflow)?;
+        <Self as ReduceTo<MaximumIndependentSet<SimpleGraph, One>>>::exact_i64(
+            num_vertices,
+            "representing the independent-set objective",
+        )?;
+        let mut choices = Vec::new();
+        let mut cursor = 0usize;
+        let mut num_groups = 0;
+        let mut add_group = |slot, string: Option<usize>, values: &[usize]| {
+            for value in values
                 .iter()
-                .map(|s| {
-                    s.iter()
-                        .enumerate()
-                        .filter(|(_, &sym)| sym == c)
-                        .map(|(i, _)| i)
-                        .collect()
-                })
-                .collect();
-
-            // Generate all k-tuples (Cartesian product of position lists)
-            let tuples = cartesian_product(&positions_per_string);
-            for tuple in tuples {
-                match_nodes.push(tuple);
-                match_chars.push(c);
+                .copied()
+                .map(Some)
+                .chain(std::iter::once(None))
+            {
+                let count = if string.is_none() && value.is_some() {
+                    3
+                } else {
+                    2
+                };
+                let end = cursor.checked_add(count).ok_or_else(overflow)?;
+                choices.push(Choice {
+                    group: num_groups,
+                    slot,
+                    string,
+                    value,
+                    vertices: cursor..end,
+                });
+                cursor = end;
             }
+            num_groups += 1;
+            Ok::<_, crate::rules::ReductionError>(())
+        };
+        for slot in 0..self.max_length() {
+            add_group(slot, None, &symbols)?;
         }
-
-        let num_vertices = match_nodes.len();
-
-        // Step 2: Build conflict edges.
-        // Two nodes u = (a_1, ..., a_k) and v = (b_1, ..., b_k) conflict when
-        // they cannot both appear in a valid common subsequence: NOT(all a_i < b_i)
-        // AND NOT(all a_i > b_i).
-        let mut edges: Vec<(usize, usize)> = Vec::new();
-
-        for i in 0..num_vertices {
-            for j in (i + 1)..num_vertices {
-                if nodes_conflict(&match_nodes[i], &match_nodes[j], k) {
-                    edges.push((i, j));
+        for (string, input) in self.strings().iter().enumerate() {
+            let positions = (0..input.len()).collect::<Vec<_>>();
+            for slot in 0..self.max_length() {
+                add_group(slot, Some(string), &positions)?;
+            }
+        }
+        let mut edges = Vec::new();
+        for (i, left) in choices.iter().enumerate() {
+            for right in &choices[i + 1..] {
+                let conflict = if left.group == right.group {
+                    true
+                } else {
+                    // Groups are generated in slot order, with symbols before embeddings.
+                    match (left.string, right.string) {
+                        (None, None) => left.value.is_none() && right.value.is_some(),
+                        (Some(a), Some(b)) if a == b => right
+                            .value
+                            .is_some_and(|j| left.value.is_none_or(|i| i >= j)),
+                        (None, Some(string)) if left.slot == right.slot => {
+                            left.value != right.value.map(|j| self.strings()[string][j])
+                        }
+                        _ => false,
+                    }
+                };
+                if conflict {
+                    for a in left.vertices.clone() {
+                        for b in right.vertices.clone() {
+                            edges.push((a, b));
+                        }
+                    }
                 }
             }
         }
-
         let target = MaximumIndependentSet::new(
             SimpleGraph::new(num_vertices, edges),
             vec![One; num_vertices],
         );
-
         Ok(ReductionLCSToIS {
             target,
-            match_nodes,
-            match_chars,
+            choices,
+            num_groups,
             max_length: self.max_length(),
         })
     }
 }
 
-/// Check whether two match nodes conflict (cannot both be in a common subsequence).
-///
-/// Two nodes `u = (a_1, ..., a_k)` and `v = (b_1, ..., b_k)` conflict when
-/// NOT (all a_i < b_i) AND NOT (all a_i > b_i).
-fn nodes_conflict(u: &[usize], v: &[usize], k: usize) -> bool {
-    let mut all_less = true;
-    let mut all_greater = true;
-    for i in 0..k {
-        if u[i] >= v[i] {
-            all_less = false;
-        }
-        if u[i] <= v[i] {
-            all_greater = false;
-        }
-    }
-    !all_less && !all_greater
-}
-
-/// Compute the Cartesian product of a list of position vectors.
-fn cartesian_product(lists: &[Vec<usize>]) -> Vec<Vec<usize>> {
-    if lists.is_empty() {
-        return vec![vec![]];
-    }
-
-    let mut result = vec![vec![]];
-    for list in lists {
-        let mut new_result = Vec::new();
-        for prefix in &result {
-            for &item in list {
-                let mut new_tuple = prefix.clone();
-                new_tuple.push(item);
-                new_result.push(new_tuple);
-            }
-        }
-        result = new_result;
-    }
-    result
-}
-
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
     use crate::export::SolutionPair;
 
-    /// Build the example from the issue: k=2, s1="ABAC", s2="BACA", alphabet={A,B,C}.
-    fn lcs_abac_baca() -> LongestCommonSubsequence {
-        // A=0, B=1, C=2
-        LongestCommonSubsequence::new(
-            3,
-            vec![
-                vec![0, 1, 0, 2], // ABAC
-                vec![1, 0, 2, 0], // BACA
-            ],
-        )
-    }
-
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "longestcommonsubsequence_to_maximumindependentset",
         build: || {
-            // Issue example: MIS solution {v2, v4, v5} gives LCS "BAC" (length 3).
-            // Match nodes (ordered by character):
-            //   c=A(0): v0=(0,1), v1=(0,3), v2=(2,1), v3=(2,3)
-            //   c=B(1): v4=(1,0)
-            //   c=C(2): v5=(3,2)
-            // MIS {v2, v4, v5} => positions B@(1,0), A@(2,1), C@(3,2)
-            // source_config = [1, 0, 2, null] (B, A, C, padding)
-            crate::example_db::specs::rule_example_with_witness::<
-                _,
-                MaximumIndependentSet<SimpleGraph, One>,
-            >(
-                lcs_abac_baca(),
-                SolutionPair {
-                    source_config: serde_json::json!(vec![Some(1), Some(0), Some(2), None]),
-                    target_config: serde_json::json!(vec![false, false, true, false, true, true]),
-                },
+            let source = LongestCommonSubsequence::new(3, vec![vec![0, 1, 0, 2], vec![1, 0, 2, 0]]);
+            let reduction = ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&source)
+                .expect("reduction should succeed");
+            // BAC, then padding; its positions are (1,2,3) and (0,1,2).
+            let assignments = [
+                Some(1),
+                Some(0),
+                Some(2),
+                None,
+                Some(1),
+                Some(2),
+                Some(3),
+                None,
+                Some(0),
+                Some(1),
+                Some(2),
+                None,
+            ];
+            let mut target_config = vec![false; reduction.target.num_vertices()];
+            for choice in &reduction.choices {
+                if assignments[choice.group] == choice.value {
+                    target_config[choice.vertices.clone()].fill(true);
+                }
+            }
+            crate::example_db::specs::assemble_rule_example(
+                &source,
+                reduction.target_problem(),
+                vec![SolutionPair {
+                    source_config: serde_json::json!(&assignments[..source.max_length()]),
+                    target_config: serde_json::json!(target_config),
+                }],
             )
         },
     }]
diff --git a/src/rules/minimumvertexcover_longestcommonsubsequence.rs b/src/rules/minimumvertexcover_longestcommonsubsequence.rs
index cfe1799c0..92762e3f9 100644
--- a/src/rules/minimumvertexcover_longestcommonsubsequence.rs
+++ b/src/rules/minimumvertexcover_longestcommonsubsequence.rs
@@ -42,6 +42,7 @@ impl ReductionResult for ReductionVCToLCS {
     transform = {
         exact {
             alphabet_size = "num_vertices",
+            num_distinct_symbols = "num_vertices",
             num_strings = "num_edges + 1",
             max_length = "num_vertices",
             total_length = "num_vertices + 2 * num_edges * num_vertices - 2 * num_edges",
@@ -51,9 +52,6 @@ impl ReductionResult for ReductionVCToLCS {
             num_transitions = "num_vertices",
         },
     },
-    unavailable = {
-        cross_frequency_product = "each symbol occurs once in the base string and at most twice in each of num_edges edge strings; the source-only bound num_vertices * 2^num_edges needs a variable exponent, unsupported by the exact evaluator; endpoint incidences determine the exact product",
-    }
 )]
 impl ReduceTo<LongestCommonSubsequence> for MinimumVertexCover<SimpleGraph, One> {
     type Result = ReductionVCToLCS;
diff --git a/src/unit_tests/rules/longestcommonsubsequence_maximumindependentset.rs b/src/unit_tests/rules/longestcommonsubsequence_maximumindependentset.rs
index 7daf6a1e0..f8510ba66 100644
--- a/src/unit_tests/rules/longestcommonsubsequence_maximumindependentset.rs
+++ b/src/unit_tests/rules/longestcommonsubsequence_maximumindependentset.rs
@@ -1,150 +1,145 @@
 use super::*;
-use crate::rules::test_helpers::assert_optimization_round_trip_from_optimization_target;
-use crate::solvers::BruteForce;
-use crate::topology::Graph;
+use crate::solvers::{BruteForce, ILPSolver};
 use crate::traits::Problem;
+use crate::types::Max;
 
 #[test]
-fn test_longestcommonsubsequence_to_maximumindependentset_closed_loop() {
-    // Issue example: k=2, s1="ABAC", s2="BACA", alphabet={A=0, B=1, C=2}
-    let lcs = LongestCommonSubsequence::new(
-        3,
-        vec![
-            vec![0, 1, 0, 2], // ABAC
-            vec![1, 0, 2, 0], // BACA
-        ],
-    );
-    let reduction = ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&lcs)
-        .expect("reduction should succeed");
-    assert_optimization_round_trip_from_optimization_target(
-        &lcs,
-        &reduction,
-        "LCS->MIS (ABAC/BACA)",
+fn test_lcs_to_mis_polynomial_bound_for_repeated_strings() {
+    let source = LongestCommonSubsequence::new(1, vec![vec![0, 0]; 16]);
+    let graph = crate::rules::ReductionGraph::new();
+    let entry = graph
+        .find_entry(
+            "LongestCommonSubsequence",
+            &crate::export::variant_to_map(LongestCommonSubsequence::variant()),
+            "MaximumIndependentSet",
+            &crate::export::variant_to_map(MaximumIndependentSet::<SimpleGraph, One>::variant()),
+        )
+        .unwrap();
+    let predicted = entry
+        .parameter_contract
+        .as_ref()
+        .unwrap()
+        .transform()
+        .unwrap()
+        .evaluate(&source.parameters())
+        .unwrap();
+    // Two slots, one symbol, 32 input positions, and 16 strings.
+    assert_eq!(predicted.get("num_vertices"), Some(202));
+    let reduction =
+        ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&source).unwrap();
+    assert_eq!(reduction.target_problem().num_vertices(), 202);
+    assert!(
+        u64::try_from(reduction.target_problem().num_edges()).unwrap()
+            <= predicted.get("num_edges").unwrap()
     );
+    assert_round_trip(&source, 2);
+
+    // Parameters must not calculate the obsolete exponential statistic.
+    let many_strings = LongestCommonSubsequence::new(1, vec![vec![0, 0]; 64]);
+    assert_eq!(many_strings.parameters().get("num_strings"), Some(64));
 }
 
-#[test]
-fn test_lcs_to_mis_graph_structure() {
-    // Issue example: should produce 6 vertices, 9 edges
-    let lcs = LongestCommonSubsequence::new(
-        3,
-        vec![
-            vec![0, 1, 0, 2], // ABAC
-            vec![1, 0, 2, 0], // BACA
-        ],
+fn assert_round_trip(source: &LongestCommonSubsequence, length: i64) {
+    let source_solution = BruteForce::new().solve(source).unwrap().unwrap();
+    assert_eq!(
+        source.evaluate(&source_solution).unwrap(),
+        Max(Some(length))
     );
-    let reduction = ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&lcs)
-        .expect("reduction should succeed");
+    let reduction = ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(source).unwrap();
     let target = reduction.target_problem();
-
-    assert_eq!(target.graph().num_vertices(), 6);
-    assert_eq!(target.graph().num_edges(), 9);
-}
-
-#[test]
-fn test_lcs_to_mis_cross_frequency_product() {
-    // s1="ABAC" has A:2, B:1, C:1
-    // s2="BACA" has A:2, B:1, C:1
-    // cross_freq = 2*2 + 1*1 + 1*1 = 6
-    let lcs = LongestCommonSubsequence::new(3, vec![vec![0, 1, 0, 2], vec![1, 0, 2, 0]]);
-    assert_eq!(lcs.cross_frequency_product(), 6);
+    let solution = ILPSolver::new().solve(target).unwrap();
+    let baseline = i64::try_from(2 * source.max_length() * (source.num_strings() + 1)).unwrap();
+    assert_eq!(
+        target.evaluate(&solution).unwrap(),
+        Max(Some(baseline + length))
+    );
+    let decoded = reduction.extract_solution(&solution).unwrap();
+    assert_eq!(source.evaluate(&decoded).unwrap(), Max(Some(length)));
 }
 
 #[test]
-fn test_lcs_to_mis_optimal_value() {
-    // LCS of "ABAC" and "BACA" is "BAC" (length 3)
-    let lcs = LongestCommonSubsequence::new(3, vec![vec![0, 1, 0, 2], vec![1, 0, 2, 0]]);
-    let reduction = ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&lcs)
-        .expect("reduction should succeed");
-    let target = reduction.target_problem();
-
-    let solver = BruteForce::new();
-    let witness = solver
-        .solve(target)
-        .unwrap()
-        .expect("should have a solution");
-    let mis_size: usize = witness.iter().filter(|&&selected| selected).count();
-    assert_eq!(mis_size, 3);
+fn test_longestcommonsubsequence_to_maximumindependentset_closed_loop() {
+    assert_round_trip(
+        &LongestCommonSubsequence::new(3, vec![vec![0, 1, 0, 2], vec![1, 0, 2, 0]]),
+        3,
+    );
 }
 
 #[test]
-fn test_lcs_to_mis_three_strings() {
-    // k=3 strings over binary alphabet
-    let lcs = LongestCommonSubsequence::new(2, vec![vec![0, 1, 0], vec![1, 0, 1], vec![0, 1, 1]]);
-    let reduction = ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&lcs)
-        .expect("reduction should succeed");
-    assert_optimization_round_trip_from_optimization_target(
-        &lcs,
-        &reduction,
-        "LCS->MIS (3 strings)",
-    );
+fn test_lcs_to_mis_ordering_across_multiple_strings() {
+    for (strings, length) in [
+        (vec![vec![0, 1, 0], vec![1, 0, 1], vec![0, 1, 1]], 2),
+        (vec![vec![0, 1], vec![1, 0], vec![0, 1], vec![1, 0]], 1),
+        (vec![vec![0, 1, 0]], 3),
+    ] {
+        assert_round_trip(&LongestCommonSubsequence::new(2, strings), length);
+    }
 }
 
 #[test]
-fn test_lcs_to_mis_single_char_alphabet() {
-    // All same character: LCS = min length
-    let lcs = LongestCommonSubsequence::new(1, vec![vec![0, 0, 0], vec![0, 0]]);
-    let reduction = ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&lcs)
-        .expect("reduction should succeed");
-    assert_optimization_round_trip_from_optimization_target(
-        &lcs,
-        &reduction,
-        "LCS->MIS (single char)",
-    );
+fn test_lcs_to_mis_empty_common_subsequence_and_empty_inputs() {
+    for (alphabet, strings) in [
+        (2, vec![vec![0, 0], vec![1, 1]]),
+        (2, vec![vec![0, 1], vec![]]),
+        (0, vec![]),
+    ] {
+        assert_round_trip(&LongestCommonSubsequence::new(alphabet, strings), 0);
+    }
 }
 
 #[test]
-fn test_lcs_to_mis_no_common_chars() {
-    // No common characters: LCS = 0
-    let lcs = LongestCommonSubsequence::new(2, vec![vec![0, 0, 0], vec![1, 1, 1]]);
-    let reduction = ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&lcs)
-        .expect("reduction should succeed");
+fn test_lcs_to_mis_rejects_malformed_or_incomplete_encodings() {
+    let source = LongestCommonSubsequence::new(1, vec![vec![0]]);
+    let reduction =
+        ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&source).unwrap();
     let target = reduction.target_problem();
-
-    // No match nodes since no character appears in both strings at any position
-    // cross_freq = 0*3 + 3*0 = 0
-    assert_eq!(target.graph().num_vertices(), 0);
-    assert_eq!(lcs.cross_frequency_product(), 0);
+    assert!(reduction
+        .extract_solution(&vec![false; target.num_vertices() - 1])
+        .is_err());
+    assert!(reduction
+        .extract_solution(&vec![true; target.num_vertices()])
+        .is_err());
+    assert!(reduction
+        .extract_solution(&vec![false; target.num_vertices()])
+        .is_err());
+    // One complete symbol cluster, with its embedding group missing.
+    let symbol_only = vec![true, true, true, false, false, false, false, false, false];
+    assert_eq!(target.evaluate(&symbol_only).unwrap(), Max(Some(3)));
+    assert!(reduction.extract_solution(&symbol_only).is_err());
+    let mut partial = ILPSolver::new().solve(target).unwrap();
+    let selected = partial.iter().position(|&bit| bit).unwrap();
+    partial[selected] = false;
+    assert!(target.evaluate(&partial).unwrap().0.is_some());
+    assert!(reduction.extract_solution(&partial).is_err());
 }
 
 #[test]
-fn test_lcs_to_mis_extract_solution() {
-    let lcs = LongestCommonSubsequence::new(
-        3,
-        vec![
-            vec![0, 1, 0, 2], // ABAC
-            vec![1, 0, 2, 0], // BACA
-        ],
+fn test_lcs_to_mis_complete_nonoptimal_encoding_decodes() {
+    let source = LongestCommonSubsequence::new(1, vec![vec![0]]);
+    let reduction =
+        ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&source).unwrap();
+    // Symbol choices are [active (3), padding (2)]; position choices are
+    // [position 0 (2), padding (2)]. Select both padding clusters.
+    let solution = vec![false, false, false, true, true, false, false, true, true];
+    assert_eq!(
+        reduction.target_problem().evaluate(&solution).unwrap(),
+        Max(Some(4))
     );
-    let reduction = ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&lcs)
-        .expect("reduction should succeed");
-
-    // Vertices: A nodes at indices 0-3, B node at index 4, C node at index 5
-    // Actually the ordering depends on implementation: char 0 (A) first, then 1 (B), then 2 (C)
-    // Let's verify by solving
-    let solver = BruteForce::new();
-    let witness = solver
-        .solve(reduction.target_problem())
-        .unwrap()
-        .expect("should have a solution");
-    let source_sol = reduction.extract_solution(&witness).unwrap();
-
-    // The extracted solution should be valid for the source
-    let value = lcs.evaluate(&source_sol).unwrap();
-    assert!(value.0.is_some(), "extracted solution should be valid");
-    assert_eq!(value.0.unwrap(), 3, "LCS length should be 3");
+    let decoded = reduction.extract_solution(&solution).unwrap();
+    assert_eq!(decoded, vec![None]);
+    assert_eq!(source.evaluate(&decoded).unwrap(), Max(Some(0)));
 }
 
 #[test]
-fn test_lcs_to_mis_four_strings() {
-    // k=4 strings
-    let lcs =
-        LongestCommonSubsequence::new(2, vec![vec![0, 1], vec![1, 0], vec![0, 1], vec![1, 0]]);
-    let reduction = ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&lcs)
-        .expect("reduction should succeed");
-    assert_optimization_round_trip_from_optimization_target(
-        &lcs,
-        &reduction,
-        "LCS->MIS (4 strings)",
+fn test_lcs_to_mis_ignores_unused_declared_symbols() {
+    let source = LongestCommonSubsequence::new(usize::MAX, vec![vec![usize::MAX - 1]]);
+    let reduction =
+        ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&source).unwrap();
+    assert_eq!(source.parameters().get("num_distinct_symbols"), Some(1));
+    assert_eq!(reduction.target_problem().num_vertices(), 9);
+    let solution = ILPSolver::new().solve(reduction.target_problem()).unwrap();
+    assert_eq!(
+        reduction.extract_solution(&solution).unwrap(),
+        vec![Some(usize::MAX - 1)]
     );
 }

From d0010360eb87aeab409e2528e12ac17982370c16 Mon Sep 17 00:00:00 2001
From: Xiwei Pan <90967972+isPANN@users.noreply.github.com>
Date: Sat, 10 Oct 2026 08:41:31 -0700
Subject: [PATCH 2/5] Check sparse LCS target optimum with brute force

---
 .../longestcommonsubsequence_maximumindependentset.rs    | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/src/unit_tests/rules/longestcommonsubsequence_maximumindependentset.rs b/src/unit_tests/rules/longestcommonsubsequence_maximumindependentset.rs
index f8510ba66..aa4ab89c1 100644
--- a/src/unit_tests/rules/longestcommonsubsequence_maximumindependentset.rs
+++ b/src/unit_tests/rules/longestcommonsubsequence_maximumindependentset.rs
@@ -137,7 +137,14 @@ fn test_lcs_to_mis_ignores_unused_declared_symbols() {
         ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&source).unwrap();
     assert_eq!(source.parameters().get("num_distinct_symbols"), Some(1));
     assert_eq!(reduction.target_problem().num_vertices(), 9);
-    let solution = ILPSolver::new().solve(reduction.target_problem()).unwrap();
+    let solution = BruteForce::new()
+        .solve(reduction.target_problem())
+        .unwrap()
+        .unwrap();
+    assert_eq!(
+        reduction.target_problem().evaluate(&solution).unwrap(),
+        Max(Some(5))
+    );
     assert_eq!(
         reduction.extract_solution(&solution).unwrap(),
         vec![Some(usize::MAX - 1)]

From cd16fbf2fefac56a88c1930643b1d93fa683f3e0 Mon Sep 17 00:00:00 2001
From: Xiwei Pan <90967972+isPANN@users.noreply.github.com>
Date: Sat, 10 Oct 2026 10:15:50 -0700
Subject: [PATCH 3/5] Keep LCS conflict graphs compact with a capped hybrid

---
 docs/paper/reductions.typ                     |  27 +-
 problemreductions-cli/tests/cli_tests.rs      |   4 +-
 src/models/misc/longest_common_subsequence.rs |  42 +-
 src/models/misc/mod.rs                        |   1 +
 ...commonsubsequence_maximumindependentset.rs | 368 ++++++++++--------
 ...mumvertexcover_longestcommonsubsequence.rs |   2 +-
 .../models/misc/longest_common_subsequence.rs |  26 ++
 ...commonsubsequence_maximumindependentset.rs | 253 ++++++++----
 8 files changed, 457 insertions(+), 266 deletions(-)

diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ
index c65801b08..4f76da0e7 100644
--- a/docs/paper/reductions.typ
+++ b/docs/paper/reductions.typ
@@ -14038,10 +14038,9 @@ The following reductions to Integer Linear Programming are straightforward formu
 #let lcs_mis_sol = lcs_mis.solutions.at(0)
 #let lcs_mis_length = lcs_mis_sol.source_config.filter(x => x != none).len()
 #let lcs_mis_slots = lcs_mis_sol.source_config.len()
-#let lcs_mis_baseline = 2 * lcs_mis_slots * (lcs_mis.source.instance.strings.len() + 1)
 #reduction-rule("LongestCommonSubsequence", "MaximumIndependentSet",
   example: true,
-  example-caption: [Polynomial choice encoding of two strings over a 3-symbol alphabet],
+  example-caption: [Capped tuple encoding of two strings over a 3-symbol alphabet],
   extra: [
     #pred-commands(
       "pred create --example " + rule-spec(lcs_mis) + " -o lcs.json",
@@ -14049,24 +14048,28 @@ The following reductions to Integer Linear Programming are straightforward formu
       "pred solve bundle.json",
       "pred evaluate lcs.json --config " + cli-config(lcs_mis_sol.source_config),
     )
-    The strings #fmt-values(lcs_mis.source.instance.strings.at(0)) and #fmt-values(lcs_mis.source.instance.strings.at(1)) have #lcs_mis_slots slots. There are #lcs_mis.source.instance.strings.len() strings and #lcs_mis.target.instance.graph.num_vertices vertices in the target. Source witness $(#fmt-values(lcs_mis_sol.source_config))$ selects #lcs_mis_length active symbol clusters; filling every group gives MIS size $= #lcs_mis_baseline + #lcs_mis_length = #lcs_mis_sol.target_config.filter(x => x).len()$.
+    The strings #fmt-values(lcs_mis.source.instance.strings.at(0)) and #fmt-values(lcs_mis.source.instance.strings.at(1)) have #lcs_mis_slots slots. Their tuple count fits the cap, giving #lcs_mis.target.instance.graph.num_vertices vertices. Source witness $(#fmt-values(lcs_mis_sol.source_config))$ decodes from target vertices ${#lcs_mis_sol.target_config.enumerate().filter(((i, x)) => x).map(((i, x)) => str(i)).join(", ")}$, with MIS size $= #lcs_mis_sol.target_config.filter(x => x).len() = #lcs_mis_length$.
   ],
 )[
-  Symbol and embedding choice groups give a polynomial-size unweighted conflict graph. With $k$ strings, minimum length $L$, total length $T$, and $A$ distinct symbols occurring in the input, the graph has exactly $L(3A+2+2(T+k))$ vertices and at most the square of this count in edges. Its maximum independent set has size $2L(k+1)$ plus the LCS length. Since $A <= T$, unused declared alphabet symbols cannot inflate the graph.
+  A capped match-tuple graph with a compact anchored fallback gives polynomial overhead while preserving small tuple graphs. Let $s_a$ be the first shortest input string, $L=|s_a|$, $k$ the number of input strings, $T$ their total length, and $F=sum_(r != a) sum_(p=0)^(L-1) |{j:s_r[j]=s_a[p]}|$. With $B=L(k+2)+F$, both target parameters have complete polynomial bounds: $V<=B$ and $E<=B^2$. Since $F<=L(T-L)$, unused declared alphabet symbols cannot inflate the bound.
 ][
-  _Construction._ Let $s_1, dots, s_k$ be the input strings and $L = min_i |s_i|$, with $L=0$ for no strings. Let $Sigma'$ be the set of symbols occurring in these strings, $A=|Sigma'|$, $T=sum_i |s_i|$, and $G=L(k+1)$.
+  _Construction._ Return the empty graph when $L=0$. Otherwise keep $s_a$ first, remove exact duplicate strings and every other string containing $s_a$ as a subsequence, and preserve the remaining input order. Write $k'$ and $F'$ for the retained counts, $G=L k'$, and $B'=L(k'+2)+F'$. Build sparse lists of matching positions over occurring symbols.
 
-  For every slot $p in {0, dots, L-1}$ create a symbol group $X_p$ with choices $Sigma' union {bot}$, where $bot$ means padding. For every string $r$ and slot $p$, create an embedding group $Y_(r,p)$ with choices $0, dots, |s_r|-1$ and padding. Replace each active symbol choice by three mutually nonadjacent vertices, and every embedding or padding choice by two mutually nonadjacent vertices. All vertices of a choice have identical external neighbours.
+  For symbols present in every retained string, count $C'=sum_c product_r "freq"(c,s_r)$ with arithmetic capped at $B'$, before enumeration. When $C'<=B'$, create one vertex for each matching position tuple. Join two tuples unless all coordinates increase strictly in one direction. This is the match-node construction; its optimum equals LCS. Every intermediate Cartesian prefix is bounded by the final tuple count because all participating lists are nonempty.
 
-  For every incompatible pair of choices, add all edges between their clusters. Choices conflict when: (1) they are distinct choices in the same group; (2) they belong to symbol groups at $p<q$, with padding at $p$ and an active symbol at $q$; (3) they belong to $X_p$ and $Y_(r,p)$ and disagree, where padding agrees only with padding and symbol $a$ agrees with position $j$ precisely when $s_r[j]=a$; or (4) they belong to embedding groups for the same string at $p<q$, with padding followed by an active position, or active positions $j,j'$ with $j >= j'$. Check all slot pairs, including nonadjacent slots. There are no other edges.
+  The alternative polynomial encoding creates an anchor group $X_p$ at every anchor position $p$: two nonadjacent active twins and one skip vertex adjacent to both. For each other retained string $r$, create a clique $Y_(r,p)$ with one vertex per matching position $j$ and one skip vertex. Join the anchor twins to the embedding skip, and the anchor skip to every matching position. Between slots $p<q$ in the same string, join matching vertices $j,j'$ exactly when $j>=j'$. Check all slot pairs, including nonadjacent ones. There are no other edges. Anchor groups contribute $3L$ vertices and embeddings $L(k'-1)+F'$, exactly $B'$ in total. If $C'>B'$, use this encoding without enumerating tuples. Otherwise choose the graph with fewer vertices plus edges, preferring tuples on a tie. A tuple graph with $C'+E_T<=B'$ wins without constructing the alternative. For other admitted tuple graphs, compare $E_T-E_A>B'-C'$ without adding potentially overflowing totals.
 
-  _Correctness._ ($arrow.r.double$) Any common subsequence of length $ell$ selects its symbols in the first $ell$ slots and increasing embedding positions in every string, followed by padding. Taking every vertex of each selected choice cluster gives an independent set of size $2G+ell$.
+  _Correctness._ Removing a containing string preserves every candidate by transitivity of subsequence inclusion; duplicates repeat the same constraint. Thus preprocessing preserves the entire feasible source set. For tuples, pairwise compatibility is a strictly increasing chain in every string, so selecting tuples and reading their common symbols maps common subsequences to independent sets and conversely, preserving length.
 
-  ($arrow.l.double$) A maximum independent set fills every cluster it touches: any omitted vertex of that cluster can be added. It touches at most one choice per group. Suppose $d_X$ symbol groups and $d_Y$ embedding groups are missing, and $q$ active symbol choices are selected. Discard each active slot lacking an embedding group; this removes at most $d_Y$ letters. The remaining letters match strictly increasing positions in every string, so $q <= "LCS" + d_Y$. Its size is at most
-  $2(G-d_X-d_Y)+q <= 2G+"LCS"-2d_X-d_Y.$
-  Missing any group makes this strictly smaller than the full encoding of an optimal common subsequence. Therefore every optimum fills all groups, its symbols form a valid padded common subsequence, and its size is exactly $2G+"LCS"$. If $L=0$, both optima are zero and the graph is empty.
+  For the anchored branch ($arrow.r.double$), a common subsequence of length $ell$ selects both active twins at its anchor positions and increasing matching positions in every retained string, using skips elsewhere. It gives an independent set of size $G+ell$.
 
-  _Solution extraction._ Validate independence, reject partial clusters or missing groups, then read the original symbol labels selected in $X_0, dots, X_(L-1)$. Every optimum passes these checks. A complete nonoptimal encoding also decodes to a valid source witness. The metadata parameter `num_distinct_symbols` supplies $A$; construction uses $O(V^2+T log(T+1)+k)$ time and extraction $O(V+E)$ time including validation.
+  ($arrow.l.double$) Any maximum independent set saturates the active twins, since they have identical external neighbours. Let $q$ be its active anchor choices and $d_X,d_Y$ its empty anchor and embedding groups. Its size is $G-d_X-d_Y+q$. Discard active anchor positions with any missing embedding; each discarded position has a distinct empty embedding group, so at most $d_Y$ are discarded. The remaining $ell>=q-d_Y$ letters embed in strictly increasing positions in every retained string. Hence
+  $G-d_X-d_Y+q<=G+ell-d_X<=G+"LCS".$
+  Forward construction attains equality, so every optimum has $d_X=0$ and decodes an optimal common subsequence, even when embedding groups are empty. The anchored optimum is $G+"LCS"$.
+
+  _Solution extraction._ Validate independence once. In the tuple branch sort selected tuples by anchor position and read their symbols. In the anchored branch reject partial twin pairs; retain only active anchor positions with a selected matching position in every embedding group. Read the original symbols in anchor order and pack them before trailing padding. Every optimal target witness decodes optimally; accepted nonoptimal witnesses decode feasibly.
+
+  _Overhead._ The selected graph has either $C'$ or $B'$ vertices, in both cases at most $B$, and edges are at most $B^2$. Selection minimizes vertices plus edges among the admitted constructions; it may use more vertices to save edges. Thus the registered relations are upper bounds. Removing strings cannot increase $k'$ or $F'$, and removes only positive frequency factors from each common-symbol tuple count. Metadata `anchor_matching_pairs` supplies the original $F$. For MVC-derived inputs with $N$ vertices and $M$ edges, $L=N$, $k=M+1$, $F=2M(N-1)$, giving $V<=3N+3 M N-2M$. Construction uses sparse input positions and no declared-alphabet iteration; validated extraction takes $O(V log(V+1)+E)$ time.
 ]
 
 #let cs_ilp_str = load-example(
diff --git a/problemreductions-cli/tests/cli_tests.rs b/problemreductions-cli/tests/cli_tests.rs
index 8d8cc42e4..f1b6348d7 100644
--- a/problemreductions-cli/tests/cli_tests.rs
+++ b/problemreductions-cli/tests/cli_tests.rs
@@ -5696,8 +5696,8 @@ fn test_vertex_cover_via_lcs_to_mis_solves_and_recovers_optimum() {
         String::from_utf8_lossy(&reduced.stderr)
     );
     let data: serde_json::Value = serde_json::from_slice(&std::fs::read(&bundle).unwrap()).unwrap();
-    // L=3, A=3, k=3, T=11: V=3*(9+2+28)=117.
-    assert_eq!(data["target"]["data"]["graph"]["num_vertices"], 117);
+    // Vertex-symbol frequencies give 2 alignments for 0, 1 for 1, and 2 for 2.
+    assert_eq!(data["target"]["data"]["graph"]["num_vertices"], 5);
     let solved = pred()
         .args([
             "solve",
diff --git a/src/models/misc/longest_common_subsequence.rs b/src/models/misc/longest_common_subsequence.rs
index 7145d55df..c1561ca5f 100644
--- a/src/models/misc/longest_common_subsequence.rs
+++ b/src/models/misc/longest_common_subsequence.rs
@@ -41,6 +41,8 @@ pub struct LongestCommonSubsequence {
     alphabet_size: usize,
     strings: Vec<Vec<usize>>,
     max_length: usize,
+    #[serde(skip)]
+    anchor_matching_pairs: u64,
 }
 
 #[derive(Deserialize)]
@@ -122,10 +124,32 @@ impl LongestCommonSubsequence {
         {
             return Err("input symbols must be less than alphabet_size".into());
         }
+        let mut anchor_matching_pairs = 0u64;
+        if let Some((anchor, input)) = strings
+            .iter()
+            .enumerate()
+            .min_by_key(|(_, s)| s.len())
+            .filter(|(_, s)| !s.is_empty())
+        {
+            let mut frequencies = std::collections::HashMap::<usize, u64>::new();
+            for &symbol in input {
+                *frequencies.entry(symbol).or_default() += 1;
+            }
+            for (r, string) in strings.iter().enumerate() {
+                if r != anchor {
+                    for symbol in string {
+                        anchor_matching_pairs = anchor_matching_pairs
+                            .checked_add(frequencies.get(symbol).copied().unwrap_or(0))
+                            .ok_or("anchor matching-pair count exceeds u64")?;
+                    }
+                }
+            }
+        }
         Ok(Self {
             alphabet_size,
             strings,
             max_length,
+            anchor_matching_pairs,
         })
     }
 
@@ -167,13 +191,10 @@ impl LongestCommonSubsequence {
             .sum()
     }
 
-    /// Returns the number of distinct symbols occurring in the input strings.
-    pub fn num_distinct_symbols(&self) -> usize {
-        self.strings
-            .iter()
-            .flatten()
-            .collect::<std::collections::BTreeSet<_>>()
-            .len()
+    /// Equal-symbol position pairs between the first shortest string and all others.
+    /// Counts the original input strings before a reduction removes redundancy.
+    pub fn anchor_matching_pairs(&self) -> u64 {
+        self.anchor_matching_pairs
     }
 
     /// Returns the number of adjacent position transitions.
@@ -188,7 +209,8 @@ impl LongestCommonSubsequence {
     /// where count(c, s) is the number of occurrences of symbol c in string s.
     ///
     /// This statistic describes the legacy match-tuple expansion, not the
-    /// polynomial-size choice graph used by the LCS → MaxIS reduction.
+    /// capped hybrid used by the LCS → MaxIS reduction. This uncapped getter
+    /// is not a canonical parameter and can overflow for many repeated strings.
     pub fn cross_frequency_product(&self) -> usize {
         (0..self.alphabet_size)
             .map(|c| {
@@ -203,7 +225,7 @@ impl LongestCommonSubsequence {
 
 /// Check whether `candidate` is a subsequence of `target` using greedy
 /// left-to-right matching.
-fn is_subsequence(candidate: &[usize], target: &[usize]) -> bool {
+pub(crate) fn is_subsequence(candidate: &[usize], target: &[usize]) -> bool {
     let mut it = target.iter();
     for &symbol in candidate {
         loop {
@@ -226,7 +248,7 @@ impl Problem for LongestCommonSubsequence {
         ("alphabet_size", alphabet_size),
         ("max_length", max_length),
         ("num_strings", num_strings),
-        ("num_distinct_symbols", num_distinct_symbols),
+        ("anchor_matching_pairs", anchor_matching_pairs),
         ("num_transitions", num_transitions),
         ("sum_triangular_lengths", sum_triangular_lengths),
         ("total_length", total_length),
diff --git a/src/models/misc/mod.rs b/src/models/misc/mod.rs
index e18f75d24..83dd2e2b3 100644
--- a/src/models/misc/mod.rs
+++ b/src/models/misc/mod.rs
@@ -213,6 +213,7 @@ pub use integer_expression_membership::{IntExpr, IntegerExpressionMembership};
 pub use job_shop_scheduling::JobShopScheduling;
 pub use knapsack::Knapsack;
 pub use kth_largest_m_tuple::KthLargestMTuple;
+pub(crate) use longest_common_subsequence::is_subsequence;
 pub use longest_common_subsequence::LongestCommonSubsequence;
 pub use maximum_likelihood_ranking::MaximumLikelihoodRanking;
 pub use minimum_axiom_set::MinimumAxiomSet;
diff --git a/src/rules/longestcommonsubsequence_maximumindependentset.rs b/src/rules/longestcommonsubsequence_maximumindependentset.rs
index 17e74d7dd..ff394cb57 100644
--- a/src/rules/longestcommonsubsequence_maximumindependentset.rs
+++ b/src/rules/longestcommonsubsequence_maximumindependentset.rs
@@ -1,33 +1,33 @@
-//! Polynomial-size LCS reduction using symbol and embedding choice groups.
+//! Capped match-tuple graph with a polynomial anchored fallback.
 //!
-//! Each choice is an independent cluster: two vertices for a position or padding,
-//! three for an active symbol. Conflicts enforce one choice per group, matching
-//! characters, increasing positions, and a padding suffix. Every optimum fills
-//! all groups; its size is 2 * max_length * (num_strings + 1) plus the LCS length.
+//! Redundant strings are removed first. Tuple vertices preserve the LCS value;
+//! for k retained strings, anchored graphs have L * k plus the LCS value.
+//! The cap is L * (k + 2) + F,
+//! where F counts equal-symbol position pairs against a shortest input string.
 
 use crate::models::graph::MaximumIndependentSet;
-use crate::models::misc::LongestCommonSubsequence;
+use crate::models::misc::{is_subsequence, LongestCommonSubsequence};
 use crate::reduction;
 use crate::rules::traits::{ReduceTo, ReductionResult};
 use crate::topology::SimpleGraph;
 use crate::types::One;
+use std::collections::{BTreeMap, HashSet};
 use std::ops::Range;
 
 #[derive(Debug, Clone)]
-struct Choice {
-    group: usize,
-    slot: usize,
-    string: Option<usize>,
-    value: Option<usize>,
-    vertices: Range<usize>,
+enum Encoding {
+    Tuples(Vec<(usize, Vec<usize>)>),
+    Anchored {
+        anchor: Vec<usize>,
+        embeddings: Vec<Vec<Range<usize>>>,
+    },
 }
 
-/// Stores the choice clusters needed to decode a complete independent set.
+/// Target graph and the selected mathematical witness mapping.
 #[derive(Debug, Clone)]
 pub struct ReductionLCSToIS {
     target: MaximumIndependentSet<SimpleGraph, One>,
-    choices: Vec<Choice>,
-    num_groups: usize,
+    encoding: Encoding,
     max_length: usize,
 }
 
@@ -49,150 +49,165 @@ impl ReductionResult for ReductionLCSToIS {
             |value| value.0.is_some(),
             "selected vertices do not form an independent set",
         )?;
-        let mut selected_groups = vec![false; self.num_groups];
-        let mut decoded = vec![None; self.max_length];
-        for choice in &self.choices {
-            let selected = solution[choice.vertices.clone()]
-                .iter()
-                .filter(|&&bit| bit)
-                .count();
-            if selected == 0 {
-                continue;
-            }
-            if selected != choice.vertices.len() {
-                return Err(crate::rules::ExtractionError::invalid(
-                    "selected choice cluster is incomplete",
-                ));
+        let mut decoded = Vec::with_capacity(self.max_length);
+        match &self.encoding {
+            Encoding::Tuples(nodes) => {
+                let mut selected = nodes
+                    .iter()
+                    .zip(solution)
+                    .filter(|(_, bit)| **bit)
+                    .map(|((symbol, positions), _)| (positions[0], *symbol))
+                    .collect::<Vec<_>>();
+                selected.sort_unstable_by_key(|&(position, _)| position);
+                decoded.extend(selected.into_iter().map(|(_, symbol)| Some(symbol)));
             }
-            selected_groups[choice.group] = true;
-            if choice.group < self.max_length {
-                decoded[choice.group] = choice.value;
+            Encoding::Anchored { anchor, embeddings } => {
+                for (p, &symbol) in anchor.iter().enumerate() {
+                    if solution[3 * p] != solution[3 * p + 1] {
+                        return Err(crate::rules::ExtractionError::invalid(
+                            "active anchor twins are incomplete",
+                        ));
+                    }
+                    if solution[3 * p]
+                        && embeddings.iter().all(|groups| {
+                            let group = &groups[p];
+                            solution[group.start..group.end - 1].iter().any(|&bit| bit)
+                        })
+                    {
+                        decoded.push(Some(symbol));
+                    }
+                }
             }
         }
-        if let Some(group) = selected_groups.iter().position(|&selected| !selected) {
-            return Err(crate::rules::ExtractionError::invalid(format!(
-                "choice group {group} has no selected choice"
-            )));
+        while decoded.len() < self.max_length {
+            decoded.push(None);
         }
         Ok(decoded)
     }
 }
 
-#[reduction(
-    transform = {
-        exact {
-            num_vertices = "max_length * (3 * num_distinct_symbols + 2 + 2 * (total_length + num_strings))",
-        },
-        upper_bound {
-            num_edges = "(max_length * (3 * num_distinct_symbols + 2 + 2 * (total_length + num_strings)))^2",
-        },
-    }
-)]
+#[reduction(transform = upper_bound {
+    num_vertices = "max_length * (num_strings + 2) + anchor_matching_pairs",
+    num_edges = "(max_length * (num_strings + 2) + anchor_matching_pairs)^2",
+})]
 impl ReduceTo<MaximumIndependentSet<SimpleGraph, One>> for LongestCommonSubsequence {
     type Result = ReductionLCSToIS;
 
     fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
+        if self.max_length() == 0 {
+            return Ok(ReductionLCSToIS {
+                target: MaximumIndependentSet::new(SimpleGraph::new(0, vec![]), vec![]),
+                encoding: Encoding::Tuples(vec![]),
+                max_length: 0,
+            });
+        }
         let overflow = || {
             crate::rules::ReductionError::integer_overflow::<
                 Self,
                 MaximumIndependentSet<SimpleGraph, One>,
-            >("counting choice vertices")
+            >("counting anchored vertices")
         };
-        let total_length = self
+        let anchor = self
             .strings()
             .iter()
-            .try_fold(0usize, |total, string| total.checked_add(string.len()))
-            .ok_or_else(overflow)?;
-        let symbols = self
-            .strings()
-            .iter()
-            .flatten()
-            .copied()
-            .collect::<std::collections::BTreeSet<_>>()
-            .into_iter()
+            .min_by_key(|s| s.len())
+            .map(Vec::as_slice)
+            .unwrap_or_default();
+        let mut seen = HashSet::new();
+        let retained = std::iter::once(anchor).chain(
+            self.strings()
+                .iter()
+                .map(Vec::as_slice)
+                .filter(|string| !is_subsequence(anchor, string) && seen.insert(*string)),
+        );
+        let positions = retained
+            .map(|string| {
+                let mut map = BTreeMap::<usize, Vec<usize>>::new();
+                for (j, &symbol) in string.iter().enumerate() {
+                    map.entry(symbol).or_default().push(j);
+                }
+                map
+            })
             .collect::<Vec<_>>();
-        let per_slot = symbols
-            .len()
-            .checked_mul(3)
-            .and_then(|value| value.checked_add(2))
-            .and_then(|value| {
-                total_length
-                    .checked_add(self.num_strings())?
-                    .checked_mul(2)?
-                    .checked_add(value)
+
+        // Only nonempty position lists enter the product; a later absent symbol
+        // must contribute zero before any multiplication can exceed the cap.
+        let common = positions[0]
+            .keys()
+            .filter_map(|&symbol| {
+                let lists = positions
+                    .iter()
+                    .map(|map| map.get(&symbol).map(Vec::as_slice))
+                    .collect::<Option<Vec<_>>>()?;
+                Some((symbol, lists))
             })
-            .ok_or_else(overflow)?;
-        let num_vertices = self
-            .max_length()
-            .checked_mul(per_slot)
-            .ok_or_else(overflow)?;
+            .collect::<Vec<_>>();
+        let mut cap = anchor.len().checked_mul(3).ok_or_else(overflow)?;
+        for map in &positions[1..] {
+            for symbol in anchor {
+                cap = cap
+                    .checked_add(map.get(symbol).map_or(0, Vec::len))
+                    .and_then(|count| count.checked_add(1))
+                    .ok_or_else(overflow)?;
+            }
+        }
+        let tuple_count = common.iter().try_fold(0usize, |total, (_, lists)| {
+            let product = lists.iter().try_fold(1usize, |product, list| {
+                product
+                    .checked_mul(list.len())
+                    .filter(|&count| count <= cap)
+            })?;
+            total.checked_add(product).filter(|&count| count <= cap)
+        });
+        let mut num_vertices = tuple_count.unwrap_or(cap);
         <Self as ReduceTo<MaximumIndependentSet<SimpleGraph, One>>>::exact_i64(
             num_vertices,
             "representing the independent-set objective",
         )?;
-        let mut choices = Vec::new();
-        let mut cursor = 0usize;
-        let mut num_groups = 0;
-        let mut add_group = |slot, string: Option<usize>, values: &[usize]| {
-            for value in values
-                .iter()
-                .copied()
-                .map(Some)
-                .chain(std::iter::once(None))
-            {
-                let count = if string.is_none() && value.is_some() {
-                    3
-                } else {
-                    2
-                };
-                let end = cursor.checked_add(count).ok_or_else(overflow)?;
-                choices.push(Choice {
-                    group: num_groups,
-                    slot,
-                    string,
-                    value,
-                    vertices: cursor..end,
-                });
-                cursor = end;
-            }
-            num_groups += 1;
-            Ok::<_, crate::rules::ReductionError>(())
-        };
-        for slot in 0..self.max_length() {
-            add_group(slot, None, &symbols)?;
-        }
-        for (string, input) in self.strings().iter().enumerate() {
-            let positions = (0..input.len()).collect::<Vec<_>>();
-            for slot in 0..self.max_length() {
-                add_group(slot, Some(string), &positions)?;
-            }
-        }
         let mut edges = Vec::new();
-        for (i, left) in choices.iter().enumerate() {
-            for right in &choices[i + 1..] {
-                let conflict = if left.group == right.group {
-                    true
-                } else {
-                    // Groups are generated in slot order, with symbols before embeddings.
-                    match (left.string, right.string) {
-                        (None, None) => left.value.is_none() && right.value.is_some(),
-                        (Some(a), Some(b)) if a == b => right
-                            .value
-                            .is_some_and(|j| left.value.is_none_or(|i| i >= j)),
-                        (None, Some(string)) if left.slot == right.slot => {
-                            left.value != right.value.map(|j| self.strings()[string][j])
-                        }
-                        _ => false,
-                    }
-                };
-                if conflict {
-                    for a in left.vertices.clone() {
-                        for b in right.vertices.clone() {
-                            edges.push((a, b));
-                        }
+        let mut encoding = if tuple_count.is_some() {
+            let mut nodes = Vec::with_capacity(num_vertices);
+            for (symbol, lists) in common {
+                let mut tuples = vec![Vec::new()];
+                for list in lists {
+                    tuples = tuples
+                        .into_iter()
+                        .flat_map(|prefix| {
+                            list.iter().map(move |&position| {
+                                let mut tuple = prefix.clone();
+                                tuple.push(position);
+                                tuple
+                            })
+                        })
+                        .collect();
+                }
+                nodes.extend(tuples.into_iter().map(|tuple| (symbol, tuple)));
+            }
+            for (i, (_, left)) in nodes.iter().enumerate() {
+                for (j, (_, right)) in nodes.iter().enumerate().skip(i + 1) {
+                    if !left.iter().zip(right).all(|(a, b)| a < b)
+                        && !left.iter().zip(right).all(|(a, b)| a > b)
+                    {
+                        edges.push((i, j));
                     }
                 }
             }
+            Encoding::Tuples(nodes)
+        } else {
+            let (anchor_edges, anchor_encoding) = anchored_graph(anchor, &positions, cap)?;
+            edges = anchor_edges;
+            anchor_encoding
+        };
+        // A tuple graph costing at most the anchor's vertices alone cannot lose.
+        if tuple_count.is_some() && edges.len() > cap - num_vertices {
+            let (anchor_edges, anchor_encoding) = anchored_graph(anchor, &positions, cap)?;
+            if edges.len() > anchor_edges.len()
+                && edges.len() - anchor_edges.len() > cap - num_vertices
+            {
+                num_vertices = cap;
+                edges = anchor_edges;
+                encoding = anchor_encoding;
+            }
         }
         let target = MaximumIndependentSet::new(
             SimpleGraph::new(num_vertices, edges),
@@ -200,13 +215,63 @@ impl ReduceTo<MaximumIndependentSet<SimpleGraph, One>> for LongestCommonSubseque
         );
         Ok(ReductionLCSToIS {
             target,
-            choices,
-            num_groups,
+            encoding,
             max_length: self.max_length(),
         })
     }
 }
 
+fn anchored_graph(
+    anchor: &[usize],
+    positions: &[BTreeMap<usize, Vec<usize>>],
+    cap: usize,
+) -> Result<(Vec<(usize, usize)>, Encoding), crate::rules::ReductionError> {
+    <LongestCommonSubsequence as ReduceTo<MaximumIndependentSet<SimpleGraph, One>>>::exact_i64(
+        cap,
+        "representing the anchored independent-set objective",
+    )?;
+    let mut edges = Vec::new();
+    let mut cursor = anchor.len() * 3;
+    let mut embeddings = Vec::with_capacity(positions.len() - 1);
+    for p in 0..anchor.len() {
+        edges.extend([(3 * p, 3 * p + 2), (3 * p + 1, 3 * p + 2)]);
+    }
+    for map in &positions[1..] {
+        let mut groups = Vec::<(&[usize], Range<usize>)>::with_capacity(anchor.len());
+        for (p, symbol) in anchor.iter().enumerate() {
+            let matches = map.get(symbol).map(Vec::as_slice).unwrap_or_default();
+            let group = cursor..cursor + matches.len() + 1;
+            cursor = group.end;
+            for a in group.clone() {
+                for b in a + 1..group.end {
+                    edges.push((a, b));
+                }
+            }
+            let skip = group.end - 1;
+            edges.extend([(3 * p, skip), (3 * p + 1, skip)]);
+            edges.extend((group.start..skip).map(|j| (3 * p + 2, j)));
+            // Only this string's earlier slots can cross. Sorted matches let
+            // us emit exactly the conflicting prefix of each group.
+            for (earlier, previous) in &groups {
+                for (i, &position) in earlier.iter().enumerate() {
+                    let conflicts = matches.partition_point(|&j| j <= position);
+                    edges.extend((0..conflicts).map(|j| (previous.start + i, group.start + j)));
+                }
+            }
+            groups.push((matches, group));
+        }
+        embeddings.push(groups.into_iter().map(|(_, range)| range).collect());
+    }
+    debug_assert_eq!(cursor, cap);
+    Ok((
+        edges,
+        Encoding::Anchored {
+            anchor: anchor.to_vec(),
+            embeddings,
+        },
+    ))
+}
+
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
     use crate::export::SolutionPair;
@@ -215,36 +280,15 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
         id: "longestcommonsubsequence_to_maximumindependentset",
         build: || {
             let source = LongestCommonSubsequence::new(3, vec![vec![0, 1, 0, 2], vec![1, 0, 2, 0]]);
-            let reduction = ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&source)
-                .expect("reduction should succeed");
-            // BAC, then padding; its positions are (1,2,3) and (0,1,2).
-            let assignments = [
-                Some(1),
-                Some(0),
-                Some(2),
-                None,
-                Some(1),
-                Some(2),
-                Some(3),
-                None,
-                Some(0),
-                Some(1),
-                Some(2),
-                None,
-            ];
-            let mut target_config = vec![false; reduction.target.num_vertices()];
-            for choice in &reduction.choices {
-                if assignments[choice.group] == choice.value {
-                    target_config[choice.vertices.clone()].fill(true);
-                }
-            }
-            crate::example_db::specs::assemble_rule_example(
-                &source,
-                reduction.target_problem(),
-                vec![SolutionPair {
-                    source_config: serde_json::json!(&assignments[..source.max_length()]),
-                    target_config: serde_json::json!(target_config),
-                }],
+            crate::example_db::specs::rule_example_with_witness::<
+                _,
+                MaximumIndependentSet<SimpleGraph, One>,
+            >(
+                source,
+                SolutionPair {
+                    source_config: serde_json::json!(vec![Some(1), Some(0), Some(2), None]),
+                    target_config: serde_json::json!(vec![false, false, true, false, true, true]),
+                },
             )
         },
     }]
diff --git a/src/rules/minimumvertexcover_longestcommonsubsequence.rs b/src/rules/minimumvertexcover_longestcommonsubsequence.rs
index 92762e3f9..644fbd5df 100644
--- a/src/rules/minimumvertexcover_longestcommonsubsequence.rs
+++ b/src/rules/minimumvertexcover_longestcommonsubsequence.rs
@@ -42,7 +42,7 @@ impl ReductionResult for ReductionVCToLCS {
     transform = {
         exact {
             alphabet_size = "num_vertices",
-            num_distinct_symbols = "num_vertices",
+            anchor_matching_pairs = "2 * num_edges * (num_vertices - 1)",
             num_strings = "num_edges + 1",
             max_length = "num_vertices",
             total_length = "num_vertices + 2 * num_edges * num_vertices - 2 * num_edges",
diff --git a/src/unit_tests/models/misc/longest_common_subsequence.rs b/src/unit_tests/models/misc/longest_common_subsequence.rs
index ac7665979..0b3bc935f 100644
--- a/src/unit_tests/models/misc/longest_common_subsequence.rs
+++ b/src/unit_tests/models/misc/longest_common_subsequence.rs
@@ -4,6 +4,32 @@ use crate::solvers::BruteForceProblem as _;
 use crate::traits::Problem;
 use crate::types::Max;
 
+#[test]
+fn test_lcs_anchor_matching_pairs_uses_first_shortest_string() {
+    let source =
+        LongestCommonSubsequence::new(2, vec![vec![0, 0, 1], vec![0, 1, 1], vec![0, 0, 0, 1]]);
+    assert_eq!(source.parameters().get("anchor_matching_pairs"), Some(11));
+    let reordered =
+        LongestCommonSubsequence::new(2, vec![vec![0, 1, 1], vec![0, 0, 1], vec![0, 0, 0, 1]]);
+    assert_eq!(reordered.parameters().get("anchor_matching_pairs"), Some(9));
+    let restored: LongestCommonSubsequence =
+        serde_json::from_value(serde_json::to_value(&source).unwrap()).unwrap();
+    assert_eq!(restored.parameters(), source.parameters());
+    for strings in [
+        vec![],
+        vec![vec![]],
+        vec![vec![0]],
+        vec![vec![], vec![0, 1]],
+    ] {
+        assert_eq!(
+            LongestCommonSubsequence::new(2, strings)
+                .parameters()
+                .get("anchor_matching_pairs"),
+            Some(0)
+        );
+    }
+}
+
 fn issue_yes_instance() -> LongestCommonSubsequence {
     LongestCommonSubsequence::new(
         2,
diff --git a/src/unit_tests/rules/longestcommonsubsequence_maximumindependentset.rs b/src/unit_tests/rules/longestcommonsubsequence_maximumindependentset.rs
index aa4ab89c1..f2b0cc090 100644
--- a/src/unit_tests/rules/longestcommonsubsequence_maximumindependentset.rs
+++ b/src/unit_tests/rules/longestcommonsubsequence_maximumindependentset.rs
@@ -3,9 +3,94 @@ use crate::solvers::{BruteForce, ILPSolver};
 use crate::traits::Problem;
 use crate::types::Max;
 
+fn assert_round_trip(source: &LongestCommonSubsequence, length: i64, target_value: i64) {
+    let source_solution = BruteForce::new().solve(source).unwrap().unwrap();
+    assert_eq!(
+        source.evaluate(&source_solution).unwrap(),
+        Max(Some(length))
+    );
+    let reduction = ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(source).unwrap();
+    let target = reduction.target_problem();
+    let solution = if target.num_vertices() <= 12 {
+        BruteForce::new().solve(target).unwrap().unwrap()
+    } else {
+        ILPSolver::new().solve(target).unwrap()
+    };
+    assert_eq!(target.evaluate(&solution).unwrap(), Max(Some(target_value)));
+    let decoded = reduction.extract_solution(&solution).unwrap();
+    assert_eq!(source.evaluate(&decoded).unwrap(), Max(Some(length)));
+}
+
 #[test]
-fn test_lcs_to_mis_polynomial_bound_for_repeated_strings() {
-    let source = LongestCommonSubsequence::new(1, vec![vec![0, 0]; 16]);
+fn test_longestcommonsubsequence_to_maximumindependentset_closed_loop() {
+    let source = LongestCommonSubsequence::new(3, vec![vec![0, 1, 0, 2], vec![1, 0, 2, 0]]);
+    let reduction =
+        ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&source).unwrap();
+    // Four A alignments, one B alignment, and one C alignment.
+    assert_eq!(reduction.target_problem().num_vertices(), 6);
+    assert_round_trip(&source, 3, 3);
+}
+
+#[test]
+fn test_lcs_to_mis_removes_redundant_strings() {
+    let repeated = LongestCommonSubsequence::new(1, vec![vec![0, 0]; 64]);
+    let reduction =
+        ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&repeated).unwrap();
+    assert_eq!(reduction.target_problem().num_vertices(), 2);
+    assert_eq!(reduction.target_problem().num_edges(), 0);
+    assert_round_trip(&repeated, 2, 2);
+
+    let source = LongestCommonSubsequence::new(
+        3,
+        vec![vec![2, 0, 1, 2], vec![0, 1], vec![0, 1], vec![1, 0]],
+    );
+    let reduction =
+        ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&source).unwrap();
+    assert_eq!(reduction.target_problem().num_vertices(), 2);
+    assert_eq!(reduction.target_problem().num_edges(), 1);
+    assert_eq!(source.parameters().get("anchor_matching_pairs"), Some(6));
+    assert_round_trip(&source, 1, 1);
+}
+
+fn crossing_strings(longer: usize) -> LongestCommonSubsequence {
+    let blocks = |count| [vec![1; count], vec![0; count]].concat();
+    LongestCommonSubsequence::new(2, vec![vec![0, 1], blocks(3), blocks(longer)])
+}
+
+#[test]
+fn test_lcs_to_mis_caps_tuple_expansion_before_allocation() {
+    // At the 24-vertex cap, the tuple graph is a clique (276 edges).
+    // The anchored graph has the same vertices and only 83 edges.
+    let at_cap = crossing_strings(4);
+    let reduction =
+        ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&at_cap).unwrap();
+    assert_eq!(reduction.target_problem().num_vertices(), 24);
+    assert_eq!(reduction.target_problem().num_edges(), 83);
+    assert_round_trip(&at_cap, 1, 7);
+
+    // 30 tuples exceed the cap: 6 anchor vertices + (6+2)+(10+2) embeddings.
+    let source = crossing_strings(5);
+    let reduction =
+        ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&source).unwrap();
+    assert_eq!(reduction.target_problem().num_vertices(), 26);
+    assert_round_trip(&source, 1, 7);
+
+    // Sixty-four distinct balanced binary strings would have 2*4^64 tuples.
+    let strings = (0u8..=u8::MAX)
+        .filter(|bits| bits.count_ones() == 4)
+        .take(64)
+        .map(|bits| (0..8).map(|p| usize::from((bits >> p) & 1)).collect())
+        .collect();
+    let source = LongestCommonSubsequence::new(2, strings);
+    let reduction =
+        ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&source).unwrap();
+    assert_eq!(reduction.target_problem().num_vertices(), 2544);
+    assert_eq!(source.parameters().get("anchor_matching_pairs"), Some(2016));
+}
+
+#[test]
+fn test_lcs_to_mis_polynomial_parameter_bound() {
+    let source = crossing_strings(5);
     let graph = crate::rules::ReductionGraph::new();
     let entry = graph
         .find_entry(
@@ -15,81 +100,67 @@ fn test_lcs_to_mis_polynomial_bound_for_repeated_strings() {
             &crate::export::variant_to_map(MaximumIndependentSet::<SimpleGraph, One>::variant()),
         )
         .unwrap();
-    let predicted = entry
+    let transform = entry
         .parameter_contract
         .as_ref()
         .unwrap()
         .transform()
-        .unwrap()
-        .evaluate(&source.parameters())
         .unwrap();
-    // Two slots, one symbol, 32 input positions, and 16 strings.
-    assert_eq!(predicted.get("num_vertices"), Some(202));
+    let predicted = transform.evaluate(&source.parameters()).unwrap();
+    assert_eq!(predicted.get("num_vertices"), Some(26));
+    assert_eq!(predicted.get("num_edges"), Some(676));
     let reduction =
         ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&source).unwrap();
-    assert_eq!(reduction.target_problem().num_vertices(), 202);
-    assert!(
-        u64::try_from(reduction.target_problem().num_edges()).unwrap()
-            <= predicted.get("num_edges").unwrap()
-    );
-    assert_round_trip(&source, 2);
-
-    // Parameters must not calculate the obsolete exponential statistic.
-    let many_strings = LongestCommonSubsequence::new(1, vec![vec![0, 0]; 64]);
-    assert_eq!(many_strings.parameters().get("num_strings"), Some(64));
-}
-
-fn assert_round_trip(source: &LongestCommonSubsequence, length: i64) {
-    let source_solution = BruteForce::new().solve(source).unwrap().unwrap();
-    assert_eq!(
-        source.evaluate(&source_solution).unwrap(),
-        Max(Some(length))
-    );
-    let reduction = ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(source).unwrap();
-    let target = reduction.target_problem();
-    let solution = ILPSolver::new().solve(target).unwrap();
-    let baseline = i64::try_from(2 * source.max_length() * (source.num_strings() + 1)).unwrap();
-    assert_eq!(
-        target.evaluate(&solution).unwrap(),
-        Max(Some(baseline + length))
-    );
-    let decoded = reduction.extract_solution(&solution).unwrap();
-    assert_eq!(source.evaluate(&decoded).unwrap(), Max(Some(length)));
+    assert!(u64::try_from(reduction.target_problem().num_edges()).unwrap() <= 676);
 }
 
 #[test]
-fn test_longestcommonsubsequence_to_maximumindependentset_closed_loop() {
-    assert_round_trip(
-        &LongestCommonSubsequence::new(3, vec![vec![0, 1, 0, 2], vec![1, 0, 2, 0]]),
-        3,
+fn test_lcs_to_mis_selects_by_vertices_and_edges() {
+    // There are 24 zero-tuples (3*2*2*2), but almost every pair conflicts.
+    // The 36-vertex anchored graph is smaller when its 96 edges are included.
+    let source = LongestCommonSubsequence::new(
+        2,
+        vec![vec![0, 0, 0], vec![0, 0, 1], vec![0, 1, 0], vec![1, 0, 0]],
     );
-}
+    let reduction =
+        ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&source).unwrap();
+    assert_eq!(reduction.target_problem().num_vertices(), 36);
+    assert_eq!(reduction.target_problem().num_edges(), 96);
+    assert_round_trip(&source, 2, 14);
 
-#[test]
-fn test_lcs_to_mis_ordering_across_multiple_strings() {
-    for (strings, length) in [
-        (vec![vec![0, 1, 0], vec![1, 0, 1], vec![0, 1, 1]], 2),
-        (vec![vec![0, 1], vec![1, 0], vec![0, 1], vec![1, 0]], 1),
-        (vec![vec![0, 1, 0]], 3),
-    ] {
-        assert_round_trip(&LongestCommonSubsequence::new(2, strings), length);
-    }
+    // Both constructions cost 133 vertices plus edges; keep the tuple graph.
+    let source = LongestCommonSubsequence::new(
+        2,
+        vec![vec![0, 0, 0, 1], vec![0, 1, 0, 1], vec![1, 1, 0, 0]],
+    );
+    let reduction =
+        ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&source).unwrap();
+    assert_eq!(reduction.target_problem().num_vertices(), 16);
+    assert_eq!(reduction.target_problem().num_edges(), 117);
+    assert_round_trip(&source, 2, 2);
 }
 
 #[test]
-fn test_lcs_to_mis_empty_common_subsequence_and_empty_inputs() {
-    for (alphabet, strings) in [
-        (2, vec![vec![0, 0], vec![1, 1]]),
-        (2, vec![vec![0, 1], vec![]]),
-        (0, vec![]),
+fn test_lcs_to_mis_ordering_and_empty_common_subsequences() {
+    for (alphabet, strings, length) in [
+        (2, vec![vec![0, 1, 0], vec![1, 0, 1], vec![0, 1, 1]], 2),
+        (2, vec![vec![0, 1], vec![1, 0], vec![0, 1], vec![1, 0]], 1),
+        (2, vec![vec![0, 1, 0]], 3),
+        (2, vec![vec![0, 0], vec![1, 1]], 0),
+        (2, vec![vec![0, 1], vec![]], 0),
+        (0, vec![], 0),
     ] {
-        assert_round_trip(&LongestCommonSubsequence::new(alphabet, strings), 0);
+        assert_round_trip(
+            &LongestCommonSubsequence::new(alphabet, strings),
+            length,
+            length,
+        );
     }
 }
 
 #[test]
-fn test_lcs_to_mis_rejects_malformed_or_incomplete_encodings() {
-    let source = LongestCommonSubsequence::new(1, vec![vec![0]]);
+fn test_lcs_to_mis_rejects_invalid_and_partial_twin_witnesses() {
+    let source = crossing_strings(5);
     let reduction =
         ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&source).unwrap();
     let target = reduction.target_problem();
@@ -99,51 +170,75 @@ fn test_lcs_to_mis_rejects_malformed_or_incomplete_encodings() {
     assert!(reduction
         .extract_solution(&vec![true; target.num_vertices()])
         .is_err());
-    assert!(reduction
-        .extract_solution(&vec![false; target.num_vertices()])
-        .is_err());
-    // One complete symbol cluster, with its embedding group missing.
-    let symbol_only = vec![true, true, true, false, false, false, false, false, false];
-    assert_eq!(target.evaluate(&symbol_only).unwrap(), Max(Some(3)));
-    assert!(reduction.extract_solution(&symbol_only).is_err());
-    let mut partial = ILPSolver::new().solve(target).unwrap();
-    let selected = partial.iter().position(|&bit| bit).unwrap();
-    partial[selected] = false;
-    assert!(target.evaluate(&partial).unwrap().0.is_some());
+    let mut partial = vec![false; target.num_vertices()];
+    partial[0] = true;
+    assert_eq!(target.evaluate(&partial).unwrap(), Max(Some(1)));
     assert!(reduction.extract_solution(&partial).is_err());
 }
 
 #[test]
-fn test_lcs_to_mis_complete_nonoptimal_encoding_decodes() {
-    let source = LongestCommonSubsequence::new(1, vec![vec![0]]);
+fn test_lcs_to_mis_decodes_missing_embedding_groups() {
+    let source = crossing_strings(5);
     let reduction =
         ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&source).unwrap();
-    // Symbol choices are [active (3), padding (2)]; position choices are
-    // [position 0 (2), padding (2)]. Select both padding clusters.
-    let solution = vec![false, false, false, true, true, false, false, true, true];
+    let mut solution = vec![false; reduction.target_problem().num_vertices()];
+    solution[..2].fill(true);
     assert_eq!(
         reduction.target_problem().evaluate(&solution).unwrap(),
-        Max(Some(4))
+        Max(Some(2))
     );
     let decoded = reduction.extract_solution(&solution).unwrap();
-    assert_eq!(decoded, vec![None]);
+    assert_eq!(decoded, vec![None, None]);
     assert_eq!(source.evaluate(&decoded).unwrap(), Max(Some(0)));
+
+    let source = LongestCommonSubsequence::new(
+        3,
+        vec![
+            vec![0, 0, 0, 0, 0, 0, 1, 2],
+            vec![1, 0, 0, 0, 0, 0, 0, 2],
+            vec![2, 0, 0, 0, 0, 0, 0, 1],
+        ],
+    );
+    let reduction =
+        ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&source).unwrap();
+    assert_eq!(reduction.target_problem().num_vertices(), 116);
+    // Activate seven anchor slots but omit the first string's embedding of 1.
+    // Six zeros still embed in both strings, giving an optimal 30-vertex set.
+    let mut solution = vec![false; 116];
+    for p in 0..7 {
+        solution[3 * p..3 * p + 2].fill(true);
+    }
+    for p in 0..6 {
+        solution[24 + 8 * p] = true;
+        solution[70 + 8 * p] = true;
+    }
+    for vertex in [23, 69, 112, 115] {
+        solution[vertex] = true;
+    }
+    assert_eq!(
+        reduction.target_problem().evaluate(&solution).unwrap(),
+        Max(Some(30))
+    );
+    assert_eq!(
+        reduction.extract_solution(&solution).unwrap(),
+        [vec![Some(0); 6], vec![None; 2]].concat()
+    );
+    assert_round_trip(&source, 6, 30);
 }
 
 #[test]
-fn test_lcs_to_mis_ignores_unused_declared_symbols() {
+fn test_lcs_to_mis_preserves_sparse_original_symbols() {
     let source = LongestCommonSubsequence::new(usize::MAX, vec![vec![usize::MAX - 1]]);
     let reduction =
         ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&source).unwrap();
-    assert_eq!(source.parameters().get("num_distinct_symbols"), Some(1));
-    assert_eq!(reduction.target_problem().num_vertices(), 9);
+    assert_eq!(reduction.target_problem().num_vertices(), 1);
     let solution = BruteForce::new()
         .solve(reduction.target_problem())
         .unwrap()
         .unwrap();
     assert_eq!(
         reduction.target_problem().evaluate(&solution).unwrap(),
-        Max(Some(5))
+        Max(Some(1))
     );
     assert_eq!(
         reduction.extract_solution(&solution).unwrap(),

From 69f59884c656c454e0e741bbdcb153dd9d4e03e9 Mon Sep 17 00:00:00 2001
From: Xiwei Pan <90967972+isPANN@users.noreply.github.com>
Date: Sat, 10 Oct 2026 10:29:16 -0700
Subject: [PATCH 4/5] Prune impossible LCS anchor letters before graph encoding

---
 docs/paper/reductions.typ                     |  8 ++--
 ...commonsubsequence_maximumindependentset.rs | 48 ++++++++++++++-----
 ...commonsubsequence_maximumindependentset.rs | 27 +++++++++++
 3 files changed, 66 insertions(+), 17 deletions(-)

diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ
index 4f76da0e7..fef7e1685 100644
--- a/docs/paper/reductions.typ
+++ b/docs/paper/reductions.typ
@@ -14053,13 +14053,13 @@ The following reductions to Integer Linear Programming are straightforward formu
 )[
   A capped match-tuple graph with a compact anchored fallback gives polynomial overhead while preserving small tuple graphs. Let $s_a$ be the first shortest input string, $L=|s_a|$, $k$ the number of input strings, $T$ their total length, and $F=sum_(r != a) sum_(p=0)^(L-1) |{j:s_r[j]=s_a[p]}|$. With $B=L(k+2)+F$, both target parameters have complete polynomial bounds: $V<=B$ and $E<=B^2$. Since $F<=L(T-L)$, unused declared alphabet symbols cannot inflate the bound.
 ][
-  _Construction._ Return the empty graph when $L=0$. Otherwise keep $s_a$ first, remove exact duplicate strings and every other string containing $s_a$ as a subsequence, and preserve the remaining input order. Write $k'$ and $F'$ for the retained counts, $G=L k'$, and $B'=L(k'+2)+F'$. Build sparse lists of matching positions over occurring symbols.
+  _Construction._ Return the empty graph when $L=0$. Otherwise keep $s_a$ first, remove exact duplicate strings and every other string containing $s_a$ as a subsequence, and preserve the remaining input order. Build sparse lists of matching positions over occurring symbols. Keep only letters present in every remaining string in the anchor, giving length $L'<=L$, then remove other remaining strings containing this filtered anchor. Keep the common-symbol set fixed so removing a constraint cannot reintroduce an unavailable letter. Write $k'$ and $F'$ for the final retained counts, $G=L' k'$, and $B'=L'(k'+2)+F'$.
 
   For symbols present in every retained string, count $C'=sum_c product_r "freq"(c,s_r)$ with arithmetic capped at $B'$, before enumeration. When $C'<=B'$, create one vertex for each matching position tuple. Join two tuples unless all coordinates increase strictly in one direction. This is the match-node construction; its optimum equals LCS. Every intermediate Cartesian prefix is bounded by the final tuple count because all participating lists are nonempty.
 
-  The alternative polynomial encoding creates an anchor group $X_p$ at every anchor position $p$: two nonadjacent active twins and one skip vertex adjacent to both. For each other retained string $r$, create a clique $Y_(r,p)$ with one vertex per matching position $j$ and one skip vertex. Join the anchor twins to the embedding skip, and the anchor skip to every matching position. Between slots $p<q$ in the same string, join matching vertices $j,j'$ exactly when $j>=j'$. Check all slot pairs, including nonadjacent ones. There are no other edges. Anchor groups contribute $3L$ vertices and embeddings $L(k'-1)+F'$, exactly $B'$ in total. If $C'>B'$, use this encoding without enumerating tuples. Otherwise choose the graph with fewer vertices plus edges, preferring tuples on a tie. A tuple graph with $C'+E_T<=B'$ wins without constructing the alternative. For other admitted tuple graphs, compare $E_T-E_A>B'-C'$ without adding potentially overflowing totals.
+  The alternative polynomial encoding creates an anchor group $X_p$ at every anchor position $p$: two nonadjacent active twins and one skip vertex adjacent to both. For each other retained string $r$, create a clique $Y_(r,p)$ with one vertex per matching position $j$ and one skip vertex. Join the anchor twins to the embedding skip, and the anchor skip to every matching position. Between slots $p<q$ in the same string, join matching vertices $j,j'$ exactly when $j>=j'$. Check all slot pairs, including nonadjacent ones. There are no other edges. Anchor groups contribute $3L'$ vertices and embeddings $L'(k'-1)+F'$, exactly $B'$ in total. If $C'>B'$, use this encoding without enumerating tuples. Otherwise choose the graph with fewer vertices plus edges, preferring tuples on a tie. A tuple graph with $C'+E_T<=B'$ wins without constructing the alternative. For other admitted tuple graphs, compare $E_T-E_A>B'-C'$ without adding potentially overflowing totals.
 
-  _Correctness._ Removing a containing string preserves every candidate by transitivity of subsequence inclusion; duplicates repeat the same constraint. Thus preprocessing preserves the entire feasible source set. For tuples, pairwise compatibility is a strictly increasing chain in every string, so selecting tuples and reading their common symbols maps common subsequences to independent sets and conversely, preserving length.
+  _Correctness._ Removing a containing string preserves every candidate by transitivity of subsequence inclusion; duplicates repeat the same constraint. Every common word uses only symbols present in all strings, so filtering the anchor preserves every candidate; the filtered anchor is itself a subsequence of the original. Thus preprocessing preserves the entire feasible source set. For tuples, pairwise compatibility is a strictly increasing chain in every string, so selecting tuples and reading their common symbols maps common subsequences to independent sets and conversely, preserving length.
 
   For the anchored branch ($arrow.r.double$), a common subsequence of length $ell$ selects both active twins at its anchor positions and increasing matching positions in every retained string, using skips elsewhere. It gives an independent set of size $G+ell$.
 
@@ -14069,7 +14069,7 @@ The following reductions to Integer Linear Programming are straightforward formu
 
   _Solution extraction._ Validate independence once. In the tuple branch sort selected tuples by anchor position and read their symbols. In the anchored branch reject partial twin pairs; retain only active anchor positions with a selected matching position in every embedding group. Read the original symbols in anchor order and pack them before trailing padding. Every optimal target witness decodes optimally; accepted nonoptimal witnesses decode feasibly.
 
-  _Overhead._ The selected graph has either $C'$ or $B'$ vertices, in both cases at most $B$, and edges are at most $B^2$. Selection minimizes vertices plus edges among the admitted constructions; it may use more vertices to save edges. Thus the registered relations are upper bounds. Removing strings cannot increase $k'$ or $F'$, and removes only positive frequency factors from each common-symbol tuple count. Metadata `anchor_matching_pairs` supplies the original $F$. For MVC-derived inputs with $N$ vertices and $M$ edges, $L=N$, $k=M+1$, $F=2M(N-1)$, giving $V<=3N+3 M N-2M$. Construction uses sparse input positions and no declared-alphabet iteration; validated extraction takes $O(V log(V+1)+E)$ time.
+  _Overhead._ The selected graph has either $C'$ or $B'$ vertices, in both cases at most $B$, and edges are at most $B^2$. Selection minimizes vertices plus edges among the admitted constructions; it may use more vertices to save edges. Thus the registered relations are upper bounds. Removing anchor letters and strings cannot increase $L'$, $k'$ or $F'$, and removes only positive frequency factors from each common-symbol tuple count. Metadata `anchor_matching_pairs` supplies the original $F$. For MVC-derived inputs with $N$ vertices and $M$ edges, $L=N$, $k=M+1$, $F=2M(N-1)$, giving $V<=3N+3 M N-2M$. Construction uses sparse input positions and no declared-alphabet iteration; validated extraction takes $O(V log(V+1)+E)$ time.
 ]
 
 #let cs_ilp_str = load-example(
diff --git a/src/rules/longestcommonsubsequence_maximumindependentset.rs b/src/rules/longestcommonsubsequence_maximumindependentset.rs
index ff394cb57..ad093aab6 100644
--- a/src/rules/longestcommonsubsequence_maximumindependentset.rs
+++ b/src/rules/longestcommonsubsequence_maximumindependentset.rs
@@ -1,9 +1,9 @@
 //! Capped match-tuple graph with a polynomial anchored fallback.
 //!
-//! Redundant strings are removed first. Tuple vertices preserve the LCS value;
-//! for k retained strings, anchored graphs have L * k plus the LCS value.
-//! The cap is L * (k + 2) + F,
-//! where F counts equal-symbol position pairs against a shortest input string.
+//! Remove redundant strings and impossible anchor letters first. Tuple graphs
+//! preserve LCS; anchored optima are L * k + LCS for k retained strings.
+//! Both graphs have at most L * (k + 2) + F vertices, where L is the filtered
+//! anchor length and F counts matches against it. Original input counts bound these.
 
 use crate::models::graph::MaximumIndependentSet;
 use crate::models::misc::{is_subsequence, LongestCommonSubsequence};
@@ -114,13 +114,16 @@ impl ReduceTo<MaximumIndependentSet<SimpleGraph, One>> for LongestCommonSubseque
             .map(Vec::as_slice)
             .unwrap_or_default();
         let mut seen = HashSet::new();
-        let retained = std::iter::once(anchor).chain(
-            self.strings()
-                .iter()
-                .map(Vec::as_slice)
-                .filter(|string| !is_subsequence(anchor, string) && seen.insert(*string)),
-        );
+        let retained = std::iter::once(anchor)
+            .chain(
+                self.strings()
+                    .iter()
+                    .map(Vec::as_slice)
+                    .filter(|string| !is_subsequence(anchor, string) && seen.insert(*string)),
+            )
+            .collect::<Vec<_>>();
         let positions = retained
+            .iter()
             .map(|string| {
                 let mut map = BTreeMap::<usize, Vec<usize>>::new();
                 for (j, &symbol) in string.iter().enumerate() {
@@ -129,11 +132,30 @@ impl ReduceTo<MaximumIndependentSet<SimpleGraph, One>> for LongestCommonSubseque
                 map
             })
             .collect::<Vec<_>>();
+        let common_symbols = positions[0]
+            .keys()
+            .copied()
+            .filter(|symbol| positions.iter().all(|map| map.contains_key(symbol)))
+            .collect::<HashSet<_>>();
+        let anchor = anchor
+            .iter()
+            .copied()
+            .filter(|symbol| common_symbols.contains(symbol))
+            .collect::<Vec<_>>();
+        let positions = positions
+            .into_iter()
+            .zip(retained)
+            .enumerate()
+            .filter(|(r, (_, string))| *r == 0 || !is_subsequence(&anchor, string))
+            .map(|(_, (map, _))| map)
+            .collect::<Vec<_>>();
 
         // Only nonempty position lists enter the product; a later absent symbol
         // must contribute zero before any multiplication can exceed the cap.
         let common = positions[0]
             .keys()
+            // Removing a constraint must not reintroduce an impossible letter.
+            .filter(|symbol| common_symbols.contains(symbol))
             .filter_map(|&symbol| {
                 let lists = positions
                     .iter()
@@ -144,7 +166,7 @@ impl ReduceTo<MaximumIndependentSet<SimpleGraph, One>> for LongestCommonSubseque
             .collect::<Vec<_>>();
         let mut cap = anchor.len().checked_mul(3).ok_or_else(overflow)?;
         for map in &positions[1..] {
-            for symbol in anchor {
+            for symbol in &anchor {
                 cap = cap
                     .checked_add(map.get(symbol).map_or(0, Vec::len))
                     .and_then(|count| count.checked_add(1))
@@ -194,13 +216,13 @@ impl ReduceTo<MaximumIndependentSet<SimpleGraph, One>> for LongestCommonSubseque
             }
             Encoding::Tuples(nodes)
         } else {
-            let (anchor_edges, anchor_encoding) = anchored_graph(anchor, &positions, cap)?;
+            let (anchor_edges, anchor_encoding) = anchored_graph(&anchor, &positions, cap)?;
             edges = anchor_edges;
             anchor_encoding
         };
         // A tuple graph costing at most the anchor's vertices alone cannot lose.
         if tuple_count.is_some() && edges.len() > cap - num_vertices {
-            let (anchor_edges, anchor_encoding) = anchored_graph(anchor, &positions, cap)?;
+            let (anchor_edges, anchor_encoding) = anchored_graph(&anchor, &positions, cap)?;
             if edges.len() > anchor_edges.len()
                 && edges.len() - anchor_edges.len() > cap - num_vertices
             {
diff --git a/src/unit_tests/rules/longestcommonsubsequence_maximumindependentset.rs b/src/unit_tests/rules/longestcommonsubsequence_maximumindependentset.rs
index f2b0cc090..98012e1c8 100644
--- a/src/unit_tests/rules/longestcommonsubsequence_maximumindependentset.rs
+++ b/src/unit_tests/rules/longestcommonsubsequence_maximumindependentset.rs
@@ -140,6 +140,33 @@ fn test_lcs_to_mis_selects_by_vertices_and_edges() {
     assert_round_trip(&source, 2, 2);
 }
 
+#[test]
+fn test_lcs_to_mis_removes_impossible_anchor_letters() {
+    let source = LongestCommonSubsequence::new(
+        3,
+        vec![
+            vec![0, 0, 1, 2],
+            [vec![1; 3], vec![0; 5]].concat(),
+            [vec![1; 4], vec![0; 6]].concat(),
+        ],
+    );
+    // Only 001 remains in the anchor: 9 anchor vertices + 29 matches + 6 skips.
+    // Anchor edges 6, embedding cliques 88, consistency 41, crossings 114.
+    let reduction =
+        ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&source).unwrap();
+    assert_eq!(reduction.target_problem().num_vertices(), 44);
+    assert_eq!(reduction.target_problem().num_edges(), 249);
+    assert_round_trip(&source, 2, 11);
+
+    // After removing the absent 1, both other strings contain the whole anchor.
+    let source = LongestCommonSubsequence::new(2, vec![vec![0, 0, 1], vec![0; 5], vec![0; 6]]);
+    let reduction =
+        ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&source).unwrap();
+    assert_eq!(reduction.target_problem().num_vertices(), 2);
+    assert_eq!(reduction.target_problem().num_edges(), 0);
+    assert_round_trip(&source, 2, 2);
+}
+
 #[test]
 fn test_lcs_to_mis_ordering_and_empty_common_subsequences() {
     for (alphabet, strings, length) in [

From 29ba7b5870fd4ded51c45aec791904966125a87b Mon Sep 17 00:00:00 2001
From: Xiwei Pan <90967972+isPANN@users.noreply.github.com>
Date: Sun, 11 Oct 2026 03:14:38 -0700
Subject: [PATCH 5/5] Rebuild LCS to MIS as a normalized reward-anchored hybrid

Normalize the input (common anchor letters, drop strings containing the
filtered anchor, dedupe), then build a reward-anchored graph with one
reward vertex per slot. Use the match-tuple graph instead only when it has
neither more vertices nor more edges, so one explicit polynomial bound
over registered parameters covers both branches:
V <= L(k+T-L), E <= A(S-A) + L(k-1), A = L(L+1)/2.

Both encodings share one decoder. Drop the rule-internal
anchor_matching_pairs and cross_frequency_product parameters, restore the
generic unavailable-field CLI test on another path, and rewrite the paper
entry for the new construction.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 docs/paper/reductions.typ                     |  25 +-
 problemreductions-cli/tests/cli_tests.rs      |  24 +-
 src/models/misc/longest_common_subsequence.rs |  51 ---
 ...commonsubsequence_maximumindependentset.rs | 383 +++++++-----------
 ...mumvertexcover_longestcommonsubsequence.rs |   1 -
 .../models/misc/longest_common_subsequence.rs |  26 --
 ...commonsubsequence_maximumindependentset.rs | 373 +++++++++--------
 7 files changed, 361 insertions(+), 522 deletions(-)

diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ
index fef7e1685..ede29d9cc 100644
--- a/docs/paper/reductions.typ
+++ b/docs/paper/reductions.typ
@@ -14040,7 +14040,7 @@ The following reductions to Integer Linear Programming are straightforward formu
 #let lcs_mis_slots = lcs_mis_sol.source_config.len()
 #reduction-rule("LongestCommonSubsequence", "MaximumIndependentSet",
   example: true,
-  example-caption: [Capped tuple encoding of two strings over a 3-symbol alphabet],
+  example-caption: [Two conflicting match tuples for strings with opposite symbol order],
   extra: [
     #pred-commands(
       "pred create --example " + rule-spec(lcs_mis) + " -o lcs.json",
@@ -14048,28 +14048,27 @@ The following reductions to Integer Linear Programming are straightforward formu
       "pred solve bundle.json",
       "pred evaluate lcs.json --config " + cli-config(lcs_mis_sol.source_config),
     )
-    The strings #fmt-values(lcs_mis.source.instance.strings.at(0)) and #fmt-values(lcs_mis.source.instance.strings.at(1)) have #lcs_mis_slots slots. Their tuple count fits the cap, giving #lcs_mis.target.instance.graph.num_vertices vertices. Source witness $(#fmt-values(lcs_mis_sol.source_config))$ decodes from target vertices ${#lcs_mis_sol.target_config.enumerate().filter(((i, x)) => x).map(((i, x)) => str(i)).join(", ")}$, with MIS size $= #lcs_mis_sol.target_config.filter(x => x).len() = #lcs_mis_length$.
+    The strings #fmt-values(lcs_mis.source.instance.strings.at(0)) and #fmt-values(lcs_mis.source.instance.strings.at(1)) leave one embedding string after normalization, and the source witness has length #lcs_mis_slots. The graph has #lcs_mis.target.instance.graph.num_vertices vertices and #lcs_mis.target.instance.graph.edges.len() edges. Source witness $(#fmt-values(lcs_mis_sol.source_config))$ decodes from target vertices ${#lcs_mis_sol.target_config.enumerate().filter(((i, x)) => x).map(((i, x)) => str(i)).join(", ")}$, with MIS size $= #lcs_mis_sol.target_config.filter(x => x).len() = #lcs_mis_length$.
   ],
 )[
-  A capped match-tuple graph with a compact anchored fallback gives polynomial overhead while preserving small tuple graphs. Let $s_a$ be the first shortest input string, $L=|s_a|$, $k$ the number of input strings, $T$ their total length, and $F=sum_(r != a) sum_(p=0)^(L-1) |{j:s_r[j]=s_a[p]}|$. With $B=L(k+2)+F$, both target parameters have complete polynomial bounds: $V<=B$ and $E<=B^2$. Since $F<=L(T-L)$, unused declared alphabet symbols cannot inflate the bound.
+  Use a match-tuple graph when it has neither more vertices nor more edges than a reward-anchored graph; otherwise use the anchored graph. Let $k$ be the number of input strings, $T$ their total length, $L$ the shortest string length (zero for no strings), $S=sum_r |s_r|(|s_r|+1)\/2$, and $A=L(L+1)\/2$. The target satisfies
+  $ V <= L(k+T-L), quad E <= A(S-A)+L(k-1). $
 ][
-  _Construction._ Return the empty graph when $L=0$. Otherwise keep $s_a$ first, remove exact duplicate strings and every other string containing $s_a$ as a subsequence, and preserve the remaining input order. Build sparse lists of matching positions over occurring symbols. Keep only letters present in every remaining string in the anchor, giving length $L'<=L$, then remove other remaining strings containing this filtered anchor. Keep the common-symbol set fixed so removing a constraint cannot reintroduce an unavailable letter. Write $k'$ and $F'$ for the final retained counts, $G=L' k'$, and $B'=L'(k'+2)+F'$.
+  _Construction._ Choose the first shortest string as the anchor and delete its symbols absent from any input string. Write $a$ for this filtered anchor and $h=|a|$. Filter every other string to the symbols of $a$, omit strings containing $a$ as a subsequence, and remove duplicates, leaving $m$ embedding strings.
 
-  For symbols present in every retained string, count $C'=sum_c product_r "freq"(c,s_r)$ with arithmetic capped at $B'$, before enumeration. When $C'<=B'$, create one vertex for each matching position tuple. Join two tuples unless all coordinates increase strictly in one direction. This is the match-node construction; its optimum equals LCS. Every intermediate Cartesian prefix is bounded by the final tuple count because all participating lists are nonempty.
+  _Anchored encoding._ Create one reward vertex $z_p$ for each anchor position $p$. For each embedding string $s_r$ and position $p$, create a clique $Y_(r,p)$ containing one vertex per position $j$ with $s_r[j]=a[p]$, plus a skip vertex. Join $z_p$ to that skip. Between slots $p<q$ in the same string, join matching vertices $j,j'$ exactly when $j>=j'$. There are no other edges.
 
-  The alternative polynomial encoding creates an anchor group $X_p$ at every anchor position $p$: two nonadjacent active twins and one skip vertex adjacent to both. For each other retained string $r$, create a clique $Y_(r,p)$ with one vertex per matching position $j$ and one skip vertex. Join the anchor twins to the embedding skip, and the anchor skip to every matching position. Between slots $p<q$ in the same string, join matching vertices $j,j'$ exactly when $j>=j'$. Check all slot pairs, including nonadjacent ones. There are no other edges. Anchor groups contribute $3L'$ vertices and embeddings $L'(k'-1)+F'$, exactly $B'$ in total. If $C'>B'$, use this encoding without enumerating tuples. Otherwise choose the graph with fewer vertices plus edges, preferring tuples on a tie. A tuple graph with $C'+E_T<=B'$ wins without constructing the alternative. For other admitted tuple graphs, compare $E_T-E_A>B'-C'$ without adding potentially overflowing totals.
+  _Tuple encoding and selection._ A vertex is a tuple of equal-symbol positions, one in $a$ and one in each embedding string. Two vertices are adjacent unless all coordinates are strictly increasing in the same direction. Its vertex count is $V_t=sum_p product_r |{j:s_r[j]=a[p]}|$; form these tuples only if $V_t<=V_a$. Choose the tuple graph precisely when also $E_t<=E_a$, where subscripts denote the tuple and anchored graphs. Otherwise choose the anchored graph.
 
-  _Correctness._ Removing a containing string preserves every candidate by transitivity of subsequence inclusion; duplicates repeat the same constraint. Every common word uses only symbols present in all strings, so filtering the anchor preserves every candidate; the filtered anchor is itself a subsequence of the original. Thus preprocessing preserves the entire feasible source set. For tuples, pairwise compatibility is a strictly increasing chain in every string, so selecting tuples and reading their common symbols maps common subsequences to independent sets and conversely, preserving length.
+  _Correctness._ Every common subsequence uses only symbols present in all input strings, so filtering the anchor preserves the feasible words. Filtering other strings, removing duplicates, and omitting strings containing the filtered anchor also preserve these words. Tuple independent sets, sorted by anchor position, are exactly common-subsequence embeddings, so their maximum size is $"LCS"$. For the anchored encoding:
 
-  For the anchored branch ($arrow.r.double$), a common subsequence of length $ell$ selects both active twins at its anchor positions and increasing matching positions in every retained string, using skips elsewhere. It gives an independent set of size $G+ell$.
+  ($arrow.r.double$) A common subsequence of length $ell$ selects its reward vertices and increasing matching positions in each embedding string, using skips at the other slots. This gives an independent set of size $h m+ell$.
 
-  ($arrow.l.double$) Any maximum independent set saturates the active twins, since they have identical external neighbours. Let $q$ be its active anchor choices and $d_X,d_Y$ its empty anchor and embedding groups. Its size is $G-d_X-d_Y+q$. Discard active anchor positions with any missing embedding; each discarded position has a distinct empty embedding group, so at most $d_Y$ are discarded. The remaining $ell>=q-d_Y$ letters embed in strictly increasing positions in every retained string. Hence
-  $G-d_X-d_Y+q<=G+ell-d_X<=G+"LCS".$
-  Forward construction attains equality, so every optimum has $d_X=0$ and decodes an optimal common subsequence, even when embedding groups are empty. The anchored optimum is $G+"LCS"$.
+  ($arrow.l.double$) An independent set with $q$ rewards and $d$ empty embedding groups has size $h m+q-d$. A selected reward missing a match in some string has an empty group, because its skip is adjacent to the reward. Discard these rewards; each discarded slot accounts for a distinct empty group. The remaining $ell>=q-d$ symbols form a common subsequence, so the independent-set size is at most $h m+ell<=h m+"LCS"$. The forward construction attains equality, and every optimum decodes an optimal common subsequence. In particular, empty embedding groups are permitted. The two objectives differ, so the reduction registers witness extraction without an aggregate value map.
 
-  _Solution extraction._ Validate independence once. In the tuple branch sort selected tuples by anchor position and read their symbols. In the anchored branch reject partial twin pairs; retain only active anchor positions with a selected matching position in every embedding group. Read the original symbols in anchor order and pack them before trailing padding. Every optimal target witness decodes optimally; accepted nonoptimal witnesses decode feasibly.
+  _Solution extraction._ Validate independence once. Order tuple vertices by anchor position and anchored rewards by anchor slot. Read the symbol of each selected vertex that has a selected match in every embedding string; tuples have no embedding strings, so every selected tuple is read. Pad the result to the original length $L$. This also maps nonoptimal independent sets to feasible common subsequences. With no embedding strings the tuple graph has $h$ isolated vertices and is always selected.
 
-  _Overhead._ The selected graph has either $C'$ or $B'$ vertices, in both cases at most $B$, and edges are at most $B^2$. Selection minimizes vertices plus edges among the admitted constructions; it may use more vertices to save edges. Thus the registered relations are upper bounds. Removing anchor letters and strings cannot increase $L'$, $k'$ or $F'$, and removes only positive frequency factors from each common-symbol tuple count. Metadata `anchor_matching_pairs` supplies the original $F$. For MVC-derived inputs with $N$ vertices and $M$ edges, $L=N$, $k=M+1$, $F=2M(N-1)$, giving $V<=3N+3 M N-2M$. Construction uses sparse input positions and no declared-alphabet iteration; validated extraction takes $O(V log(V+1)+E)$ time.
+  _Overhead._ For $k>=1$, the anchored graph has $h(m+1)+F$ vertices, where $F$ counts retained equal-symbol position pairs. Since $h<=L$, $m<=k-1$, and $F<=L(T-L)$, the vertex bound follows. For one embedding string of length $n$, within-slot cliques contribute at most $h n(n+1)\/2$ edges. Each of the $h(h-1)\/2$ slot pairs contributes at most $n(n+1)\/2$ crossing edges, counting all pairs $j>=j'$. Together these are at most $A n(n+1)\/2$ edges, plus at most $L$ reward-to-skip edges. Summing over a subset of the original non-anchor strings gives $E<=A(S-A)+L(k-1)$. Empty input has $V=E=L=0$ and satisfies both formulas. Dominance transfers both bounds to the tuple branch. All bounds use only registered source parameters.
 ]
 
 #let cs_ilp_str = load-example(
diff --git a/problemreductions-cli/tests/cli_tests.rs b/problemreductions-cli/tests/cli_tests.rs
index f1b6348d7..c2a2c8e55 100644
--- a/problemreductions-cli/tests/cli_tests.rs
+++ b/problemreductions-cli/tests/cli_tests.rs
@@ -5611,12 +5611,12 @@ fn test_path_preserves_exact_variables_and_bounded_quadratic_terms() {
 }
 
 #[test]
-fn test_path_vertex_cover_to_lcs_has_complete_parameter_formulas() {
+fn test_path_overall_preserves_unavailable_fields_alongside_exact_fields() {
     let output = pred()
         .args([
             "path",
-            "MinimumVertexCover/SimpleGraph/One",
-            "LongestCommonSubsequence",
+            "SubsetSum",
+            "DecisionOpenShopScheduling",
             "--limit",
             "1",
             "--json",
@@ -5628,14 +5628,19 @@ fn test_path_vertex_cover_to_lcs_has_complete_parameter_formulas() {
     let fields = envelope["paths"][0]["overall_parameters"]["fields"]
         .as_array()
         .unwrap();
-    let alphabet = fields
+    let machines = fields
         .iter()
-        .find(|field| field["field"] == "alphabet_size")
+        .find(|field| field["field"] == "num_machines")
         .unwrap();
-    assert_eq!(alphabet["relation"], "exact");
-    assert!(fields
+    assert_eq!(machines["relation"], "exact");
+    let horizon = fields
         .iter()
-        .all(|field| field["relation"] != "unavailable"));
+        .find(|field| field["field"] == "schedule_horizon")
+        .unwrap();
+    assert_eq!(horizon["relation"], "unavailable");
+    assert!(horizon["reason"]
+        .as_str()
+        .is_some_and(|reason| !reason.is_empty()));
 }
 
 #[test]
@@ -5695,9 +5700,6 @@ fn test_vertex_cover_via_lcs_to_mis_solves_and_recovers_optimum() {
         "{}",
         String::from_utf8_lossy(&reduced.stderr)
     );
-    let data: serde_json::Value = serde_json::from_slice(&std::fs::read(&bundle).unwrap()).unwrap();
-    // Vertex-symbol frequencies give 2 alignments for 0, 1 for 1, and 2 for 2.
-    assert_eq!(data["target"]["data"]["graph"]["num_vertices"], 5);
     let solved = pred()
         .args([
             "solve",
diff --git a/src/models/misc/longest_common_subsequence.rs b/src/models/misc/longest_common_subsequence.rs
index c1561ca5f..24b0bfdac 100644
--- a/src/models/misc/longest_common_subsequence.rs
+++ b/src/models/misc/longest_common_subsequence.rs
@@ -41,8 +41,6 @@ pub struct LongestCommonSubsequence {
     alphabet_size: usize,
     strings: Vec<Vec<usize>>,
     max_length: usize,
-    #[serde(skip)]
-    anchor_matching_pairs: u64,
 }
 
 #[derive(Deserialize)]
@@ -124,32 +122,10 @@ impl LongestCommonSubsequence {
         {
             return Err("input symbols must be less than alphabet_size".into());
         }
-        let mut anchor_matching_pairs = 0u64;
-        if let Some((anchor, input)) = strings
-            .iter()
-            .enumerate()
-            .min_by_key(|(_, s)| s.len())
-            .filter(|(_, s)| !s.is_empty())
-        {
-            let mut frequencies = std::collections::HashMap::<usize, u64>::new();
-            for &symbol in input {
-                *frequencies.entry(symbol).or_default() += 1;
-            }
-            for (r, string) in strings.iter().enumerate() {
-                if r != anchor {
-                    for symbol in string {
-                        anchor_matching_pairs = anchor_matching_pairs
-                            .checked_add(frequencies.get(symbol).copied().unwrap_or(0))
-                            .ok_or("anchor matching-pair count exceeds u64")?;
-                    }
-                }
-            }
-        }
         Ok(Self {
             alphabet_size,
             strings,
             max_length,
-            anchor_matching_pairs,
         })
     }
 
@@ -191,36 +167,10 @@ impl LongestCommonSubsequence {
             .sum()
     }
 
-    /// Equal-symbol position pairs between the first shortest string and all others.
-    /// Counts the original input strings before a reduction removes redundancy.
-    pub fn anchor_matching_pairs(&self) -> u64 {
-        self.anchor_matching_pairs
-    }
-
     /// Returns the number of adjacent position transitions.
     pub fn num_transitions(&self) -> usize {
         self.max_length.saturating_sub(1)
     }
-
-    /// Returns the cross-frequency product: the sum over each alphabet symbol
-    /// of the product of that symbol's frequency across all input strings.
-    ///
-    /// Formally: Σ_{c ∈ 0..alphabet_size} Π_{i=1..k} count(c, strings\[i\])
-    /// where count(c, s) is the number of occurrences of symbol c in string s.
-    ///
-    /// This statistic describes the legacy match-tuple expansion, not the
-    /// capped hybrid used by the LCS → MaxIS reduction. This uncapped getter
-    /// is not a canonical parameter and can overflow for many repeated strings.
-    pub fn cross_frequency_product(&self) -> usize {
-        (0..self.alphabet_size)
-            .map(|c| {
-                self.strings
-                    .iter()
-                    .map(|s| s.iter().filter(|&&sym| sym == c).count())
-                    .product::<usize>()
-            })
-            .sum()
-    }
 }
 
 /// Check whether `candidate` is a subsequence of `target` using greedy
@@ -248,7 +198,6 @@ impl Problem for LongestCommonSubsequence {
         ("alphabet_size", alphabet_size),
         ("max_length", max_length),
         ("num_strings", num_strings),
-        ("anchor_matching_pairs", anchor_matching_pairs),
         ("num_transitions", num_transitions),
         ("sum_triangular_lengths", sum_triangular_lengths),
         ("total_length", total_length),
diff --git a/src/rules/longestcommonsubsequence_maximumindependentset.rs b/src/rules/longestcommonsubsequence_maximumindependentset.rs
index ad093aab6..0705b3bcd 100644
--- a/src/rules/longestcommonsubsequence_maximumindependentset.rs
+++ b/src/rules/longestcommonsubsequence_maximumindependentset.rs
@@ -1,34 +1,33 @@
-//! Capped match-tuple graph with a polynomial anchored fallback.
+//! Polynomial reduction from LCS to unweighted independent set.
 //!
-//! Remove redundant strings and impossible anchor letters first. Tuple graphs
-//! preserve LCS; anchored optima are L * k + LCS for k retained strings.
-//! Both graphs have at most L * (k + 2) + F vertices, where L is the filtered
-//! anchor length and F counts matches against it. Original input counts bound these.
+//! Use match tuples when they dominate the normalized reward-anchored graph.
+//! The target optimum is LCS for tuples, or h * m + LCS for h slots and m strings.
 
 use crate::models::graph::MaximumIndependentSet;
 use crate::models::misc::{is_subsequence, LongestCommonSubsequence};
 use crate::reduction;
 use crate::rules::traits::{ReduceTo, ReductionResult};
-use crate::topology::SimpleGraph;
+use crate::topology::{Graph, SimpleGraph};
 use crate::types::One;
-use std::collections::{BTreeMap, HashSet};
+use std::collections::{BTreeSet, HashSet};
 use std::ops::Range;
 
+/// Both encodings decode the same way: vertex `i < symbols.len()` selects
+/// `symbols[i]` when every embedding group `i` is nonempty. Tuple vertices,
+/// ordered by anchor slot, have no embedding groups.
 #[derive(Debug, Clone)]
-enum Encoding {
-    Tuples(Vec<(usize, Vec<usize>)>),
-    Anchored {
-        anchor: Vec<usize>,
-        embeddings: Vec<Vec<Range<usize>>>,
-    },
+struct Encoding {
+    symbols: Vec<usize>,
+    // Matching vertices per string and slot; the skip vertex is range.end.
+    embeddings: Vec<Vec<Range<usize>>>,
 }
 
-/// Target graph and the selected mathematical witness mapping.
+/// Target graph and witness mapping for the selected encoding.
 #[derive(Debug, Clone)]
 pub struct ReductionLCSToIS {
     target: MaximumIndependentSet<SimpleGraph, One>,
-    encoding: Encoding,
     max_length: usize,
+    encoding: Encoding,
 }
 
 impl ReductionResult for ReductionLCSToIS {
@@ -49,251 +48,177 @@ impl ReductionResult for ReductionLCSToIS {
             |value| value.0.is_some(),
             "selected vertices do not form an independent set",
         )?;
-        let mut decoded = Vec::with_capacity(self.max_length);
-        match &self.encoding {
-            Encoding::Tuples(nodes) => {
-                let mut selected = nodes
-                    .iter()
-                    .zip(solution)
-                    .filter(|(_, bit)| **bit)
-                    .map(|((symbol, positions), _)| (positions[0], *symbol))
-                    .collect::<Vec<_>>();
-                selected.sort_unstable_by_key(|&(position, _)| position);
-                decoded.extend(selected.into_iter().map(|(_, symbol)| Some(symbol)));
-            }
-            Encoding::Anchored { anchor, embeddings } => {
-                for (p, &symbol) in anchor.iter().enumerate() {
-                    if solution[3 * p] != solution[3 * p + 1] {
-                        return Err(crate::rules::ExtractionError::invalid(
-                            "active anchor twins are incomplete",
-                        ));
-                    }
-                    if solution[3 * p]
-                        && embeddings.iter().all(|groups| {
-                            let group = &groups[p];
-                            solution[group.start..group.end - 1].iter().any(|&bit| bit)
-                        })
-                    {
-                        decoded.push(Some(symbol));
-                    }
+        let Encoding {
+            symbols,
+            embeddings,
+        } = &self.encoding;
+        let mut decoded = symbols
+            .iter()
+            .enumerate()
+            .filter(|&(i, _)| {
+                solution[i]
+                    && embeddings
+                        .iter()
+                        .all(|groups| solution[groups[i].clone()].iter().any(|&bit| bit))
+            })
+            .map(|(_, &symbol)| Some(symbol))
+            .collect::<Vec<_>>();
+        decoded.resize(self.max_length, None);
+        Ok(decoded)
+    }
+}
+
+fn tuple_graph(
+    anchor: &[usize],
+    matches: &[Vec<Vec<usize>>],
+    vertex_cap: usize,
+    edge_cap: usize,
+) -> Option<(SimpleGraph, Encoding)> {
+    let count = (0..anchor.len()).try_fold(0usize, |total, p| {
+        let product = matches.iter().try_fold(1usize, |product, slots| {
+            product
+                .checked_mul(slots[p].len())
+                .filter(|&n| n <= vertex_cap)
+        })?;
+        total.checked_add(product).filter(|&n| n <= vertex_cap)
+    })?;
+    let mut tuples = Vec::with_capacity(count);
+    for p in 0..anchor.len() {
+        let mut product = vec![vec![p]];
+        for slots in matches {
+            product = product
+                .iter()
+                .flat_map(|prefix| {
+                    slots[p].iter().map(|&j| {
+                        let mut tuple = prefix.clone();
+                        tuple.push(j);
+                        tuple
+                    })
+                })
+                .collect();
+        }
+        tuples.extend(product);
+    }
+    let mut edges = Vec::new();
+    for (i, left) in tuples.iter().enumerate() {
+        for (j, right) in tuples.iter().enumerate().skip(i + 1) {
+            let before = left[0] < right[0];
+            if left
+                .iter()
+                .zip(right)
+                .any(|(a, b)| a == b || (a < b) != before)
+            {
+                if edges.len() == edge_cap {
+                    return None;
                 }
+                edges.push((i, j));
             }
         }
-        while decoded.len() < self.max_length {
-            decoded.push(None);
+    }
+    let encoding = Encoding {
+        symbols: tuples.iter().map(|tuple| anchor[tuple[0]]).collect(),
+        embeddings: vec![],
+    };
+    Some((SimpleGraph::new(count, edges), encoding))
+}
+
+fn anchored_graph(anchor: Vec<usize>, matches: &[Vec<Vec<usize>>]) -> (SimpleGraph, Encoding) {
+    let mut edges = Vec::new();
+    let mut cursor = anchor.len();
+    let mut embeddings = Vec::new();
+    for slots in matches {
+        let mut groups = Vec::<Range<usize>>::new();
+        for (p, positions) in slots.iter().enumerate() {
+            let group = cursor..cursor + positions.len();
+            let skip = group.end;
+            cursor = skip + 1;
+            for a in group.start..=skip {
+                edges.extend((a + 1..=skip).map(|b| (a, b)));
+            }
+            edges.push((p, skip));
+            for (earlier, previous) in slots.iter().zip(&groups) {
+                for (i, &position) in earlier.iter().enumerate() {
+                    let conflicts = positions.partition_point(|&j| j <= position);
+                    edges.extend((0..conflicts).map(|j| (previous.start + i, group.start + j)));
+                }
+            }
+            groups.push(group);
         }
-        Ok(decoded)
+        embeddings.push(groups);
     }
+    (
+        SimpleGraph::new(cursor, edges),
+        Encoding {
+            symbols: anchor,
+            embeddings,
+        },
+    )
 }
 
 #[reduction(transform = upper_bound {
-    num_vertices = "max_length * (num_strings + 2) + anchor_matching_pairs",
-    num_edges = "(max_length * (num_strings + 2) + anchor_matching_pairs)^2",
+    num_vertices = "max_length * (num_strings + total_length - max_length)",
+    num_edges = "max_length * (max_length + 1) / 2 * (sum_triangular_lengths - max_length * (max_length + 1) / 2) + max_length * (num_strings - 1)",
 })]
 impl ReduceTo<MaximumIndependentSet<SimpleGraph, One>> for LongestCommonSubsequence {
     type Result = ReductionLCSToIS;
 
     fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
-        if self.max_length() == 0 {
-            return Ok(ReductionLCSToIS {
-                target: MaximumIndependentSet::new(SimpleGraph::new(0, vec![]), vec![]),
-                encoding: Encoding::Tuples(vec![]),
-                max_length: 0,
-            });
-        }
-        let overflow = || {
-            crate::rules::ReductionError::integer_overflow::<
-                Self,
-                MaximumIndependentSet<SimpleGraph, One>,
-            >("counting anchored vertices")
-        };
         let anchor = self
             .strings()
             .iter()
             .min_by_key(|s| s.len())
-            .map(Vec::as_slice)
-            .unwrap_or_default();
-        let mut seen = HashSet::new();
-        let retained = std::iter::once(anchor)
-            .chain(
-                self.strings()
-                    .iter()
-                    .map(Vec::as_slice)
-                    .filter(|string| !is_subsequence(anchor, string) && seen.insert(*string)),
-            )
+            .into_iter()
+            .flatten()
+            .copied()
+            .filter(|symbol| self.strings().iter().all(|s| s.contains(symbol)))
             .collect::<Vec<_>>();
-        let positions = retained
+        let symbols = anchor.iter().copied().collect::<HashSet<_>>();
+        let strings = self
+            .strings()
             .iter()
-            .map(|string| {
-                let mut map = BTreeMap::<usize, Vec<usize>>::new();
-                for (j, &symbol) in string.iter().enumerate() {
-                    map.entry(symbol).or_default().push(j);
-                }
-                map
+            .map(|s| {
+                s.iter()
+                    .copied()
+                    .filter(|c| symbols.contains(c))
+                    .collect::<Vec<_>>()
             })
-            .collect::<Vec<_>>();
-        let common_symbols = positions[0]
-            .keys()
-            .copied()
-            .filter(|symbol| positions.iter().all(|map| map.contains_key(symbol)))
-            .collect::<HashSet<_>>();
-        let anchor = anchor
+            .filter(|string| !is_subsequence(&anchor, string))
+            .collect::<BTreeSet<_>>();
+        let matches = strings
             .iter()
-            .copied()
-            .filter(|symbol| common_symbols.contains(symbol))
-            .collect::<Vec<_>>();
-        let positions = positions
-            .into_iter()
-            .zip(retained)
-            .enumerate()
-            .filter(|(r, (_, string))| *r == 0 || !is_subsequence(&anchor, string))
-            .map(|(_, (map, _))| map)
-            .collect::<Vec<_>>();
-
-        // Only nonempty position lists enter the product; a later absent symbol
-        // must contribute zero before any multiplication can exceed the cap.
-        let common = positions[0]
-            .keys()
-            // Removing a constraint must not reintroduce an impossible letter.
-            .filter(|symbol| common_symbols.contains(symbol))
-            .filter_map(|&symbol| {
-                let lists = positions
+            .map(|s| {
+                anchor
                     .iter()
-                    .map(|map| map.get(&symbol).map(Vec::as_slice))
-                    .collect::<Option<Vec<_>>>()?;
-                Some((symbol, lists))
+                    .map(|symbol| {
+                        (0..s.len())
+                            .filter(|&j| s[j] == *symbol)
+                            .collect::<Vec<_>>()
+                    })
+                    .collect::<Vec<_>>()
             })
             .collect::<Vec<_>>();
-        let mut cap = anchor.len().checked_mul(3).ok_or_else(overflow)?;
-        for map in &positions[1..] {
-            for symbol in &anchor {
-                cap = cap
-                    .checked_add(map.get(symbol).map_or(0, Vec::len))
-                    .and_then(|count| count.checked_add(1))
-                    .ok_or_else(overflow)?;
-            }
-        }
-        let tuple_count = common.iter().try_fold(0usize, |total, (_, lists)| {
-            let product = lists.iter().try_fold(1usize, |product, list| {
-                product
-                    .checked_mul(list.len())
-                    .filter(|&count| count <= cap)
-            })?;
-            total.checked_add(product).filter(|&count| count <= cap)
-        });
-        let mut num_vertices = tuple_count.unwrap_or(cap);
+        let anchored = anchored_graph(anchor.clone(), &matches);
         <Self as ReduceTo<MaximumIndependentSet<SimpleGraph, One>>>::exact_i64(
-            num_vertices,
+            anchored.0.num_vertices(),
             "representing the independent-set objective",
         )?;
-        let mut edges = Vec::new();
-        let mut encoding = if tuple_count.is_some() {
-            let mut nodes = Vec::with_capacity(num_vertices);
-            for (symbol, lists) in common {
-                let mut tuples = vec![Vec::new()];
-                for list in lists {
-                    tuples = tuples
-                        .into_iter()
-                        .flat_map(|prefix| {
-                            list.iter().map(move |&position| {
-                                let mut tuple = prefix.clone();
-                                tuple.push(position);
-                                tuple
-                            })
-                        })
-                        .collect();
-                }
-                nodes.extend(tuples.into_iter().map(|tuple| (symbol, tuple)));
-            }
-            for (i, (_, left)) in nodes.iter().enumerate() {
-                for (j, (_, right)) in nodes.iter().enumerate().skip(i + 1) {
-                    if !left.iter().zip(right).all(|(a, b)| a < b)
-                        && !left.iter().zip(right).all(|(a, b)| a > b)
-                    {
-                        edges.push((i, j));
-                    }
-                }
-            }
-            Encoding::Tuples(nodes)
-        } else {
-            let (anchor_edges, anchor_encoding) = anchored_graph(&anchor, &positions, cap)?;
-            edges = anchor_edges;
-            anchor_encoding
-        };
-        // A tuple graph costing at most the anchor's vertices alone cannot lose.
-        if tuple_count.is_some() && edges.len() > cap - num_vertices {
-            let (anchor_edges, anchor_encoding) = anchored_graph(&anchor, &positions, cap)?;
-            if edges.len() > anchor_edges.len()
-                && edges.len() - anchor_edges.len() > cap - num_vertices
-            {
-                num_vertices = cap;
-                edges = anchor_edges;
-                encoding = anchor_encoding;
-            }
-        }
-        let target = MaximumIndependentSet::new(
-            SimpleGraph::new(num_vertices, edges),
-            vec![One; num_vertices],
-        );
+        let (graph, encoding) = tuple_graph(
+            &anchor,
+            &matches,
+            anchored.0.num_vertices(),
+            anchored.0.num_edges(),
+        )
+        .unwrap_or(anchored);
+        let weights = vec![One; graph.num_vertices()];
+        let target = MaximumIndependentSet::new(graph, weights);
         Ok(ReductionLCSToIS {
             target,
-            encoding,
             max_length: self.max_length(),
+            encoding,
         })
     }
 }
 
-fn anchored_graph(
-    anchor: &[usize],
-    positions: &[BTreeMap<usize, Vec<usize>>],
-    cap: usize,
-) -> Result<(Vec<(usize, usize)>, Encoding), crate::rules::ReductionError> {
-    <LongestCommonSubsequence as ReduceTo<MaximumIndependentSet<SimpleGraph, One>>>::exact_i64(
-        cap,
-        "representing the anchored independent-set objective",
-    )?;
-    let mut edges = Vec::new();
-    let mut cursor = anchor.len() * 3;
-    let mut embeddings = Vec::with_capacity(positions.len() - 1);
-    for p in 0..anchor.len() {
-        edges.extend([(3 * p, 3 * p + 2), (3 * p + 1, 3 * p + 2)]);
-    }
-    for map in &positions[1..] {
-        let mut groups = Vec::<(&[usize], Range<usize>)>::with_capacity(anchor.len());
-        for (p, symbol) in anchor.iter().enumerate() {
-            let matches = map.get(symbol).map(Vec::as_slice).unwrap_or_default();
-            let group = cursor..cursor + matches.len() + 1;
-            cursor = group.end;
-            for a in group.clone() {
-                for b in a + 1..group.end {
-                    edges.push((a, b));
-                }
-            }
-            let skip = group.end - 1;
-            edges.extend([(3 * p, skip), (3 * p + 1, skip)]);
-            edges.extend((group.start..skip).map(|j| (3 * p + 2, j)));
-            // Only this string's earlier slots can cross. Sorted matches let
-            // us emit exactly the conflicting prefix of each group.
-            for (earlier, previous) in &groups {
-                for (i, &position) in earlier.iter().enumerate() {
-                    let conflicts = matches.partition_point(|&j| j <= position);
-                    edges.extend((0..conflicts).map(|j| (previous.start + i, group.start + j)));
-                }
-            }
-            groups.push((matches, group));
-        }
-        embeddings.push(groups.into_iter().map(|(_, range)| range).collect());
-    }
-    debug_assert_eq!(cursor, cap);
-    Ok((
-        edges,
-        Encoding::Anchored {
-            anchor: anchor.to_vec(),
-            embeddings,
-        },
-    ))
-}
-
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
     use crate::export::SolutionPair;
@@ -301,15 +226,15 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "longestcommonsubsequence_to_maximumindependentset",
         build: || {
-            let source = LongestCommonSubsequence::new(3, vec![vec![0, 1, 0, 2], vec![1, 0, 2, 0]]);
+            let source = LongestCommonSubsequence::new(2, vec![vec![0, 1], vec![1, 0]]);
             crate::example_db::specs::rule_example_with_witness::<
                 _,
                 MaximumIndependentSet<SimpleGraph, One>,
             >(
                 source,
                 SolutionPair {
-                    source_config: serde_json::json!(vec![Some(1), Some(0), Some(2), None]),
-                    target_config: serde_json::json!(vec![false, false, true, false, true, true]),
+                    source_config: serde_json::json!(vec![Some(0), None]),
+                    target_config: serde_json::json!(vec![true, false]),
                 },
             )
         },
diff --git a/src/rules/minimumvertexcover_longestcommonsubsequence.rs b/src/rules/minimumvertexcover_longestcommonsubsequence.rs
index 644fbd5df..fa54c9539 100644
--- a/src/rules/minimumvertexcover_longestcommonsubsequence.rs
+++ b/src/rules/minimumvertexcover_longestcommonsubsequence.rs
@@ -42,7 +42,6 @@ impl ReductionResult for ReductionVCToLCS {
     transform = {
         exact {
             alphabet_size = "num_vertices",
-            anchor_matching_pairs = "2 * num_edges * (num_vertices - 1)",
             num_strings = "num_edges + 1",
             max_length = "num_vertices",
             total_length = "num_vertices + 2 * num_edges * num_vertices - 2 * num_edges",
diff --git a/src/unit_tests/models/misc/longest_common_subsequence.rs b/src/unit_tests/models/misc/longest_common_subsequence.rs
index 0b3bc935f..ac7665979 100644
--- a/src/unit_tests/models/misc/longest_common_subsequence.rs
+++ b/src/unit_tests/models/misc/longest_common_subsequence.rs
@@ -4,32 +4,6 @@ use crate::solvers::BruteForceProblem as _;
 use crate::traits::Problem;
 use crate::types::Max;
 
-#[test]
-fn test_lcs_anchor_matching_pairs_uses_first_shortest_string() {
-    let source =
-        LongestCommonSubsequence::new(2, vec![vec![0, 0, 1], vec![0, 1, 1], vec![0, 0, 0, 1]]);
-    assert_eq!(source.parameters().get("anchor_matching_pairs"), Some(11));
-    let reordered =
-        LongestCommonSubsequence::new(2, vec![vec![0, 1, 1], vec![0, 0, 1], vec![0, 0, 0, 1]]);
-    assert_eq!(reordered.parameters().get("anchor_matching_pairs"), Some(9));
-    let restored: LongestCommonSubsequence =
-        serde_json::from_value(serde_json::to_value(&source).unwrap()).unwrap();
-    assert_eq!(restored.parameters(), source.parameters());
-    for strings in [
-        vec![],
-        vec![vec![]],
-        vec![vec![0]],
-        vec![vec![], vec![0, 1]],
-    ] {
-        assert_eq!(
-            LongestCommonSubsequence::new(2, strings)
-                .parameters()
-                .get("anchor_matching_pairs"),
-            Some(0)
-        );
-    }
-}
-
 fn issue_yes_instance() -> LongestCommonSubsequence {
     LongestCommonSubsequence::new(
         2,
diff --git a/src/unit_tests/rules/longestcommonsubsequence_maximumindependentset.rs b/src/unit_tests/rules/longestcommonsubsequence_maximumindependentset.rs
index 98012e1c8..0ded1991d 100644
--- a/src/unit_tests/rules/longestcommonsubsequence_maximumindependentset.rs
+++ b/src/unit_tests/rules/longestcommonsubsequence_maximumindependentset.rs
@@ -1,263 +1,254 @@
 use super::*;
+use crate::rules::test_helpers::{
+    assert_optimization_round_trip_from_optimization_target, assert_parameter_predictions,
+};
 use crate::solvers::{BruteForce, ILPSolver};
 use crate::traits::Problem;
 use crate::types::Max;
 
-fn assert_round_trip(source: &LongestCommonSubsequence, length: i64, target_value: i64) {
+fn reduce(source: &LongestCommonSubsequence) -> ReductionLCSToIS {
+    let reduction = ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(source).unwrap();
+    assert_parameter_predictions(source, &reduction);
+    reduction
+}
+
+fn assert_round_trip(source: &LongestCommonSubsequence, length: i64) {
     let source_solution = BruteForce::new().solve(source).unwrap().unwrap();
     assert_eq!(
         source.evaluate(&source_solution).unwrap(),
         Max(Some(length))
     );
-    let reduction = ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(source).unwrap();
+    let reduction = reduce(source);
     let target = reduction.target_problem();
-    let solution = if target.num_vertices() <= 12 {
-        BruteForce::new().solve(target).unwrap().unwrap()
-    } else {
-        ILPSolver::new().solve(target).unwrap()
-    };
-    assert_eq!(target.evaluate(&solution).unwrap(), Max(Some(target_value)));
+    // Brute force over every optimal target witness stays fast up to 13 vertices.
+    if target.num_vertices() <= 13 {
+        assert_optimization_round_trip_from_optimization_target(source, &reduction, "LCS to MIS");
+    }
+    let solution = ILPSolver::new().solve(target).unwrap();
     let decoded = reduction.extract_solution(&solution).unwrap();
     assert_eq!(source.evaluate(&decoded).unwrap(), Max(Some(length)));
 }
 
-#[test]
-fn test_longestcommonsubsequence_to_maximumindependentset_closed_loop() {
-    let source = LongestCommonSubsequence::new(3, vec![vec![0, 1, 0, 2], vec![1, 0, 2, 0]]);
-    let reduction =
-        ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&source).unwrap();
-    // Four A alignments, one B alignment, and one C alignment.
-    assert_eq!(reduction.target_problem().num_vertices(), 6);
-    assert_round_trip(&source, 3, 3);
+fn repetition_pair() -> LongestCommonSubsequence {
+    LongestCommonSubsequence::new(2, vec![vec![0, 1], vec![1, 0, 0], vec![1, 0, 0, 0]])
+}
+
+fn opposite_pair() -> LongestCommonSubsequence {
+    LongestCommonSubsequence::new(2, vec![vec![0, 1], vec![1, 0]])
 }
 
 #[test]
-fn test_lcs_to_mis_removes_redundant_strings() {
-    let repeated = LongestCommonSubsequence::new(1, vec![vec![0, 0]; 64]);
-    let reduction =
-        ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&repeated).unwrap();
+fn test_longestcommonsubsequence_to_maximumindependentset_closed_loop() {
+    let source = opposite_pair();
+    assert_round_trip(&source, 1);
+    let reduction = reduce(&source);
     assert_eq!(reduction.target_problem().num_vertices(), 2);
-    assert_eq!(reduction.target_problem().num_edges(), 0);
-    assert_round_trip(&repeated, 2, 2);
+    assert_eq!(reduction.target_problem().num_edges(), 1);
+    let witness = vec![true, false];
+    assert_eq!(
+        reduction.target_problem().evaluate(&witness).unwrap(),
+        Max(Some(1))
+    );
+    assert_eq!(
+        reduction.extract_solution(&witness).unwrap(),
+        vec![Some(0), None]
+    );
+}
 
+#[test]
+fn test_lcs_to_mis_filters_before_deduplicating_tuple_inputs() {
     let source = LongestCommonSubsequence::new(
-        3,
-        vec![vec![2, 0, 1, 2], vec![0, 1], vec![0, 1], vec![1, 0]],
+        4,
+        vec![vec![0, 1], vec![1, 2, 0], vec![1, 3, 0], vec![1, 0]],
     );
-    let reduction =
-        ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&source).unwrap();
+    let reduction = reduce(&source);
     assert_eq!(reduction.target_problem().num_vertices(), 2);
     assert_eq!(reduction.target_problem().num_edges(), 1);
-    assert_eq!(source.parameters().get("anchor_matching_pairs"), Some(6));
-    assert_round_trip(&source, 1, 1);
-}
-
-fn crossing_strings(longer: usize) -> LongestCommonSubsequence {
-    let blocks = |count| [vec![1; count], vec![0; count]].concat();
-    LongestCommonSubsequence::new(2, vec![vec![0, 1], blocks(3), blocks(longer)])
+    assert_round_trip(&source, 1);
 }
 
 #[test]
-fn test_lcs_to_mis_caps_tuple_expansion_before_allocation() {
-    // At the 24-vertex cap, the tuple graph is a clique (276 edges).
-    // The anchored graph has the same vertices and only 83 edges.
-    let at_cap = crossing_strings(4);
-    let reduction =
-        ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&at_cap).unwrap();
-    assert_eq!(reduction.target_problem().num_vertices(), 24);
-    assert_eq!(reduction.target_problem().num_edges(), 83);
-    assert_round_trip(&at_cap, 1, 7);
-
-    // 30 tuples exceed the cap: 6 anchor vertices + (6+2)+(10+2) embeddings.
-    let source = crossing_strings(5);
-    let reduction =
-        ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&source).unwrap();
-    assert_eq!(reduction.target_problem().num_vertices(), 26);
-    assert_round_trip(&source, 1, 7);
-
-    // Sixty-four distinct balanced binary strings would have 2*4^64 tuples.
-    let strings = (0u8..=u8::MAX)
-        .filter(|bits| bits.count_ones() == 4)
-        .take(64)
-        .map(|bits| (0..8).map(|p| usize::from((bits >> p) & 1)).collect())
-        .collect();
-    let source = LongestCommonSubsequence::new(2, strings);
-    let reduction =
-        ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&source).unwrap();
-    assert_eq!(reduction.target_problem().num_vertices(), 2544);
-    assert_eq!(source.parameters().get("anchor_matching_pairs"), Some(2016));
-}
-
-#[test]
-fn test_lcs_to_mis_polynomial_parameter_bound() {
-    let source = crossing_strings(5);
-    let graph = crate::rules::ReductionGraph::new();
-    let entry = graph
-        .find_entry(
-            "LongestCommonSubsequence",
-            &crate::export::variant_to_map(LongestCommonSubsequence::variant()),
-            "MaximumIndependentSet",
-            &crate::export::variant_to_map(MaximumIndependentSet::<SimpleGraph, One>::variant()),
-        )
-        .unwrap();
-    let transform = entry
-        .parameter_contract
-        .as_ref()
-        .unwrap()
-        .transform()
-        .unwrap();
-    let predicted = transform.evaluate(&source.parameters()).unwrap();
-    assert_eq!(predicted.get("num_vertices"), Some(26));
-    assert_eq!(predicted.get("num_edges"), Some(676));
-    let reduction =
-        ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&source).unwrap();
-    assert!(u64::try_from(reduction.target_problem().num_edges()).unwrap() <= 676);
+fn test_lcs_to_mis_uses_tuples_for_the_repeated_symbol_example() {
+    let source = LongestCommonSubsequence::new(3, vec![vec![0, 1, 0, 2], vec![1, 0, 2, 0]]);
+    let reduction = reduce(&source);
+    assert_eq!(reduction.target_problem().num_vertices(), 6);
+    assert_eq!(reduction.target_problem().num_edges(), 9);
+    assert_round_trip(&source, 3);
 }
 
 #[test]
-fn test_lcs_to_mis_selects_by_vertices_and_edges() {
-    // There are 24 zero-tuples (3*2*2*2), but almost every pair conflicts.
-    // The 36-vertex anchored graph is smaller when its 96 edges are included.
-    let source = LongestCommonSubsequence::new(
-        2,
-        vec![vec![0, 0, 0], vec![0, 0, 1], vec![0, 1, 0], vec![1, 0, 0]],
-    );
-    let reduction =
-        ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&source).unwrap();
-    assert_eq!(reduction.target_problem().num_vertices(), 36);
-    assert_eq!(reduction.target_problem().num_edges(), 96);
-    assert_round_trip(&source, 2, 14);
-
-    // Both constructions cost 133 vertices plus edges; keep the tuple graph.
-    let source = LongestCommonSubsequence::new(
-        2,
-        vec![vec![0, 0, 0, 1], vec![0, 1, 0, 1], vec![1, 1, 0, 0]],
+fn test_lcs_to_mis_normalization_preserves_original_padding() {
+    let source = LongestCommonSubsequence::new(2, vec![vec![0, 1], vec![0; 3], vec![0; 2]]);
+    let reduction = reduce(&source);
+    assert_eq!(reduction.target_problem().num_vertices(), 1);
+    assert_eq!(reduction.target_problem().num_edges(), 0);
+    assert_eq!(
+        reduction.extract_solution(&vec![true]).unwrap(),
+        vec![Some(0), None]
     );
-    let reduction =
-        ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&source).unwrap();
-    assert_eq!(reduction.target_problem().num_vertices(), 16);
-    assert_eq!(reduction.target_problem().num_edges(), 117);
-    assert_round_trip(&source, 2, 2);
+    assert_round_trip(&source, 1);
 }
 
 #[test]
-fn test_lcs_to_mis_removes_impossible_anchor_letters() {
-    let source = LongestCommonSubsequence::new(
-        3,
-        vec![
-            vec![0, 0, 1, 2],
-            [vec![1; 3], vec![0; 5]].concat(),
-            [vec![1; 4], vec![0; 6]].concat(),
-        ],
-    );
-    // Only 001 remains in the anchor: 9 anchor vertices + 29 matches + 6 skips.
-    // Anchor edges 6, embedding cliques 88, consistency 41, crossings 114.
-    let reduction =
-        ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&source).unwrap();
-    assert_eq!(reduction.target_problem().num_vertices(), 44);
-    assert_eq!(reduction.target_problem().num_edges(), 249);
-    assert_round_trip(&source, 2, 11);
-
-    // After removing the absent 1, both other strings contain the whole anchor.
-    let source = LongestCommonSubsequence::new(2, vec![vec![0, 0, 1], vec![0; 5], vec![0; 6]]);
-    let reduction =
-        ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&source).unwrap();
+fn test_lcs_to_mis_polynomial_size_for_many_repeated_strings() {
+    // Containing strings add no constraints, even when there would be 2^64 tuples.
+    let source = LongestCommonSubsequence::new(1, vec![vec![0, 0]; 64]);
+    let reduction = reduce(&source);
     assert_eq!(reduction.target_problem().num_vertices(), 2);
     assert_eq!(reduction.target_problem().num_edges(), 0);
-    assert_round_trip(&source, 2, 2);
+    assert_round_trip(&source, 2);
+    let entry = crate::rules::registry::reduction_entries()
+        .into_iter()
+        .find(|entry| {
+            entry.source_name == LongestCommonSubsequence::NAME
+                && entry.target_name == "MaximumIndependentSet"
+        })
+        .unwrap();
+    assert!(entry.reduce_aggregate_fn.is_none());
+    let contract = entry.parameter_contract().unwrap();
+    let predicted = contract
+        .transform()
+        .unwrap()
+        .evaluate(&source.parameters())
+        .unwrap();
+    // A=3, S-A=63*3: embedding cliques/crossings <= 567, reward links <= 126.
+    assert_eq!(predicted.get("num_vertices"), Some(380));
+    assert_eq!(predicted.get("num_edges"), Some(693));
 }
 
 #[test]
-fn test_lcs_to_mis_ordering_and_empty_common_subsequences() {
+fn test_lcs_to_mis_ordering_repetition_and_empty_common_subsequences() {
     for (alphabet, strings, length) in [
         (2, vec![vec![0, 1, 0], vec![1, 0, 1], vec![0, 1, 1]], 2),
         (2, vec![vec![0, 1], vec![1, 0], vec![0, 1], vec![1, 0]], 1),
+        (
+            3,
+            vec![vec![2, 0, 1, 2], vec![0, 1], vec![0, 1], vec![1, 0]],
+            1,
+        ),
+        (2, vec![vec![0, 0, 1], vec![0; 5], vec![0; 6]], 2),
+        (2, vec![vec![0, 1, 0], vec![0, 0, 1]], 2),
         (2, vec![vec![0, 1, 0]], 3),
-        (2, vec![vec![0, 0], vec![1, 1]], 0),
+        (2, vec![vec![0], vec![1]], 0),
         (2, vec![vec![0, 1], vec![]], 0),
+        (0, vec![vec![], vec![]], 0),
         (0, vec![], 0),
     ] {
-        assert_round_trip(
-            &LongestCommonSubsequence::new(alphabet, strings),
-            length,
-            length,
-        );
+        assert_round_trip(&LongestCommonSubsequence::new(alphabet, strings), length);
     }
 }
 
 #[test]
-fn test_lcs_to_mis_rejects_invalid_and_partial_twin_witnesses() {
-    let source = crossing_strings(5);
-    let reduction =
-        ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&source).unwrap();
-    let target = reduction.target_problem();
-    assert!(reduction
-        .extract_solution(&vec![false; target.num_vertices() - 1])
-        .is_err());
-    assert!(reduction
-        .extract_solution(&vec![true; target.num_vertices()])
-        .is_err());
-    let mut partial = vec![false; target.num_vertices()];
-    partial[0] = true;
-    assert_eq!(target.evaluate(&partial).unwrap(), Max(Some(1)));
-    assert!(reduction.extract_solution(&partial).is_err());
+fn test_lcs_to_mis_rejects_malformed_witnesses() {
+    for source in [opposite_pair(), repetition_pair()] {
+        let reduction = reduce(&source);
+        let n = reduction.target_problem().num_vertices();
+        for witness in [vec![false; n - 1], vec![false; n + 1], vec![true; n]] {
+            assert!(reduction.extract_solution(&witness).is_err());
+        }
+    }
 }
 
 #[test]
-fn test_lcs_to_mis_decodes_missing_embedding_groups() {
-    let source = crossing_strings(5);
-    let reduction =
-        ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&source).unwrap();
-    let mut solution = vec![false; reduction.target_problem().num_vertices()];
-    solution[..2].fill(true);
+fn test_lcs_to_mis_keeps_anchored_when_tuples_have_more_edges() {
+    let source = repetition_pair();
+    let reduction = reduce(&source);
+    // Seven tuples have 21 edges; the anchored graph has 13 vertices but only 20 edges.
+    assert_eq!(reduction.target_problem().num_vertices(), 13);
+    assert_eq!(reduction.target_problem().num_edges(), 20);
+    assert_round_trip(&source, 1);
+}
+
+#[test]
+fn test_lcs_to_mis_caps_many_string_tuple_products() {
+    let mut strings = vec![vec![0, 1]];
+    strings.extend((1..=64).map(|n| {
+        let mut string = vec![0; n + 1];
+        string[0] = 1;
+        string
+    }));
+    let source = LongestCommonSubsequence::new(2, strings);
+    let reduction = reduce(&source);
+    // Tuple count 64! + 1 exceeds usize; the anchored graph stays polynomial.
+    assert_eq!(reduction.target_problem().num_vertices(), 2274);
+    assert_eq!(reduction.target_problem().num_edges(), 48032);
+    let mut witness = vec![false; 2274];
+    // Embed symbol 1 everywhere, and use the skip in each symbol-0 group.
+    witness[1] = true;
+    let mut cursor = 2;
+    for n in 1..=64 {
+        witness[cursor + n] = true;
+        witness[cursor + n + 1] = true;
+        cursor += n + 3;
+    }
     assert_eq!(
-        reduction.target_problem().evaluate(&solution).unwrap(),
-        Max(Some(2))
+        reduction.target_problem().evaluate(&witness).unwrap(),
+        Max(Some(129))
     );
-    let decoded = reduction.extract_solution(&solution).unwrap();
-    assert_eq!(decoded, vec![None, None]);
-    assert_eq!(source.evaluate(&decoded).unwrap(), Max(Some(0)));
+    assert_eq!(
+        reduction.extract_solution(&witness).unwrap(),
+        vec![Some(1), None]
+    );
+}
+
+#[test]
+fn test_lcs_to_mis_tuple_cap_includes_the_boundary() {
+    let matches = vec![vec![vec![1], vec![0]]];
+    assert!(tuple_graph(&[0, 1], &matches, 2, 1).is_some());
+    assert!(tuple_graph(&[0, 1], &matches, 1, 1).is_none());
+    assert!(tuple_graph(&[0, 1], &matches, 2, 0).is_none());
+}
 
+#[test]
+fn test_lcs_to_mis_rejects_reused_positions_in_nonadjacent_slots() {
     let source = LongestCommonSubsequence::new(
-        3,
+        2,
         vec![
-            vec![0, 0, 0, 0, 0, 0, 1, 2],
-            vec![1, 0, 0, 0, 0, 0, 0, 2],
-            vec![2, 0, 0, 0, 0, 0, 0, 1],
+            vec![0, 1, 0],
+            vec![0, 0, 1],
+            vec![0, 0, 0, 1],
+            vec![1, 0, 0],
         ],
     );
-    let reduction =
-        ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&source).unwrap();
-    assert_eq!(reduction.target_problem().num_vertices(), 116);
-    // Activate seven anchor slots but omit the first string's embedding of 1.
-    // Six zeros still embed in both strings, giving an optimal 30-vertex set.
-    let mut solution = vec![false; 116];
-    for p in 0..7 {
-        solution[3 * p..3 * p + 2].fill(true);
-    }
-    for p in 0..6 {
-        solution[24 + 8 * p] = true;
-        solution[70 + 8 * p] = true;
-    }
-    for vertex in [23, 69, 112, 115] {
-        solution[vertex] = true;
-    }
+    let reduction = reduce(&source);
+    let mut witness = vec![false; reduction.target_problem().num_vertices()];
+    // First and third slots both use position zero of [0,0,0,1].
+    witness[3] = true;
+    witness[9] = true;
     assert_eq!(
-        reduction.target_problem().evaluate(&solution).unwrap(),
-        Max(Some(30))
+        reduction.target_problem().evaluate(&witness).unwrap(),
+        Max(None)
+    );
+    assert!(reduction.extract_solution(&witness).is_err());
+}
+
+#[test]
+fn test_lcs_to_mis_decodes_missing_embedding_groups() {
+    let reduction = reduce(&repetition_pair());
+    let mut witness = vec![false; 13];
+    witness[0] = true;
+    assert_eq!(
+        reduction.extract_solution(&witness).unwrap(),
+        vec![None, None]
     );
+    // Both rewards active; only slot 0 has matches in both strings. Two groups are empty.
+    witness[1] = true;
+    witness[2] = true;
+    witness[7] = true;
     assert_eq!(
-        reduction.extract_solution(&solution).unwrap(),
-        [vec![Some(0); 6], vec![None; 2]].concat()
+        reduction.target_problem().evaluate(&witness).unwrap(),
+        Max(Some(4))
+    );
+    assert_eq!(
+        reduction.extract_solution(&witness).unwrap(),
+        vec![Some(0), None]
     );
-    assert_round_trip(&source, 6, 30);
 }
 
 #[test]
 fn test_lcs_to_mis_preserves_sparse_original_symbols() {
     let source = LongestCommonSubsequence::new(usize::MAX, vec![vec![usize::MAX - 1]]);
-    let reduction =
-        ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&source).unwrap();
+    let reduction = reduce(&source);
     assert_eq!(reduction.target_problem().num_vertices(), 1);
     let solution = BruteForce::new()
         .solve(reduction.target_problem())