Merge branch 'main' into fix/strong-connectivity-augmentation-example

Regenerate examples.json fixture after merge.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: isPANN

docs/paper/reductions.typ

@@ -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},
@@ -577,6 +597,17 @@ @article{maier1978
   doi     = {10.1145/322063.322075}
 }
 
+@article{wagnerfischer1974,
+  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{blum2021,
   author  = {Christian Blum and Maria J. Blesa and Borja Calvo},
   title   = {{ILP}-based reduced variable neighborhood search for the longest common subsequence problem},
@@ -690,6 +721,17 @@ @article{lucchesi1978
   doi     = {10.1112/jlms/s2-17.3.369}
 }
 
+@article{lucchesi1978keys,
+  author  = {Cl\'audio L. Lucchesi and Sylvia L. Osborn},
+  title   = {Candidate Keys for Relations},
+  journal = {Journal of Computer and System Sciences},
+  volume  = {17},
+  number  = {2},
+  pages   = {270--279},
+  year    = {1978},
+  doi     = {10.1016/0022-0000(78)90009-0}
+}
+
 @article{lenstra1976,
   author  = {Jan Karel Lenstra and Alexander H. G. Rinnooy Kan},
   title   = {On General Routing Problems},
@@ -755,3 +797,25 @@ @article{papadimitriou1982
   year    = {1982},
   doi     = {10.1145/322307.322309}
 }
+
+@article{kou1977,
+  author  = {Lawrence T. Kou},
+  title   = {Polynomial Complete Consecutive Information Retrieval Problems},
+  journal = {SIAM Journal on Computing},
+  volume  = {6},
+  number  = {1},
+  pages   = {67--75},
+  year    = {1977},
+  doi     = {10.1137/0206005}
+}
+
+@article{boothlueker1976,
+  author  = {Kellogg S. Booth and George S. Lueker},
+  title   = {Testing for the Consecutive Ones Property, Interval Graphs, and Graph Planarity Using {PQ}-Tree Algorithms},
+  journal = {Journal of Computer and System Sciences},
+  volume  = {13},
+  number  = {3},
+  pages   = {335--379},
+  year    = {1976},
+  doi     = {10.1016/S0022-0000(76)80045-1}
+}

docs/paper/references.bib

@@ -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 -
 ```
 
@@ -351,7 +352,9 @@ pred create LengthBoundedDisjointPaths --graph 0-1,1-6,0-2,2-3,3-6,0-4,4-5,5-6 -
 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 MinimumCardinalityKey --num-attributes 6 --dependencies "0,1>2;0,2>3;1,3>4;2,4>5" --k 2 -o mck.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 +378,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 -
 ```
 
@@ -516,10 +520,17 @@ Source evaluation: Valid(2)
 
 > **Note:** The ILP solver requires a reduction path from the target problem to ILP.
 > Some problems do not currently have one. Examples include BoundedComponentSpanningForest,
-> LengthBoundedDisjointPaths, QUBO, SpinGlass, MaxCut, CircuitSAT, and MultiprocessorScheduling.
+> LengthBoundedDisjointPaths, MinimumCardinalityKey, QUBO, SpinGlass, MaxCut, CircuitSAT, and MultiprocessorScheduling.
 > Use `pred solve <file> --solver brute-force` for these, or reduce to a problem that supports ILP first.
 > For other problems, use `pred path <PROBLEM> ILP` to check whether an ILP reduction path exists.
 
+For example, the canonical Minimum Cardinality Key instance can be created and solved with:
+
+```bash
+pred create MinimumCardinalityKey --num-attributes 6 --dependencies "0,1>2;0,2>3;1,3>4;2,4>5" --k 2 -o mck.json
+pred solve mck.json --solver brute-force
+```
+
 ## Shell Completions
 
 Enable tab completion by adding one line to your shell config:

docs/src/cli.md

@@ -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
 
@@ -237,6 +238,7 @@ Flags by problem type:
   ComparativeContainment          --universe, --r-sets, --s-sets [--r-weights] [--s-weights]
   X3C (ExactCoverBy3Sets)         --universe, --sets (3 elements each)
   SetBasis                        --universe, --sets, --k
+  MinimumCardinalityKey           --num-attributes, --dependencies, --k
   BicliqueCover                   --left, --right, --biedges, --k
   BalancedCompleteBipartiteSubgraph --left, --right, --biedges, --k
   BiconnectivityAugmentation      --graph, --potential-edges, --budget [--num-vertices]
@@ -249,14 +251,15 @@ Flags by problem type:
   RuralPostman (RPP)              --graph, --edge-weights, --required-edges, --bound
   MultipleChoiceBranching         --arcs [--weights] --partition --bound [--num-vertices]
   SubgraphIsomorphism             --graph (host), --pattern (pattern)
-  LCS                             --strings
+  LCS                             --strings, --bound [--alphabet-size]
   FAS                             --arcs [--weights] [--num-vertices]
   FVS                             --arcs [--weights] [--num-vertices]
   StrongConnectivityAugmentation  --arcs, --candidate-arcs, --bound [--num-vertices]
   FlowShopScheduling              --task-lengths, --deadline [--num-processors]
   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 +278,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
@@ -283,7 +287,8 @@ Examples:
   pred create FVS --arcs \"0>1,1>2,2>0\" --weights 1,1,1
   pred create UndirectedTwoCommodityIntegralFlow --graph 0-2,1-2,2-3 --capacities 1,1,2 --source-1 0 --sink-1 3 --source-2 1 --sink-2 3 --requirement-1 1 --requirement-2 1
   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\"
-  pred create SetBasis --universe 4 --sets \"0,1;1,2;0,2;0,1,2\" --k 3")]
+  pred create SetBasis --universe 4 --sets \"0,1;1,2;0,2;0,1,2\" --k 3
+  pred create MinimumCardinalityKey --num-attributes 6 --dependencies \"0,1>2;0,2>3;1,3>4;2,4>5\" --k 2")]
 pub struct CreateArgs {
     /// Problem type (e.g., MIS, QUBO, SAT). Omit when using --example.
     #[arg(value_parser = crate::problem_name::ProblemNameParser)]
@@ -447,13 +452,13 @@ 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, LongestCommonSubsequence, MultipleChoiceBranching, OptimalLinearArrangement, RuralPostman, ShortestCommonSupersequence, 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)
     #[arg(long)]
     pub pattern: Option<String>,
-    /// Input strings for LCS (e.g., "ABAC;BACA") or SCS (e.g., "0,1,2;1,2,0")
+    /// Input strings for LCS (e.g., "ABAC;BACA" or "0,1,0;1,0,1") or SCS (e.g., "0,1,2;1,2,0")
     #[arg(long)]
     pub strings: Option<String>,
     /// Directed arcs for directed graph problems (e.g., 0>1,1>2,2>0)
@@ -468,7 +473,7 @@ pub struct CreateArgs {
     /// Candidate weighted arcs for StrongConnectivityAugmentation (e.g., 2>0:1,2>1:3)
     #[arg(long)]
     pub candidate_arcs: Option<String>,
-    /// Deadlines for MinimumTardinessSequencing (comma-separated, e.g., "5,5,5,3,3")
+    /// Deadlines for scheduling problems (comma-separated, e.g., "5,5,5,3,3")
     #[arg(long)]
     pub deadlines: Option<String>,
     /// Precedence pairs for MinimumTardinessSequencing (e.g., "0>3,1>3,1>4,2>4")
@@ -492,9 +497,21 @@ 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 LCS, SCS, or StringToStringCorrection (optional; inferred from the input strings if omitted)
     #[arg(long)]
     pub alphabet_size: Option<usize>,
+    /// Functional dependencies for MinimumCardinalityKey (semicolon-separated "lhs>rhs" pairs, e.g., "0,1>2;0,2>3")
+    #[arg(long)]
+    pub dependencies: Option<String>,
+    /// Number of attributes for MinimumCardinalityKey
+    #[arg(long)]
+    pub num_attributes: 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 +521,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 +536,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