diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ
index 8a726f8ec..c4f0cd36b 100644
--- a/docs/paper/reductions.typ
+++ b/docs/paper/reductions.typ
@@ -119,6 +119,7 @@
   "MinimumTardinessSequencing": [Minimum Tardiness Sequencing],
   "SequencingWithinIntervals": [Sequencing Within Intervals],
   "DirectedTwoCommodityIntegralFlow": [Directed Two-Commodity Integral Flow],
+  "StringToStringCorrection": [String-to-String Correction],
 )
 
 // Definition label: "def:<ProblemName>" — each definition block must have a matching label
@@ -2260,6 +2261,72 @@ NP-completeness was established by Garey, Johnson, and Stockmeyer @gareyJohnsonS
   ]
 }
 
+#{
+  let x = load-model-example("StringToStringCorrection")
+  let source = x.instance.source
+  let target = x.instance.target
+  let alpha-size = x.instance.alphabet_size
+  let bound-k = x.instance.bound
+  let n = source.len()
+  // Alphabet mapping: 0->a, 1->b, 2->c, 3->d
+  let alpha-map = range(alpha-size).map(i => str.from-unicode(97 + i))
+  let fmt-str(s) = s.map(c => alpha-map.at(c)).join("")
+  let src-str = fmt-str(source)
+  let tgt-str = fmt-str(target)
+  // Use solution [8, 5]: swap(2,3) then delete(5)
+  let sol = x.optimal.at(1)
+  // Trace the operations
+  let after-swap = (source.at(0), source.at(1), source.at(3), source.at(2), source.at(4), source.at(5))
+  let after-swap-str = after-swap.map(c => alpha-map.at(c)).join("")
+  [
+    #problem-def("StringToStringCorrection")[
+      Given a finite alphabet $Sigma$, a source string $x in Sigma^*$, a target string $y in Sigma^*$, and a positive integer $K$, determine whether $y$ can be derived from $x$ by a sequence of at most $K$ operations, where each operation is either a _single-symbol deletion_ (remove one character at a chosen position) or an _adjacent-symbol interchange_ (swap two neighboring characters).
+    ][
+      A classical NP-complete problem listed as SR20 in Garey and Johnson @garey1979. #cite(<wagner1975>, form: "prose") proved NP-completeness via transformation from Set Covering. The standard edit distance problem --- allowing insertion, deletion, and substitution --- is solvable in $O(|x| dot |y|)$ time by the Wagner--Fischer dynamic programming algorithm @wagner1974. However, restricting the operation set to only deletions and adjacent swaps makes the problem NP-complete for unbounded alphabets. When only adjacent swaps are allowed (no deletions), the problem reduces to counting inversions and is polynomial @wagner1975.#footnote[No algorithm improving on brute-force is known for the general swap-and-delete variant.]
+
+      *Example.* Let $Sigma = {#alpha-map.join(", ")}$, source $x = #src-str$ (length #n), target $y = #tgt-str$ (length #target.len()), and $K = #bound-k$.
+
+      #figure({
+        let blue = graph-colors.at(0)
+        let red = rgb("#e15759")
+        let cell(ch, highlight: false, strike: false) = {
+          let fill = if highlight { blue.transparentize(70%) } else { white }
+          box(width: 0.55cm, height: 0.55cm, fill: fill, stroke: 0.5pt + luma(120),
+            align(center + horizon, text(9pt, weight: "bold",
+              if strike { text(fill: red, [#sym.times]) } else { ch })))
+        }
+        align(center, stack(dir: ttb, spacing: 0.5cm,
+          // Step 0: source
+          stack(dir: ltr, spacing: 0pt,
+            box(width: 2.2cm, height: 0.5cm, align(right + horizon, text(8pt)[$x: quad$])),
+            ..source.map(c => cell(alpha-map.at(c))),
+          ),
+          // Step 1: after swap at positions 2,3
+          stack(dir: ltr, spacing: 0pt,
+            box(width: 2.2cm, height: 0.5cm, align(right + horizon, text(8pt)[swap$(2,3)$: quad])),
+            ..range(after-swap.len()).map(i => cell(alpha-map.at(after-swap.at(i)), highlight: after-swap.at(i) != source.at(i))),
+          ),
+          // Step 2: after delete at position 5
+          stack(dir: ltr, spacing: 0pt,
+            box(width: 2.2cm, height: 0.5cm, align(right + horizon, text(8pt)[del$(5)$: quad])),
+            ..target.map(c => cell(alpha-map.at(c))),
+            cell([], strike: true),
+          ),
+          // Result
+          stack(dir: ltr, spacing: 0pt,
+            box(width: 2.2cm, height: 0.5cm, align(right + horizon, text(8pt)[$= y$: quad])),
+            ..target.map(c => cell(alpha-map.at(c), highlight: true)),
+          ),
+        ))
+      },
+      caption: [String-to-String Correction: transforming $x = #src-str$ into $y = #tgt-str$ with $K = #bound-k$ operations. Step 1 swaps adjacent symbols at positions 2 and 3; step 2 deletes the symbol at position 5.],
+      ) <fig:stsc>
+
+      The transformation uses exactly $K = #bound-k$ operations (1 swap + 1 deletion), which is the minimum: a single operation cannot account for both the transposition of two symbols and the removal of one.
+    ]
+  ]
+}
+
 #problem-def("MinimumFeedbackArcSet")[
   Given a directed graph $G = (V, A)$, find a minimum-size subset $A' subset.eq A$ such that $G - A'$ is a directed acyclic graph (DAG). Equivalently, $A'$ must contain at least one arc from every directed cycle in $G$.
 ][
diff --git a/docs/paper/references.bib b/docs/paper/references.bib
index 971493ef1..7418ccd8b 100644
--- a/docs/paper/references.bib
+++ b/docs/paper/references.bib
@@ -1,3 +1,23 @@
+@inproceedings{wagner1975,
+  author    = {Robert A. Wagner},
+  title     = {On the Complexity of the Extended String-to-String Correction Problem},
+  booktitle = {Proceedings of the 7th Annual ACM Symposium on Theory of Computing (STOC)},
+  pages     = {218--223},
+  year      = {1975},
+  doi       = {10.1145/800116.803771}
+}
+
+@article{wagner1974,
+  author  = {Robert A. Wagner and Michael J. Fischer},
+  title   = {The String-to-String Correction Problem},
+  journal = {Journal of the ACM},
+  volume  = {21},
+  number  = {1},
+  pages   = {168--173},
+  year    = {1974},
+  doi     = {10.1145/321796.321811}
+}
+
 @article{juttner2018,
   author  = {Alpár Jüttner and Péter Madarasi},
   title   = {VF2++ — An improved subgraph isomorphism algorithm},
diff --git a/docs/src/cli.md b/docs/src/cli.md
index 563727f23..0bd19f1c1 100644
--- a/docs/src/cli.md
+++ b/docs/src/cli.md
@@ -87,7 +87,8 @@ pred reduce problem.json --to QUBO -o reduced.json
 pred solve reduced.json --solver brute-force
 
 # Pipe commands together (use - to read from stdin)
-pred create MIS --graph 0-1,1-2,2-3 | pred solve -
+pred create MIS --graph 0-1,1-2,2-3 | pred solve -   # when an ILP reduction path exists
+pred create StringToStringCorrection --source-string "0,1,2,3,1,0" --target-string "0,1,3,2,1" --bound 2 | pred solve - --solver brute-force
 pred create MIS --graph 0-1,1-2,2-3 | pred reduce - --to QUBO | pred solve -
 ```
 
@@ -352,6 +353,7 @@ pred create Factoring --target 15 --bits-m 4 --bits-n 4 -o factoring.json
 pred create Factoring --target 21 --bits-m 3 --bits-n 3 -o factoring2.json
 pred create X3C --universe 9 --sets "0,1,2;0,2,4;3,4,5;3,5,7;6,7,8;1,4,6;2,5,8" -o x3c.json
 pred create MinimumTardinessSequencing --n 5 --deadlines 5,5,5,3,3 --precedence-pairs "0>3,1>3,1>4,2>4" -o mts.json
+pred create StringToStringCorrection --source-string "0,1,2,3,1,0" --target-string "0,1,3,2,1" --bound 2 | pred solve - --solver brute-force
 pred create StrongConnectivityAugmentation --arcs "0>1,1>2,2>0,3>4,4>3,2>3,4>5,5>3" --candidate-arcs "3>0:5,3>1:3,3>2:4,4>0:6,4>1:2,4>2:7,5>0:4,5>1:3,5>2:1,0>3:8,0>4:3,0>5:2,1>3:6,1>4:4,1>5:5,2>4:3,2>5:7,1>0:2" --bound 1 -o sca.json
 ```
 
@@ -375,7 +377,8 @@ pred create MaxCut --random --num-vertices 20 --edge-prob 0.5 -o maxcut.json
 Without `-o`, the problem JSON is printed to stdout, which can be piped to other commands:
 
 ```bash
-pred create MIS --graph 0-1,1-2,2-3 | pred solve -
+pred create MIS --graph 0-1,1-2,2-3 | pred solve -   # when an ILP reduction path exists
+pred create StringToStringCorrection --source-string "0,1,2,3,1,0" --target-string "0,1,3,2,1" --bound 2 | pred solve - --solver brute-force
 pred create MIS --random --num-vertices 10 | pred inspect -
 ```
 
diff --git a/problemreductions-cli/src/cli.rs b/problemreductions-cli/src/cli.rs
index b73cac57f..051965959 100644
--- a/problemreductions-cli/src/cli.rs
+++ b/problemreductions-cli/src/cli.rs
@@ -13,7 +13,8 @@ Typical workflow:
   pred evaluate problem.json --config 1,0,1,0
 
 Piping (use - to read from stdin):
-  pred create MIS --graph 0-1,1-2 | pred solve -
+  pred create MIS --graph 0-1,1-2 | pred solve -                    # when an ILP reduction path exists
+  pred create StringToStringCorrection --source-string \"0,1,2,3,1,0\" --target-string \"0,1,3,2,1\" --bound 2 | pred solve - --solver brute-force
   pred create MIS --graph 0-1,1-2 | pred evaluate - --config 1,0,1
   pred create MIS --graph 0-1,1-2 | pred reduce - --to QUBO
 
@@ -257,6 +258,7 @@ Flags by problem type:
   StaffScheduling                 --schedules, --requirements, --num-workers, --k
   MinimumTardinessSequencing      --n, --deadlines [--precedence-pairs]
   SCS                             --strings, --bound [--alphabet-size]
+  StringToStringCorrection         --source-string, --target-string, --bound [--alphabet-size]
   D2CIF                           --arcs, --capacities, --source-1, --sink-1, --source-2, --sink-2, --requirement-1, --requirement-2
   ILP, CircuitSAT                 (via reduction only)
 
@@ -275,6 +277,7 @@ Examples:
   pred create SAT --num-vars 3 --clauses \"1,2;-1,3\"
   pred create QUBO --matrix \"1,0.5;0.5,2\"
   pred create MultipleChoiceBranching/i32 --arcs \"0>1,0>2,1>3,2>3,1>4,3>5,4>5,2>4\" --weights 3,2,4,1,2,3,1,3 --partition \"0,1;2,3;4,7;5,6\" --bound 10
+  pred create StringToStringCorrection --source-string \"0,1,2,3,1,0\" --target-string \"0,1,3,2,1\" --bound 2 | pred solve - --solver brute-force
   pred create MIS/KingsSubgraph --positions \"0,0;1,0;1,1;0,1\"
   pred create MIS/UnitDiskGraph --positions \"0,0;1,0;0.5,0.8\" --radius 1.5
   pred create MIS --random --num-vertices 10 --edge-prob 0.3
@@ -447,7 +450,7 @@ pub struct CreateArgs {
     /// Required edge indices for RuralPostman (comma-separated, e.g., "0,2,4")
     #[arg(long)]
     pub required_edges: Option<String>,
-    /// Upper bound or length bound (for BoundedComponentSpanningForest, LengthBoundedDisjointPaths, MultipleChoiceBranching, OptimalLinearArrangement, RuralPostman, or SCS)
+    /// Upper bound or length bound (for BoundedComponentSpanningForest, LengthBoundedDisjointPaths, MultipleChoiceBranching, OptimalLinearArrangement, RuralPostman, SCS, or StringToStringCorrection)
     #[arg(long, allow_hyphen_values = true)]
     pub bound: Option<i64>,
     /// Pattern graph edge list for SubgraphIsomorphism (e.g., 0-1,1-2,2-0)
@@ -492,9 +495,15 @@ pub struct CreateArgs {
     /// Number of available workers for StaffScheduling
     #[arg(long)]
     pub num_workers: Option<u64>,
-    /// Alphabet size for SCS (optional; inferred from max symbol + 1 if omitted)
+    /// Alphabet size for SCS or StringToStringCorrection (optional; inferred from max symbol + 1 if omitted)
     #[arg(long)]
     pub alphabet_size: Option<usize>,
+    /// Source string for StringToStringCorrection (comma-separated symbol indices, e.g., "0,1,2,3")
+    #[arg(long)]
+    pub source_string: Option<String>,
+    /// Target string for StringToStringCorrection (comma-separated symbol indices, e.g., "0,1,3,2")
+    #[arg(long)]
+    pub target_string: Option<String>,
 }
 
 #[derive(clap::Args)]
@@ -504,7 +513,8 @@ Examples:
   pred solve problem.json --solver brute-force   # brute-force (exhaustive search)
   pred solve reduced.json                        # solve a reduction bundle
   pred solve reduced.json -o solution.json       # save result to file
-  pred create MIS --graph 0-1,1-2 | pred solve - # read from stdin
+  pred create MIS --graph 0-1,1-2 | pred solve - # read from stdin when an ILP path exists
+  pred create StringToStringCorrection --source-string \"0,1,2,3,1,0\" --target-string \"0,1,3,2,1\" --bound 2 | pred solve - --solver brute-force
   pred solve problem.json --timeout 10           # abort after 10 seconds
 
 Typical workflow:
@@ -518,6 +528,8 @@ Solve via explicit reduction:
 Input: a problem JSON from `pred create`, or a reduction bundle from `pred reduce`.
 When given a bundle, the target is solved and the solution is mapped back to the source.
 The ILP solver auto-reduces non-ILP problems before solving.
+Problems without an ILP reduction path, such as `LengthBoundedDisjointPaths` and
+`StringToStringCorrection`, currently need `--solver brute-force`.
 
 ILP backend (default: HiGHS). To use a different backend:
   cargo install problemreductions-cli --features coin-cbc
diff --git a/problemreductions-cli/src/commands/create.rs b/problemreductions-cli/src/commands/create.rs
index 1062fcfe1..25e4454c5 100644
--- a/problemreductions-cli/src/commands/create.rs
+++ b/problemreductions-cli/src/commands/create.rs
@@ -15,7 +15,7 @@ use problemreductions::models::graph::{
 use problemreductions::models::misc::{
     BinPacking, FlowShopScheduling, LongestCommonSubsequence, MinimumTardinessSequencing,
     MultiprocessorScheduling, PaintShop, SequencingWithinIntervals, ShortestCommonSupersequence,
-    SubsetSum,
+    StringToStringCorrection, SubsetSum,
 };
 use problemreductions::models::BiconnectivityAugmentation;
 use problemreductions::prelude::*;
@@ -94,6 +94,15 @@ fn all_data_flags_empty(args: &CreateArgs) -> bool {
         && args.requirements.is_none()
         && args.num_workers.is_none()
         && args.alphabet_size.is_none()
+        && args.source_string.is_none()
+        && args.target_string.is_none()
+        && args.capacities.is_none()
+        && args.source_1.is_none()
+        && args.sink_1.is_none()
+        && args.source_2.is_none()
+        && args.sink_2.is_none()
+        && args.requirement_1.is_none()
+        && args.requirement_2.is_none()
 }
 
 fn emit_problem_output(output: &ProblemJsonOutput, out: &OutputConfig) -> Result<()> {
@@ -321,6 +330,9 @@ fn example_for(canonical: &str, graph_type: Option<&str>) -> &'static str {
         }
         "SetBasis" => "--universe 4 --sets \"0,1;1,2;0,2;0,1,2\" --k 3",
         "ShortestCommonSupersequence" => "--strings \"0,1,2;1,2,0\" --bound 4",
+        "StringToStringCorrection" => {
+            "--source-string \"0,1,2,3,1,0\" --target-string \"0,1,3,2,1\" --bound 2"
+        }
         _ => "",
     }
 }
@@ -408,12 +420,7 @@ fn print_problem_help(canonical: &str, graph_type: Option<&str>) -> Result<()> {
                 );
             } else {
                 let hint = help_flag_hint(canonical, &field.name, &field.type_name, graph_type);
-                eprintln!(
-                    "  --{:<16} {} ({})",
-                    help_flag_name(canonical, &field.name),
-                    field.description,
-                    hint
-                );
+                eprintln!("  --{:<16} {} ({})", flag_name, field.description, hint);
             }
         }
     } else {
@@ -450,10 +457,15 @@ fn problem_help_flag_name(
     if canonical == "LengthBoundedDisjointPaths" && field_name == "max_length" {
         return "bound".to_string();
     }
-    if canonical == "StaffScheduling" && field_name == "shifts_per_schedule" {
-        return "k".to_string();
+    if canonical == "StringToStringCorrection" {
+        return match field_name {
+            "source" => "source-string".to_string(),
+            "target" => "target-string".to_string(),
+            "bound" => "bound".to_string(),
+            _ => help_flag_name(canonical, field_name),
+        };
     }
-    field_name.replace('_', "-")
+    help_flag_name(canonical, field_name)
 }
 
 fn lbdp_validation_error(message: &str, usage: Option<&str>) -> anyhow::Error {
@@ -1779,6 +1791,58 @@ pub fn create(args: &CreateArgs, out: &OutputConfig) -> Result<()> {
                 resolved_variant.clone(),
             )
         }
+
+        // StringToStringCorrection
+        "StringToStringCorrection" => {
+            let usage = "Usage: pred create StringToStringCorrection --source-string \"0,1,2,3,1,0\" --target-string \"0,1,3,2,1\" --bound 2";
+            let source_str = args.source_string.as_deref().ok_or_else(|| {
+                anyhow::anyhow!("StringToStringCorrection requires --source-string\n\n{usage}")
+            })?;
+            let target_str = args.target_string.as_deref().ok_or_else(|| {
+                anyhow::anyhow!("StringToStringCorrection requires --target-string\n\n{usage}")
+            })?;
+            let bound = parse_nonnegative_usize_bound(
+                args.bound.ok_or_else(|| {
+                    anyhow::anyhow!("StringToStringCorrection requires --bound\n\n{usage}")
+                })?,
+                "StringToStringCorrection",
+                usage,
+            )?;
+            let parse_symbols = |s: &str| -> Result<Vec<usize>> {
+                if s.trim().is_empty() {
+                    return Ok(Vec::new());
+                }
+                s.split(',')
+                    .map(|v| v.trim().parse::<usize>().context("invalid symbol index"))
+                    .collect()
+            };
+            let source = parse_symbols(source_str)?;
+            let target = parse_symbols(target_str)?;
+            let inferred = source
+                .iter()
+                .chain(target.iter())
+                .copied()
+                .max()
+                .map_or(0, |m| m + 1);
+            let alphabet_size = args.alphabet_size.unwrap_or(inferred);
+            if alphabet_size < inferred {
+                anyhow::bail!(
+                    "--alphabet-size {} is smaller than max symbol + 1 ({}) in the strings",
+                    alphabet_size,
+                    inferred
+                );
+            }
+            (
+                ser(StringToStringCorrection::new(
+                    alphabet_size,
+                    source,
+                    target,
+                    bound,
+                ))?,
+                resolved_variant.clone(),
+            )
+        }
+
         _ => bail!("{}", crate::problem_name::unknown_problem_error(canonical)),
     };
 
@@ -2987,6 +3051,22 @@ mod tests {
         );
     }
 
+    #[test]
+    fn test_problem_help_uses_string_to_string_correction_cli_flags() {
+        assert_eq!(
+            problem_help_flag_name("StringToStringCorrection", "source", "Vec<usize>", false),
+            "source-string"
+        );
+        assert_eq!(
+            problem_help_flag_name("StringToStringCorrection", "target", "Vec<usize>", false),
+            "target-string"
+        );
+        assert_eq!(
+            problem_help_flag_name("StringToStringCorrection", "bound", "usize", false),
+            "bound"
+        );
+    }
+
     #[test]
     fn test_problem_help_uses_k_for_staff_scheduling() {
         assert_eq!(
@@ -3160,6 +3240,8 @@ mod tests {
             deadline: None,
             num_processors: None,
             alphabet_size: None,
+            source_string: None,
+            target_string: None,
             schedules: None,
             requirements: None,
             num_workers: None,
diff --git a/problemreductions-cli/tests/cli_tests.rs b/problemreductions-cli/tests/cli_tests.rs
index 76058569b..112c102c2 100644
--- a/problemreductions-cli/tests/cli_tests.rs
+++ b/problemreductions-cli/tests/cli_tests.rs
@@ -33,6 +33,18 @@ fn test_list_includes_undirected_two_commodity_integral_flow() {
     assert!(stdout.contains("UndirectedTwoCommodityIntegralFlow"));
 }
 
+#[test]
+fn test_solve_help_mentions_string_to_string_correction_bruteforce() {
+    let output = pred().args(["solve", "--help"]).output().unwrap();
+    assert!(output.status.success());
+    let stdout = String::from_utf8(output.stdout).unwrap();
+    assert!(
+        stdout.contains("StringToStringCorrection"),
+        "stdout: {stdout}"
+    );
+    assert!(stdout.contains("--solver brute-force"), "stdout: {stdout}");
+}
+
 #[test]
 fn test_list_rules() {
     let output = pred().args(["list", "--rules"]).output().unwrap();
@@ -2265,6 +2277,101 @@ fn test_create_scs_rejects_negative_bound() {
     assert!(stderr.contains("nonnegative --bound"), "stderr: {stderr}");
 }
 
+#[test]
+fn test_create_string_to_string_correction() {
+    let output_file =
+        std::env::temp_dir().join("pred_test_create_string_to_string_correction.json");
+    let output = pred()
+        .args([
+            "-o",
+            output_file.to_str().unwrap(),
+            "create",
+            "StringToStringCorrection",
+            "--source-string",
+            "0,1,2,3,1,0",
+            "--target-string",
+            "0,1,3,2,1",
+            "--bound",
+            "2",
+        ])
+        .output()
+        .unwrap();
+    assert!(
+        output.status.success(),
+        "stderr: {}",
+        String::from_utf8_lossy(&output.stderr)
+    );
+    let content = std::fs::read_to_string(&output_file).unwrap();
+    let json: serde_json::Value = serde_json::from_str(&content).unwrap();
+    assert_eq!(json["type"], "StringToStringCorrection");
+    assert_eq!(
+        json["data"]["source"],
+        serde_json::json!([0, 1, 2, 3, 1, 0])
+    );
+    assert_eq!(json["data"]["target"], serde_json::json!([0, 1, 3, 2, 1]));
+    assert_eq!(json["data"]["bound"], 2);
+    std::fs::remove_file(&output_file).ok();
+}
+
+#[test]
+fn test_create_model_example_string_to_string_correction() {
+    let output = pred()
+        .args(["create", "--example", "StringToStringCorrection"])
+        .output()
+        .unwrap();
+    assert!(
+        output.status.success(),
+        "stderr: {}",
+        String::from_utf8_lossy(&output.stderr)
+    );
+    let stdout = String::from_utf8(output.stdout).unwrap();
+    let json: serde_json::Value = serde_json::from_str(&stdout).unwrap();
+    assert_eq!(json["type"], "StringToStringCorrection");
+    assert_eq!(
+        json["data"]["source"],
+        serde_json::json!([0, 1, 2, 3, 1, 0])
+    );
+    assert_eq!(json["data"]["target"], serde_json::json!([0, 1, 3, 2, 1]));
+    assert_eq!(json["data"]["bound"], 2);
+}
+
+#[test]
+fn test_create_string_to_string_correction_help_uses_cli_flags() {
+    let output = pred()
+        .args(["create", "StringToStringCorrection"])
+        .output()
+        .unwrap();
+    assert!(!output.status.success());
+    let stderr = String::from_utf8_lossy(&output.stderr);
+    assert!(stderr.contains("--source-string"), "stderr: {stderr}");
+    assert!(stderr.contains("--target-string"), "stderr: {stderr}");
+    assert!(stderr.contains("--bound"), "stderr: {stderr}");
+    assert!(!stderr.contains("--bound-k"), "stderr: {stderr}");
+}
+
+#[test]
+fn test_create_string_to_string_correction_rejects_negative_bound() {
+    let output = pred()
+        .args([
+            "create",
+            "StringToStringCorrection",
+            "--source-string",
+            "0,1,2,3,1,0",
+            "--target-string",
+            "0,1,3,2,1",
+            "--bound",
+            "-1",
+        ])
+        .output()
+        .unwrap();
+    assert!(
+        !output.status.success(),
+        "negative bound should be rejected"
+    );
+    let stderr = String::from_utf8_lossy(&output.stderr);
+    assert!(stderr.contains("nonnegative --bound"), "stderr: {stderr}");
+}
+
 #[test]
 fn test_create_spinglass() {
     let output_file = std::env::temp_dir().join("pred_test_create_sg.json");
diff --git a/src/example_db/fixtures/examples.json b/src/example_db/fixtures/examples.json
index 84ca94ac3..10b81634e 100644
--- a/src/example_db/fixtures/examples.json
+++ b/src/example_db/fixtures/examples.json
@@ -43,6 +43,7 @@
     {"problem":"SpinGlass","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"couplings":[1,1,1,1,1,1,1],"fields":[0,0,0,0,0],"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[1,2,null],[3,4,null],[0,3,null],[1,3,null],[1,4,null],[2,4,null]],"node_holes":[],"nodes":[null,null,null,null,null]}}},"samples":[{"config":[1,0,1,1,0],"metric":{"Valid":-3}}],"optimal":[{"config":[0,0,1,1,0],"metric":{"Valid":-3}},{"config":[0,1,0,0,1],"metric":{"Valid":-3}},{"config":[0,1,0,1,0],"metric":{"Valid":-3}},{"config":[0,1,1,1,0],"metric":{"Valid":-3}},{"config":[1,0,0,0,1],"metric":{"Valid":-3}},{"config":[1,0,1,0,1],"metric":{"Valid":-3}},{"config":[1,0,1,1,0],"metric":{"Valid":-3}},{"config":[1,1,0,0,1],"metric":{"Valid":-3}}]},
     {"problem":"StaffScheduling","variant":{},"instance":{"num_workers":4,"requirements":[2,2,2,3,3,2,1],"schedules":[[true,true,true,true,true,false,false],[false,true,true,true,true,true,false],[false,false,true,true,true,true,true],[true,false,false,true,true,true,true],[true,true,false,false,true,true,true]],"shifts_per_schedule":5},"samples":[{"config":[1,1,1,1,0],"metric":true}],"optimal":[{"config":[0,1,1,1,1],"metric":true},{"config":[0,2,0,1,1],"metric":true},{"config":[0,2,0,2,0],"metric":true},{"config":[1,0,1,1,1],"metric":true},{"config":[1,0,2,0,1],"metric":true},{"config":[1,1,0,1,0],"metric":true},{"config":[1,1,0,1,1],"metric":true},{"config":[1,1,0,2,0],"metric":true},{"config":[1,1,1,0,1],"metric":true},{"config":[1,1,1,1,0],"metric":true},{"config":[1,2,0,0,1],"metric":true},{"config":[1,2,0,1,0],"metric":true},{"config":[2,0,0,1,1],"metric":true},{"config":[2,0,0,2,0],"metric":true},{"config":[2,0,1,0,1],"metric":true},{"config":[2,0,1,1,0],"metric":true},{"config":[2,0,2,0,0],"metric":true},{"config":[2,1,0,0,1],"metric":true},{"config":[2,1,0,1,0],"metric":true},{"config":[2,1,1,0,0],"metric":true}]},
     {"problem":"SteinerTree","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"edge_weights":[2,5,2,1,5,6,1],"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,3,null],[1,2,null],[1,3,null],[2,3,null],[2,4,null],[3,4,null]],"node_holes":[],"nodes":[null,null,null,null,null]}},"terminals":[0,2,4]},"samples":[{"config":[1,0,1,1,0,0,1],"metric":{"Valid":6}}],"optimal":[{"config":[1,0,1,1,0,0,1],"metric":{"Valid":6}}]},
+    {"problem":"StringToStringCorrection","variant":{},"instance":{"alphabet_size":4,"bound":2,"source":[0,1,2,3,1,0],"target":[0,1,3,2,1]},"samples":[{"config":[8,5],"metric":true}],"optimal":[{"config":[5,7],"metric":true},{"config":[8,5],"metric":true}]},
     {"problem":"StrongConnectivityAugmentation","variant":{"weight":"i32"},"instance":{"bound":1,"candidate_arcs":[[3,0,5],[3,1,3],[3,2,4],[4,0,6],[4,1,2],[4,2,7],[5,0,4],[5,1,3],[5,2,1],[0,3,8],[0,4,3],[0,5,2],[1,3,6],[1,4,4],[1,5,5],[2,4,3],[2,5,7],[1,0,2]],"graph":{"inner":{"edge_property":"directed","edges":[[0,1,null],[1,2,null],[2,0,null],[3,4,null],[4,3,null],[2,3,null],[4,5,null],[5,3,null]],"node_holes":[],"nodes":[null,null,null,null,null,null]}}},"samples":[{"config":[0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0],"metric":true},{"config":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"metric":false}],"optimal":[{"config":[0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0],"metric":true}]},
     {"problem":"TravelingSalesman","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"edge_weights":[1,3,2,2,3,1],"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,2,null],[0,3,null],[1,2,null],[1,3,null],[2,3,null]],"node_holes":[],"nodes":[null,null,null,null]}}},"samples":[{"config":[1,0,1,1,0,1],"metric":{"Valid":6}}],"optimal":[{"config":[1,0,1,1,0,1],"metric":{"Valid":6}}]},
     {"problem":"UndirectedTwoCommodityIntegralFlow","variant":{},"instance":{"capacities":[1,1,2],"graph":{"inner":{"edge_property":"undirected","edges":[[0,2,null],[1,2,null],[2,3,null]],"node_holes":[],"nodes":[null,null,null,null]}},"requirement_1":1,"requirement_2":1,"sink_1":3,"sink_2":3,"source_1":0,"source_2":1},"samples":[{"config":[1,0,0,0,0,0,1,0,1,0,1,0],"metric":true}],"optimal":[{"config":[0,0,1,0,1,0,0,0,1,0,1,0],"metric":true},{"config":[1,0,0,0,0,0,1,0,1,0,1,0],"metric":true}]}
@@ -59,7 +60,7 @@
     {"source":{"problem":"KSatisfiability","variant":{"k":"K2"},"instance":{"clauses":[{"literals":[1,2]},{"literals":[-1,3]},{"literals":[-2,4]},{"literals":[-3,-4]}],"num_vars":4}},"target":{"problem":"QUBO","variant":{"weight":"f64"},"instance":{"matrix":[[0.0,1.0,-1.0,0.0],[0.0,0.0,0.0,-1.0],[0.0,0.0,0.0,1.0],[0.0,0.0,0.0,0.0]],"num_vars":4}},"solutions":[{"source_config":[0,1,0,1],"target_config":[0,1,0,1]}]},
     {"source":{"problem":"KSatisfiability","variant":{"k":"K3"},"instance":{"clauses":[{"literals":[1,2,-3]},{"literals":[-1,3,4]},{"literals":[2,-4,5]},{"literals":[-2,3,-5]},{"literals":[1,-3,5]},{"literals":[-1,-2,4]},{"literals":[3,-4,-5]}],"num_vars":5}},"target":{"problem":"QUBO","variant":{"weight":"f64"},"instance":{"matrix":[[0.0,4.0,-4.0,0.0,0.0,4.0,-4.0,0.0,0.0,4.0,-4.0,0.0],[0.0,0.0,-2.0,-2.0,0.0,4.0,0.0,4.0,-4.0,0.0,-4.0,0.0],[0.0,0.0,2.0,-2.0,0.0,1.0,4.0,0.0,4.0,-4.0,0.0,4.0],[0.0,0.0,0.0,4.0,0.0,0.0,-1.0,-4.0,0.0,0.0,-1.0,-4.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,-1.0,1.0,-1.0,0.0,1.0],[0.0,0.0,0.0,0.0,0.0,-2.0,0.0,0.0,0.0,0.0,0.0,0.0],[0.0,0.0,0.0,0.0,0.0,0.0,3.0,0.0,0.0,0.0,0.0,0.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,3.0,0.0,0.0,0.0,0.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,2.0,0.0,0.0,0.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,3.0,0.0,0.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,7.0,0.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,2.0]],"num_vars":12}},"solutions":[{"source_config":[1,1,1,1,1],"target_config":[1,1,1,1,1,0,0,0,0,0,1,0]}]},
     {"source":{"problem":"KSatisfiability","variant":{"k":"K3"},"instance":{"clauses":[{"literals":[1,2,3]},{"literals":[-1,-2,3]}],"num_vars":3}},"target":{"problem":"SubsetSum","variant":{},"instance":{"sizes":["10010","10001","1010","1001","111","100","10","20","1","2"],"target":"11144"}},"solutions":[{"source_config":[0,0,1],"target_config":[0,1,0,1,1,0,1,1,1,0]}]},
-    {"source":{"problem":"KSatisfiability","variant":{"k":"KN"},"instance":{"clauses":[{"literals":[1,-2,3]},{"literals":[-1,3,4]},{"literals":[2,-3,-4]}],"num_vars":4}},"target":{"problem":"Satisfiability","variant":{},"instance":{"clauses":[{"literals":[1,-2,3]},{"literals":[-1,3,4]},{"literals":[2,-3,-4]}],"num_vars":4}},"solutions":[{"source_config":[1,1,1,0],"target_config":[1,1,1,0]}]},
+    {"source":{"problem":"KSatisfiability","variant":{"k":"KN"},"instance":{"clauses":[{"literals":[1,-2,3]},{"literals":[-1,3,4]},{"literals":[2,-3,-4]}],"num_vars":4}},"target":{"problem":"Satisfiability","variant":{},"instance":{"clauses":[{"literals":[1,-2,3]},{"literals":[-1,3,4]},{"literals":[2,-3,-4]}],"num_vars":4}},"solutions":[{"source_config":[1,1,1,1],"target_config":[1,1,1,1]}]},
     {"source":{"problem":"Knapsack","variant":{},"instance":{"capacity":7,"values":[3,4,5,7],"weights":[2,3,4,5]}},"target":{"problem":"QUBO","variant":{"weight":"f64"},"instance":{"matrix":[[-483.0,240.0,320.0,400.0,80.0,160.0,320.0],[0.0,-664.0,480.0,600.0,120.0,240.0,480.0],[0.0,0.0,-805.0,800.0,160.0,320.0,640.0],[0.0,0.0,0.0,-907.0,200.0,400.0,800.0],[0.0,0.0,0.0,0.0,-260.0,80.0,160.0],[0.0,0.0,0.0,0.0,0.0,-480.0,320.0],[0.0,0.0,0.0,0.0,0.0,0.0,-800.0]],"num_vars":7}},"solutions":[{"source_config":[1,0,0,1],"target_config":[1,0,0,1,0,0,0]}]},
     {"source":{"problem":"LongestCommonSubsequence","variant":{},"instance":{"strings":[[65,66,65,67],[66,65,67,65]]}},"target":{"problem":"ILP","variant":{"variable":"bool"},"instance":{"constraints":[{"cmp":"Le","rhs":1.0,"terms":[[0,1.0],[1,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[2,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[3,1.0],[4,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[5,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[2,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[0,1.0],[3,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[5,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[1,1.0],[4,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[0,1.0],[2,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[1,1.0],[2,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[1,1.0],[3,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[1,1.0],[5,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[4,1.0],[5,1.0]]}],"num_vars":6,"objective":[[0,1.0],[1,1.0],[2,1.0],[3,1.0],[4,1.0],[5,1.0]],"sense":"Maximize"}},"solutions":[{"source_config":[0,1,1,1],"target_config":[0,0,1,1,0,1]}]},
     {"source":{"problem":"MaxCut","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"edge_weights":[1,1,1,1,1,1,1,1,1,1,1,1,1,1,1],"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,4,null],[0,5,null],[1,2,null],[1,6,null],[2,3,null],[2,7,null],[3,4,null],[3,8,null],[4,9,null],[5,7,null],[5,8,null],[6,8,null],[6,9,null],[7,9,null]],"node_holes":[],"nodes":[null,null,null,null,null,null,null,null,null,null]}}}},"target":{"problem":"SpinGlass","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"couplings":[1,1,1,1,1,1,1,1,1,1,1,1,1,1,1],"fields":[0,0,0,0,0,0,0,0,0,0],"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,4,null],[0,5,null],[1,2,null],[1,6,null],[2,3,null],[2,7,null],[3,4,null],[3,8,null],[4,9,null],[5,7,null],[5,8,null],[6,8,null],[6,9,null],[7,9,null]],"node_holes":[],"nodes":[null,null,null,null,null,null,null,null,null,null]}}}},"solutions":[{"source_config":[1,0,1,0,0,0,0,0,1,1],"target_config":[1,0,1,0,0,0,0,0,1,1]}]},
diff --git a/src/lib.rs b/src/lib.rs
index 8fdc95511..0c0347eb2 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -60,7 +60,7 @@ pub mod prelude {
     pub use crate::models::misc::{
         BinPacking, Factoring, FlowShopScheduling, Knapsack, LongestCommonSubsequence,
         MinimumTardinessSequencing, MultiprocessorScheduling, PaintShop, SequencingWithinIntervals,
-        ShortestCommonSupersequence, StaffScheduling, SubsetSum,
+        ShortestCommonSupersequence, StaffScheduling, StringToStringCorrection, SubsetSum,
     };
     pub use crate::models::set::{
         ComparativeContainment, ExactCoverBy3Sets, MaximumSetPacking, MinimumSetCovering, SetBasis,
diff --git a/src/models/misc/mod.rs b/src/models/misc/mod.rs
index 22ff3a96e..24b28125d 100644
--- a/src/models/misc/mod.rs
+++ b/src/models/misc/mod.rs
@@ -11,6 +11,7 @@
 //! - [`PaintShop`]: Minimize color switches in paint shop scheduling
 //! - [`SequencingWithinIntervals`]: Schedule tasks within time windows
 //! - [`ShortestCommonSupersequence`]: Find a common supersequence of bounded length
+//! - [`StringToStringCorrection`]: String-to-String Correction (derive target via deletions and swaps)
 //! - [`SubsetSum`]: Find a subset summing to exactly a target value
 
 mod bin_packing;
@@ -24,6 +25,7 @@ pub(crate) mod paintshop;
 mod sequencing_within_intervals;
 pub(crate) mod shortest_common_supersequence;
 mod staff_scheduling;
+pub(crate) mod string_to_string_correction;
 mod subset_sum;
 
 pub use bin_packing::BinPacking;
@@ -37,6 +39,7 @@ pub use paintshop::PaintShop;
 pub use sequencing_within_intervals::SequencingWithinIntervals;
 pub use shortest_common_supersequence::ShortestCommonSupersequence;
 pub use staff_scheduling::StaffScheduling;
+pub use string_to_string_correction::StringToStringCorrection;
 pub use subset_sum::SubsetSum;
 
 #[cfg(feature = "example-db")]
@@ -48,6 +51,7 @@ pub(crate) fn canonical_model_example_specs() -> Vec<crate::example_db::specs::M
     specs.extend(sequencing_within_intervals::canonical_model_example_specs());
     specs.extend(staff_scheduling::canonical_model_example_specs());
     specs.extend(shortest_common_supersequence::canonical_model_example_specs());
+    specs.extend(string_to_string_correction::canonical_model_example_specs());
     specs.extend(minimum_tardiness_sequencing::canonical_model_example_specs());
     specs
 }
diff --git a/src/models/misc/string_to_string_correction.rs b/src/models/misc/string_to_string_correction.rs
new file mode 100644
index 000000000..a35af8c69
--- /dev/null
+++ b/src/models/misc/string_to_string_correction.rs
@@ -0,0 +1,219 @@
+//! String-to-String Correction problem implementation.
+//!
+//! Given a source string `s` and a target string `t` over a finite alphabet,
+//! and a bound `K`, the problem asks whether `t` can be derived from `s`
+//! using at most `K` operations, where each operation is either a deletion
+//! of a character or a swap of two adjacent characters.
+//!
+//! The configuration is a vector of length `K`, where each entry encodes one
+//! operation. For a source of length `n`, each entry is in `{0, ..., 2n}`:
+//! - `0..current_len` → delete the character at that index
+//! - `current_len..2n` → swap the character at position `value - current_len`
+//!   with its right neighbor
+//! - `2n` → no-op (skip this operation slot)
+//!
+//! This problem is NP-complete (Wagner, 1975).
+
+use crate::registry::{FieldInfo, ProblemSchemaEntry};
+use crate::traits::{Problem, SatisfactionProblem};
+use serde::{Deserialize, Serialize};
+
+inventory::submit! {
+    ProblemSchemaEntry {
+        name: "StringToStringCorrection",
+        display_name: "String-to-String Correction",
+        aliases: &[],
+        dimensions: &[],
+        module_path: module_path!(),
+        description: "Derive target string from source using at most K deletions and adjacent swaps",
+        fields: &[
+            FieldInfo { name: "alphabet_size", type_name: "usize", description: "Size of the finite alphabet" },
+            FieldInfo { name: "source", type_name: "Vec<usize>", description: "Source string (symbol indices)" },
+            FieldInfo { name: "target", type_name: "Vec<usize>", description: "Target string (symbol indices)" },
+            FieldInfo { name: "bound", type_name: "usize", description: "Maximum number of operations allowed" },
+        ],
+    }
+}
+
+/// The String-to-String Correction problem.
+///
+/// Given an alphabet of size `a`, a source string `s` over `{0, ..., a-1}`,
+/// a target string `t` over the same alphabet, and a bound `K`, determine
+/// whether `t` can be obtained from `s` by applying at most `K` operations,
+/// where each operation is either a character deletion or a swap of two
+/// adjacent characters.
+///
+/// # Representation
+///
+/// The configuration is a vector of length `K`. For a source string of
+/// length `n`, each entry is in `{0, ..., 2n}`:
+/// - Values `0..current_len` delete the character at that index in the
+///   current working string.
+/// - Values `current_len..2n` swap the character at position
+///   `value - current_len` with its right neighbor.
+/// - Value `2n` is a no-op (skip this slot).
+///
+/// The domain size per slot is fixed at `2n + 1` regardless of how
+/// deletions shorten the working string; as the working string shrinks,
+/// some encodings that were valid before may become invalid.
+///
+/// # Example
+///
+/// ```
+/// use problemreductions::models::misc::StringToStringCorrection;
+/// use problemreductions::{Problem, Solver, BruteForce};
+///
+/// // source = [0,1,2,3,1,0], target = [0,1,3,2,1], bound = 2
+/// let problem = StringToStringCorrection::new(4, vec![0,1,2,3,1,0], vec![0,1,3,2,1], 2);
+/// let solver = BruteForce::new();
+/// let solution = solver.find_satisfying(&problem);
+/// assert!(solution.is_some());
+/// ```
+#[derive(Debug, Clone, Serialize, Deserialize)]
+pub struct StringToStringCorrection {
+    alphabet_size: usize,
+    source: Vec<usize>,
+    target: Vec<usize>,
+    bound: usize,
+}
+
+impl StringToStringCorrection {
+    /// Create a new StringToStringCorrection instance.
+    ///
+    /// # Panics
+    ///
+    /// Panics if `alphabet_size` is 0 when the source or target string is
+    /// non-empty, or if any symbol in `source` or `target` is
+    /// `>= alphabet_size`.
+    pub fn new(alphabet_size: usize, source: Vec<usize>, target: Vec<usize>, bound: usize) -> Self {
+        assert!(
+            alphabet_size > 0 || (source.is_empty() && target.is_empty()),
+            "alphabet_size must be > 0 when source or target is non-empty"
+        );
+        assert!(
+            source.iter().all(|&s| s < alphabet_size),
+            "all source symbols must be < alphabet_size"
+        );
+        assert!(
+            target.iter().all(|&s| s < alphabet_size),
+            "all target symbols must be < alphabet_size"
+        );
+        Self {
+            alphabet_size,
+            source,
+            target,
+            bound,
+        }
+    }
+
+    /// Returns the alphabet size.
+    pub fn alphabet_size(&self) -> usize {
+        self.alphabet_size
+    }
+
+    /// Returns the source string.
+    pub fn source(&self) -> &[usize] {
+        &self.source
+    }
+
+    /// Returns the target string.
+    pub fn target(&self) -> &[usize] {
+        &self.target
+    }
+
+    /// Returns the operation bound.
+    pub fn bound(&self) -> usize {
+        self.bound
+    }
+
+    /// Returns the length of the source string.
+    pub fn source_length(&self) -> usize {
+        self.source.len()
+    }
+
+    /// Returns the length of the target string.
+    pub fn target_length(&self) -> usize {
+        self.target.len()
+    }
+}
+
+impl Problem for StringToStringCorrection {
+    const NAME: &'static str = "StringToStringCorrection";
+    type Metric = bool;
+
+    fn variant() -> Vec<(&'static str, &'static str)> {
+        crate::variant_params![]
+    }
+
+    fn dims(&self) -> Vec<usize> {
+        vec![2 * self.source.len() + 1; self.bound]
+    }
+
+    fn evaluate(&self, config: &[usize]) -> bool {
+        if config.len() != self.bound {
+            return false;
+        }
+        if self.target.len() > self.source.len()
+            || self.target.len() < self.source.len().saturating_sub(self.bound)
+        {
+            return false;
+        }
+        let n = self.source.len();
+        let domain = 2 * n + 1;
+        if config.iter().any(|&v| v >= domain) {
+            return false;
+        }
+        let noop = 2 * n;
+        let mut working = self.source.clone();
+        for &op in config {
+            if op == noop {
+                // no-op
+                continue;
+            }
+            let current_len = working.len();
+            if op < current_len {
+                // delete at index op
+                working.remove(op);
+            } else {
+                let swap_pos = op - current_len;
+                if swap_pos + 1 < current_len {
+                    working.swap(swap_pos, swap_pos + 1);
+                } else {
+                    // invalid operation for current string state
+                    return false;
+                }
+            }
+        }
+        working == self.target
+    }
+}
+
+impl SatisfactionProblem for StringToStringCorrection {}
+
+crate::declare_variants! {
+    default sat StringToStringCorrection => "(2 * source_length + 1) ^ bound",
+}
+
+#[cfg(feature = "example-db")]
+pub(crate) fn canonical_model_example_specs() -> Vec<crate::example_db::specs::ModelExampleSpec> {
+    vec![crate::example_db::specs::ModelExampleSpec {
+        id: "string_to_string_correction",
+        build: || {
+            let problem =
+                StringToStringCorrection::new(4, vec![0, 1, 2, 3, 1, 0], vec![0, 1, 3, 2, 1], 2);
+            // source has length 6. Domain = 2*6+1 = 13. No-op = 12.
+            // First operation: swap at positions 2,3 in original 6-element string.
+            //   current_len = 6, so swap range starts at 6.
+            //   swap_pos = value - current_len. For swap_pos=2, value = 6 + 2 = 8
+            //   After swap: [0,1,3,2,1,0]
+            // Second operation: delete at position 5 (the trailing 0).
+            //   current_len = 6, 5 < 6 → delete index 5
+            //   After delete: [0,1,3,2,1] = target
+            crate::example_db::specs::satisfaction_example(problem, vec![vec![8, 5]])
+        },
+    }]
+}
+
+#[cfg(test)]
+#[path = "../../unit_tests/models/misc/string_to_string_correction.rs"]
+mod tests;
diff --git a/src/models/mod.rs b/src/models/mod.rs
index 4711d9bbd..d25015413 100644
--- a/src/models/mod.rs
+++ b/src/models/mod.rs
@@ -24,7 +24,7 @@ pub use graph::{
 pub use misc::{
     BinPacking, Factoring, FlowShopScheduling, Knapsack, LongestCommonSubsequence,
     MinimumTardinessSequencing, MultiprocessorScheduling, PaintShop, SequencingWithinIntervals,
-    ShortestCommonSupersequence, StaffScheduling, SubsetSum,
+    ShortestCommonSupersequence, StaffScheduling, StringToStringCorrection, SubsetSum,
 };
 pub use set::{
     ComparativeContainment, ExactCoverBy3Sets, MaximumSetPacking, MinimumSetCovering, SetBasis,
diff --git a/src/unit_tests/models/misc/string_to_string_correction.rs b/src/unit_tests/models/misc/string_to_string_correction.rs
new file mode 100644
index 000000000..9b4c25063
--- /dev/null
+++ b/src/unit_tests/models/misc/string_to_string_correction.rs
@@ -0,0 +1,151 @@
+use super::*;
+use crate::solvers::{BruteForce, Solver};
+use crate::traits::Problem;
+
+#[test]
+fn test_string_to_string_correction_creation() {
+    let problem = StringToStringCorrection::new(4, vec![0, 1, 2, 3, 1, 0], vec![0, 1, 3, 2, 1], 2);
+    assert_eq!(problem.alphabet_size(), 4);
+    assert_eq!(problem.source(), &[0, 1, 2, 3, 1, 0]);
+    assert_eq!(problem.target(), &[0, 1, 3, 2, 1]);
+    assert_eq!(problem.bound(), 2);
+    assert_eq!(problem.source_length(), 6);
+    assert_eq!(problem.target_length(), 5);
+    // domain = 2*6+1 = 13, bound = 2
+    assert_eq!(problem.dims(), vec![13; 2]);
+    assert_eq!(
+        <StringToStringCorrection as Problem>::NAME,
+        "StringToStringCorrection"
+    );
+    assert_eq!(<StringToStringCorrection as Problem>::variant(), vec![]);
+}
+
+#[test]
+fn test_string_to_string_correction_evaluation() {
+    let problem = StringToStringCorrection::new(4, vec![0, 1, 2, 3, 1, 0], vec![0, 1, 3, 2, 1], 2);
+    // Known solution: swap positions 2&3 (value=8), then delete index 5 (value=5)
+    // Step 1: current_len=6, op=8 >= 6, swap_pos = 8-6=2, swap(2,3) → [0,1,3,2,1,0]
+    // Step 2: current_len=6, op=5 < 6, delete(5) → [0,1,3,2,1] = target
+    assert!(problem.evaluate(&[8, 5]));
+    // All no-ops should not produce target (source != target)
+    assert!(!problem.evaluate(&[12, 12]));
+}
+
+#[test]
+fn test_string_to_string_correction_invalid_operations() {
+    let problem = StringToStringCorrection::new(4, vec![0, 1, 2, 3, 1, 0], vec![0, 1, 3, 2, 1], 2);
+    // out-of-domain values
+    assert!(!problem.evaluate(&[13, 5]));
+    assert!(!problem.evaluate(&[8, 13]));
+    // wrong length config
+    assert!(!problem.evaluate(&[8]));
+    assert!(!problem.evaluate(&[8, 5, 12]));
+}
+
+#[test]
+fn test_string_to_string_correction_invalid_after_deletion() {
+    // After a deletion, some swap indices become invalid
+    let problem = StringToStringCorrection::new(2, vec![0, 1, 0], vec![1], 2);
+    // source len = 3, domain = 7, noop = 6
+    // op=0: delete index 0 → [1, 0], current_len=2
+    // op=5: 5 >= 2, swap_pos = 5-2=3, need 3+1<2 → false → invalid
+    assert!(!problem.evaluate(&[0, 5]));
+}
+
+#[test]
+fn test_string_to_string_correction_serialization() {
+    let problem = StringToStringCorrection::new(4, vec![0, 1, 2, 3, 1, 0], vec![0, 1, 3, 2, 1], 2);
+    let json = serde_json::to_value(&problem).unwrap();
+    let restored: StringToStringCorrection = serde_json::from_value(json).unwrap();
+    assert_eq!(restored.alphabet_size(), problem.alphabet_size());
+    assert_eq!(restored.source(), problem.source());
+    assert_eq!(restored.target(), problem.target());
+    assert_eq!(restored.bound(), problem.bound());
+}
+
+#[test]
+fn test_string_to_string_correction_solver() {
+    // Small instance: source [0,1], target [1,0], bound 1
+    // Need a single swap: swap_pos=0, value = current_len + 0 = 2
+    let problem = StringToStringCorrection::new(2, vec![0, 1], vec![1, 0], 1);
+    let solver = BruteForce::new();
+    let solution = solver
+        .find_satisfying(&problem)
+        .expect("should find a solution");
+    assert!(problem.evaluate(&solution));
+}
+
+#[test]
+fn test_string_to_string_correction_paper_example() {
+    // Paper example: source [0,1,2,3,1,0], target [0,1,3,2,1], bound 2
+    let problem = StringToStringCorrection::new(4, vec![0, 1, 2, 3, 1, 0], vec![0, 1, 3, 2, 1], 2);
+    // Verify the known solution
+    assert!(problem.evaluate(&[8, 5]));
+
+    // Verify all solutions with brute force
+    let solver = BruteForce::new();
+    let all_solutions = solver.find_all_satisfying(&problem);
+    assert!(!all_solutions.is_empty());
+    // The known solution must be among them
+    assert!(all_solutions.contains(&vec![8, 5]));
+    for sol in &all_solutions {
+        assert!(problem.evaluate(sol));
+    }
+}
+
+#[test]
+fn test_string_to_string_correction_unsatisfiable() {
+    // bound=0, source != target → impossible
+    let problem = StringToStringCorrection::new(2, vec![0, 1], vec![1, 0], 0);
+    assert_eq!(problem.dims(), Vec::<usize>::new());
+    assert!(!problem.evaluate(&[]));
+
+    let solver = BruteForce::new();
+    assert!(solver.find_satisfying(&problem).is_none());
+}
+
+#[test]
+fn test_string_to_string_correction_identity() {
+    // source == target, bound_k=0 → satisfied with empty config
+    let problem = StringToStringCorrection::new(2, vec![0, 1], vec![0, 1], 0);
+    assert!(problem.evaluate(&[]));
+}
+
+#[test]
+fn test_string_to_string_correction_empty_strings() {
+    // Both empty, bound_k=0 → trivially satisfied
+    let problem = StringToStringCorrection::new(0, vec![], vec![], 0);
+    assert!(problem.evaluate(&[]));
+}
+
+#[test]
+fn test_string_to_string_correction_delete_only() {
+    // source [0,1,2], target [0,2], bound 1
+    // Delete index 1: op=1, current_len=3, 1<3 → delete → [0,2] = target
+    let problem = StringToStringCorrection::new(3, vec![0, 1, 2], vec![0, 2], 1);
+    assert!(problem.evaluate(&[1]));
+
+    let solver = BruteForce::new();
+    let solution = solver
+        .find_satisfying(&problem)
+        .expect("should find a solution");
+    assert!(problem.evaluate(&solution));
+}
+
+#[test]
+fn test_string_to_string_correction_rejects_target_longer_than_source() {
+    let problem = StringToStringCorrection::new(3, vec![0, 1], vec![0, 1, 2], 1);
+    assert!(!problem.evaluate(&[4]));
+}
+
+#[test]
+fn test_string_to_string_correction_rejects_excessive_deletions_requirement() {
+    let problem = StringToStringCorrection::new(4, vec![0, 1, 2, 3], vec![0], 2);
+    assert!(!problem.evaluate(&[8, 8]));
+}
+
+#[test]
+fn test_string_to_string_correction_is_available_in_prelude() {
+    let problem = crate::prelude::StringToStringCorrection::new(2, vec![0], vec![0], 0);
+    assert!(problem.evaluate(&[]));
+}