diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ
index e027882dc..80a0a4d00 100644
--- a/docs/paper/reductions.typ
+++ b/docs/paper/reductions.typ
@@ -2190,13 +2190,60 @@ NP-completeness was established by Garey, Johnson, and Stockmeyer @gareyJohnsonS
   *Example.* Consider host graph $G$ with 7 vertices: a $K_4$ clique on ${0, 1, 2, 3}$ and a triangle on ${4, 5, 6}$ connected via edge $(3, 4)$. Pattern $H = K_4$ with vertices ${a, b, c, d}$. The mapping $f(a) = 0, f(b) = 1, f(c) = 2, f(d) = 3$ preserves all 6 edges of $K_4$, confirming a subgraph isomorphism exists.
 ]
 
-#problem-def("LongestCommonSubsequence")[
-  Given $k$ strings $s_1, dots, s_k$ over a finite alphabet $Sigma$, find a longest string $w$ that is a subsequence of every $s_i$. A string $w$ is a _subsequence_ of $s$ if $w$ can be obtained by deleting zero or more characters from $s$ without changing the order of the remaining characters.
-][
-  The LCS problem is polynomial-time solvable for $k = 2$ strings via dynamic programming in $O(n_1 n_2)$ time (Wagner & Fischer, 1974), but NP-hard for $k gt.eq 3$ strings @maier1978. It is a foundational problem in bioinformatics (sequence alignment), version control (diff algorithms), and data compression. The problem is listed as SR10 in Garey & Johnson @garey1979.
+#{
+  let x = load-model-example("LongestCommonSubsequence")
+  let strings = x.instance.strings
+  let witness = x.samples.at(0).config
+  let fmt-str(s) = "\"" + s.map(c => str(c)).join("") + "\""
+  let string-list = strings.map(fmt-str).join(", ")
+  let find-embed(target, candidate) = {
+    let positions = ()
+    let j = 0
+    for (i, ch) in target.enumerate() {
+      if j < candidate.len() and ch == candidate.at(j) {
+        positions.push(i)
+        j += 1
+      }
+    }
+    positions
+  }
+  let embeds = strings.map(s => find-embed(s, witness))
+  [
+    #problem-def("LongestCommonSubsequence")[
+      Given a finite alphabet $Sigma$, a set $R = {r_1, dots, r_m}$ of strings over $Sigma^*$, and a positive integer $K$, determine whether there exists a string $w in Sigma^*$ with $|w| gt.eq K$ such that every string $r_i in R$ contains $w$ as a _subsequence_: there exist indices $1 lt.eq j_1 < j_2 < dots < j_(|w|) lt.eq |r_i|$ with $r_i[j_t] = w[t]$ for all $t$.
+    ][
+      A classic NP-complete string problem, listed as problem SR10 in Garey and Johnson @garey1979. #cite(<maier1978>, form: "prose") proved NP-completeness, while Garey and Johnson note polynomial-time cases for fixed $K$ or fixed $|R|$. For the special case of two strings, the classical dynamic-programming algorithm of #cite(<wagnerfischer1974>, form: "prose") runs in $O(|r_1| dot |r_2|)$ time. The decision model implemented in this repository fixes the witness length to exactly $K$; this is equivalent to the standard "$|w| gt.eq K$" formulation because any longer common subsequence has a length-$K$ prefix.
 
-  *Example.* Let $s_1 = $ `ABAC` and $s_2 = $ `BACA` over $Sigma = {A, B, C}$. The longest common subsequence has length 3, e.g., `BAC`: positions 1, 2, 3 of $s_1$ match positions 0, 1, 2 of $s_2$.
-]
+      *Example.* Let $Sigma = {0, 1}$ and let the input set $R$ contain the strings #string-list. The witness $w = $ #fmt-str(witness) is a common subsequence of every string in $R$.
+
+      #figure({
+        let blue = graph-colors.at(0)
+        align(center, stack(dir: ttb, spacing: 0.35cm,
+          stack(dir: ltr, spacing: 0pt,
+            box(width: 1.2cm, height: 0.45cm, align(center + horizon, text(8pt, "w ="))),
+            ..witness.enumerate().map(((i, symbol)) => {
+              box(width: 0.48cm, height: 0.48cm, fill: blue.transparentize(70%), stroke: 0.5pt + luma(120),
+                align(center + horizon, text(9pt, weight: "bold", str(symbol))))
+            }),
+          ),
+          ..strings.enumerate().map(((ri, s)) => {
+            let embed = embeds.at(ri)
+            stack(dir: ltr, spacing: 0pt,
+              box(width: 1.2cm, height: 0.45cm, align(center + horizon, text(8pt, "r" + str(ri + 1) + " ="))),
+              ..s.enumerate().map(((i, symbol)) => {
+                let fill = if embed.contains(i) { blue.transparentize(78%) } else { white }
+                box(width: 0.48cm, height: 0.48cm, fill: fill, stroke: 0.5pt + luma(120),
+                  align(center + horizon, text(9pt, weight: "bold", str(symbol))))
+              }),
+            )
+          }),
+        ))
+      })
+
+      The highlighted positions show one left-to-right embedding of $w = $ #fmt-str(witness) in each input string, certifying the YES answer for $K = 3$.
+    ]
+  ]
+}
 
 #problem-def("SubsetSum")[
   Given a finite set $A = {a_0, dots, a_(n-1)}$ with sizes $s(a_i) in ZZ^+$ and a target $B in ZZ^+$, determine whether there exists a subset $A' subset.eq A$ such that $sum_(a in A') s(a) = B$.
@@ -3585,19 +3632,19 @@ The following reductions to Integer Linear Programming are straightforward formu
 ]
 
 #reduction-rule("LongestCommonSubsequence", "ILP")[
-  The match-pair ILP formulation @blum2021 encodes subsequence alignment as a binary optimization. For two strings $s_1$ (length $n_1$) and $s_2$ (length $n_2$), each position pair $(j_1, j_2)$ where $s_1[j_1] = s_2[j_2]$ yields a binary variable. Constraints enforce one-to-one matching and order preservation (no crossings). The objective maximizes the number of matched pairs.
+  A bounded-witness ILP formulation turns the decision version of LCS into a feasibility problem. Binary variables choose the symbol at each witness position and, for every input string, choose where that witness position is realized. Linear constraints enforce symbol consistency and strictly increasing source positions.
 ][
-  _Construction._ Given strings $s_1$ and $s_2$:
+  _Construction._ Given alphabet $Sigma$, strings $R = {r_1, dots, r_m}$, and bound $K$:
 
-  _Variables:_ Binary $m_(j_1, j_2) in {0, 1}$ for each $(j_1, j_2)$ with $s_1[j_1] = s_2[j_2]$. Interpretation: $m_(j_1, j_2) = 1$ iff position $j_1$ of $s_1$ is matched to position $j_2$ of $s_2$.
+  _Variables:_ Binary $x_(p, a) in {0, 1}$ for witness position $p in {1, dots, K}$ and symbol $a in Sigma$, with $x_(p, a) = 1$ iff the $p$-th witness symbol equals $a$. For every input string $r_i$, witness position $p$, and source index $j in {1, dots, |r_i|}$, binary $y_(i, p, j) = 1$ iff the $p$-th witness symbol is matched to position $j$ of $r_i$.
 
-  _Constraints:_ (1) Each position in $s_1$ matched at most once: $sum_(j_2 : (j_1, j_2) in M) m_(j_1, j_2) lt.eq 1$ for all $j_1$. (2) Each position in $s_2$ matched at most once: $sum_(j_1 : (j_1, j_2) in M) m_(j_1, j_2) lt.eq 1$ for all $j_2$. (3) No crossings: for $(j_1, j_2), (j'_1, j'_2) in M$ with $j_1 < j'_1$ and $j_2 > j'_2$: $m_(j_1, j_2) + m_(j'_1, j'_2) lt.eq 1$.
+  _Constraints:_ (1) Exactly one symbol per witness position: $sum_(a in Sigma) x_(p, a) = 1$ for all $p$. (2) Exactly one matched source position for each $(i, p)$: $sum_(j = 1)^(|r_i|) y_(i, p, j) = 1$. (3) Character consistency: if $r_i[j] = a$, then $y_(i, p, j) lt.eq x_(p, a)$. (4) Strictly increasing matches: for consecutive witness positions $p$ and $p + 1$, forbid $y_(i, p, j') = y_(i, p + 1, j) = 1$ whenever $j' gt.eq j$.
 
-  _Objective:_ Maximize $sum_((j_1, j_2) in M) m_(j_1, j_2)$.
+  _Objective:_ Use the zero objective. The target ILP is feasible iff the source LCS instance is a YES instance.
 
-  _Correctness._ ($arrow.r.double$) A common subsequence of length $ell$ defines $ell$ matched pairs that are order-preserving (no crossings) and one-to-one, yielding a feasible ILP solution with objective $ell$. ($arrow.l.double$) An ILP solution with objective $ell$ defines $ell$ matched pairs; constraints (1)--(2) ensure one-to-one matching, and constraint (3) ensures order preservation, so the matched characters form a common subsequence of length $ell$.
+  _Correctness._ ($arrow.r.double$) If a witness $w = w_1 dots w_K$ is a common subsequence of every string, set $x_(p, w_p) = 1$ and choose, in every $r_i$, the positions where that embedding occurs. Constraints (1)--(4) are satisfied, so the ILP is feasible. ($arrow.l.double$) Any feasible ILP solution selects exactly one symbol for each witness position and exactly one realization in each source string. Character consistency ensures the chosen positions spell the same witness string in every input string, and the ordering constraints ensure those positions are strictly increasing. Therefore the extracted witness is a common subsequence of length $K$.
 
-  _Solution extraction._ Collect pairs $(j_1, j_2)$ with $m_(j_1, j_2) = 1$, sort by $j_1$, and read the characters.
+  _Solution extraction._ For each witness position $p$, read the unique symbol $a$ with $x_(p, a) = 1$ and output the resulting length-$K$ string.
 ]
 
 == Unit Disk Mapping
diff --git a/docs/paper/references.bib b/docs/paper/references.bib
index 526068c65..0585a73df 100644
--- a/docs/paper/references.bib
+++ b/docs/paper/references.bib
@@ -597,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},
diff --git a/problemreductions-cli/src/cli.rs b/problemreductions-cli/src/cli.rs
index 48f367000..d3099362a 100644
--- a/problemreductions-cli/src/cli.rs
+++ b/problemreductions-cli/src/cli.rs
@@ -251,7 +251,7 @@ 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]
@@ -452,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, SCS, or StringToStringCorrection)
+    /// 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)
@@ -497,7 +497,7 @@ pub struct CreateArgs {
     /// Number of available workers for StaffScheduling
     #[arg(long)]
     pub num_workers: Option<u64>,
-    /// Alphabet size for SCS or StringToStringCorrection (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")
diff --git a/problemreductions-cli/src/commands/create.rs b/problemreductions-cli/src/commands/create.rs
index e5e865f85..5b96722cb 100644
--- a/problemreductions-cli/src/commands/create.rs
+++ b/problemreductions-cli/src/commands/create.rs
@@ -332,6 +332,9 @@ fn example_for(canonical: &str, graph_type: Option<&str>) -> &'static str {
             "--universe 4 --r-sets \"0,1,2,3;0,1\" --s-sets \"0,1,2,3;2,3\" --r-weights 2,5 --s-weights 3,6"
         }
         "SetBasis" => "--universe 4 --sets \"0,1;1,2;0,2;0,1,2\" --k 3",
+        "LongestCommonSubsequence" => {
+            "--strings \"010110;100101;001011\" --bound 3 --alphabet-size 2"
+        }
         "MinimumCardinalityKey" => {
             "--num-attributes 6 --dependencies \"0,1>2;0,2>3;1,3>4;2,4>5\" --k 2"
         }
@@ -377,6 +380,10 @@ fn help_flag_hint(
 ) -> &'static str {
     match (canonical, field_name) {
         ("BoundedComponentSpanningForest", "max_weight") => "integer",
+        ("LongestCommonSubsequence", "strings") => {
+            "raw strings: \"ABAC;BACA\" or symbol lists: \"0,1,0;1,0,1\""
+        }
+        ("ShortestCommonSupersequence", "strings") => "symbol lists: \"0,1,2;1,2,0\"",
         ("MultipleChoiceBranching", "partition") => "semicolon-separated groups: \"0,1;2,3\"",
         _ => type_format_hint(type_name, graph_type),
     }
@@ -1294,18 +1301,85 @@ pub fn create(args: &CreateArgs, out: &OutputConfig) -> Result<()> {
 
         // LongestCommonSubsequence
         "LongestCommonSubsequence" => {
+            let usage =
+                "Usage: pred create LCS --strings \"010110;100101;001011\" --bound 3 [--alphabet-size 2]";
             let strings_str = args.strings.as_deref().ok_or_else(|| {
-                anyhow::anyhow!(
-                    "LCS requires --strings\n\n\
-                     Usage: pred create LCS --strings \"ABAC;BACA\""
-                )
+                anyhow::anyhow!("LongestCommonSubsequence requires --strings\n\n{usage}")
             })?;
-            let strings: Vec<Vec<u8>> = strings_str
-                .split(';')
-                .map(|s| s.trim().as_bytes().to_vec())
-                .collect();
+            let bound_i64 = args.bound.ok_or_else(|| {
+                anyhow::anyhow!("LongestCommonSubsequence requires --bound\n\n{usage}")
+            })?;
+            anyhow::ensure!(
+                bound_i64 >= 0,
+                "LongestCommonSubsequence requires a nonnegative --bound, got {}",
+                bound_i64
+            );
+            let bound = bound_i64 as usize;
+
+            let segments: Vec<&str> = strings_str.split(';').map(str::trim).collect();
+            let comma_mode = segments.iter().any(|segment| segment.contains(','));
+
+            let (strings, inferred_alphabet_size): (Vec<Vec<usize>>, usize) = if comma_mode {
+                let strings = segments
+                    .iter()
+                    .map(|segment| {
+                        if segment.is_empty() {
+                            return Ok(Vec::new());
+                        }
+                        segment
+                            .split(',')
+                            .map(|value| {
+                                value.trim().parse::<usize>().map_err(|e| {
+                                    anyhow::anyhow!("Invalid LCS alphabet index: {}", e)
+                                })
+                            })
+                            .collect::<Result<Vec<_>>>()
+                    })
+                    .collect::<Result<Vec<_>>>()?;
+                let inferred = strings
+                    .iter()
+                    .flat_map(|string| string.iter())
+                    .copied()
+                    .max()
+                    .map(|value| value + 1)
+                    .unwrap_or(0);
+                (strings, inferred)
+            } else {
+                let mut encoding = BTreeMap::new();
+                let mut next_symbol = 0usize;
+                let strings = segments
+                    .iter()
+                    .map(|segment| {
+                        segment
+                            .as_bytes()
+                            .iter()
+                            .map(|byte| {
+                                let entry = encoding.entry(*byte).or_insert_with(|| {
+                                    let current = next_symbol;
+                                    next_symbol += 1;
+                                    current
+                                });
+                                *entry
+                            })
+                            .collect::<Vec<_>>()
+                    })
+                    .collect::<Vec<_>>();
+                (strings, next_symbol)
+            };
+
+            let alphabet_size = args.alphabet_size.unwrap_or(inferred_alphabet_size);
+            anyhow::ensure!(
+                alphabet_size >= inferred_alphabet_size,
+                "--alphabet-size {} is smaller than the inferred alphabet size ({})",
+                alphabet_size,
+                inferred_alphabet_size
+            );
+            anyhow::ensure!(
+                alphabet_size > 0 || (bound == 0 && strings.iter().all(|string| string.is_empty())),
+                "LongestCommonSubsequence requires a positive alphabet. Provide --alphabet-size when all strings are empty and --bound > 0.\n\n{usage}"
+            );
             (
-                ser(LongestCommonSubsequence::new(strings))?,
+                ser(LongestCommonSubsequence::new(alphabet_size, strings, bound))?,
                 resolved_variant.clone(),
             )
         }
@@ -3089,6 +3163,7 @@ fn create_random(
 #[cfg(test)]
 mod tests {
     use super::create;
+    use super::help_flag_hint;
     use super::help_flag_name;
     use super::parse_bool_rows;
     use super::problem_help_flag_name;
@@ -3118,6 +3193,19 @@ mod tests {
         );
     }
 
+    #[test]
+    fn test_problem_help_uses_problem_specific_lcs_strings_hint() {
+        assert_eq!(
+            help_flag_hint(
+                "LongestCommonSubsequence",
+                "strings",
+                "Vec<Vec<usize>>",
+                None,
+            ),
+            "raw strings: \"ABAC;BACA\" or symbol lists: \"0,1,0;1,0,1\""
+        );
+    }
+
     #[test]
     fn test_problem_help_uses_string_to_string_correction_cli_flags() {
         assert_eq!(
@@ -3134,6 +3222,14 @@ mod tests {
         );
     }
 
+    #[test]
+    fn test_problem_help_keeps_generic_vec_vec_usize_hint_for_other_models() {
+        assert_eq!(
+            help_flag_hint("SetBasis", "sets", "Vec<Vec<usize>>", None),
+            "semicolon-separated sets: \"0,1;1,2;0,2\""
+        );
+    }
+
     #[test]
     fn test_problem_help_uses_k_for_staff_scheduling() {
         assert_eq!(
diff --git a/problemreductions-cli/tests/cli_tests.rs b/problemreductions-cli/tests/cli_tests.rs
index bffb1a1b7..1a94f07e2 100644
--- a/problemreductions-cli/tests/cli_tests.rs
+++ b/problemreductions-cli/tests/cli_tests.rs
@@ -2837,6 +2837,46 @@ fn test_create_set_basis_no_flags_uses_actual_cli_flag_names() {
     );
 }
 
+#[test]
+fn test_create_lcs_with_raw_strings_infers_alphabet() {
+    let output = pred()
+        .args(["create", "LCS", "--strings", "ABAC;BACA", "--bound", "2"])
+        .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"], "LongestCommonSubsequence");
+    assert_eq!(json["data"]["alphabet_size"], 3);
+    assert_eq!(json["data"]["bound"], 2);
+    assert_eq!(
+        json["data"]["strings"],
+        serde_json::json!([[0, 1, 0, 2], [1, 0, 2, 0]])
+    );
+}
+
+#[test]
+fn test_create_lcs_rejects_empty_strings_with_positive_bound_without_panicking() {
+    let output = pred()
+        .args(["create", "LCS", "--strings", "", "--bound", "1"])
+        .output()
+        .unwrap();
+    assert!(!output.status.success());
+    let stderr = String::from_utf8_lossy(&output.stderr);
+    assert!(
+        stderr.contains("Provide --alphabet-size when all strings are empty and --bound > 0"),
+        "expected user-facing validation error, got: {stderr}"
+    );
+    assert!(
+        !stderr.contains("panicked at"),
+        "create command should reject invalid LCS input without panicking: {stderr}"
+    );
+}
+
 #[test]
 fn test_create_kcoloring_missing_k() {
     let output = pred()
diff --git a/src/example_db/fixtures/examples.json b/src/example_db/fixtures/examples.json
index 9248c8292..bc223618e 100644
--- a/src/example_db/fixtures/examples.json
+++ b/src/example_db/fixtures/examples.json
@@ -17,6 +17,7 @@
     {"problem":"KColoring","variant":{"graph":"SimpleGraph","k":"K3"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,2,null],[1,3,null],[2,3,null],[2,4,null],[3,4,null]],"node_holes":[],"nodes":[null,null,null,null,null]}},"num_colors":3},"samples":[{"config":[0,1,1,0,2],"metric":true}],"optimal":[{"config":[0,1,1,0,2],"metric":true},{"config":[0,1,1,2,0],"metric":true},{"config":[0,1,2,0,1],"metric":true},{"config":[0,2,1,0,2],"metric":true},{"config":[0,2,2,0,1],"metric":true},{"config":[0,2,2,1,0],"metric":true},{"config":[1,0,0,1,2],"metric":true},{"config":[1,0,0,2,1],"metric":true},{"config":[1,0,2,1,0],"metric":true},{"config":[1,2,0,1,2],"metric":true},{"config":[1,2,2,0,1],"metric":true},{"config":[1,2,2,1,0],"metric":true},{"config":[2,0,0,1,2],"metric":true},{"config":[2,0,0,2,1],"metric":true},{"config":[2,0,1,2,0],"metric":true},{"config":[2,1,0,2,1],"metric":true},{"config":[2,1,1,0,2],"metric":true},{"config":[2,1,1,2,0],"metric":true}]},
     {"problem":"KSatisfiability","variant":{"k":"K3"},"instance":{"clauses":[{"literals":[1,2,3]},{"literals":[-1,-2,3]},{"literals":[1,-2,-3]}],"num_vars":3},"samples":[{"config":[1,0,1],"metric":true}],"optimal":[{"config":[0,0,1],"metric":true},{"config":[0,1,0],"metric":true},{"config":[1,0,0],"metric":true},{"config":[1,0,1],"metric":true},{"config":[1,1,1],"metric":true}]},
     {"problem":"LengthBoundedDisjointPaths","variant":{"graph":"SimpleGraph"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[1,6,null],[0,2,null],[2,3,null],[3,6,null],[0,4,null],[4,5,null],[5,6,null]],"node_holes":[],"nodes":[null,null,null,null,null,null,null]}},"max_length":3,"num_paths_required":2,"sink":6,"source":0},"samples":[{"config":[1,1,0,0,0,0,1,1,0,1,1,0,0,1],"metric":true}],"optimal":[{"config":[1,0,0,0,1,1,1,1,0,1,1,0,0,1],"metric":true},{"config":[1,0,0,0,1,1,1,1,1,0,0,0,0,1],"metric":true},{"config":[1,0,1,1,0,0,1,1,0,0,0,1,1,1],"metric":true},{"config":[1,0,1,1,0,0,1,1,1,0,0,0,0,1],"metric":true},{"config":[1,1,0,0,0,0,1,1,0,0,0,1,1,1],"metric":true},{"config":[1,1,0,0,0,0,1,1,0,1,1,0,0,1],"metric":true}]},
+    {"problem":"LongestCommonSubsequence","variant":{},"instance":{"alphabet_size":2,"bound":3,"strings":[[0,1,0,1,1,0],[1,0,0,1,0,1],[0,0,1,0,1,1],[1,1,0,0,1,0],[0,1,0,1,0,1],[1,0,1,0,1,0]]},"samples":[{"config":[0,1,0],"metric":true}],"optimal":[{"config":[0,0,0],"metric":true},{"config":[0,0,1],"metric":true},{"config":[0,1,0],"metric":true},{"config":[1,0,1],"metric":true},{"config":[1,1,1],"metric":true}]},
     {"problem":"MaxCut","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"edge_weights":[1,1,1,1,1,1],"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,2,null],[1,3,null],[2,3,null],[2,4,null],[3,4,null]],"node_holes":[],"nodes":[null,null,null,null,null]}}},"samples":[{"config":[1,0,0,1,0],"metric":{"Valid":5}}],"optimal":[{"config":[0,1,1,0,0],"metric":{"Valid":5}},{"config":[0,1,1,0,1],"metric":{"Valid":5}},{"config":[1,0,0,1,0],"metric":{"Valid":5}},{"config":[1,0,0,1,1],"metric":{"Valid":5}}]},
     {"problem":"MaximalIS","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[1,2,null],[2,3,null],[3,4,null]],"node_holes":[],"nodes":[null,null,null,null,null]}},"weights":[1,1,1,1,1]},"samples":[{"config":[0,1,0,1,0],"metric":{"Valid":2}},{"config":[1,0,1,0,1],"metric":{"Valid":3}}],"optimal":[{"config":[1,0,1,0,1],"metric":{"Valid":3}}]},
     {"problem":"MaximumClique","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,2,null],[1,3,null],[2,3,null],[2,4,null],[3,4,null]],"node_holes":[],"nodes":[null,null,null,null,null]}},"weights":[1,1,1,1,1]},"samples":[{"config":[0,0,1,1,1],"metric":{"Valid":3}}],"optimal":[{"config":[0,0,1,1,1],"metric":{"Valid":3}}]},
@@ -59,18 +60,18 @@
     {"source":{"problem":"KColoring","variant":{"graph":"SimpleGraph","k":"KN"},"instance":{"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]}},"num_colors":3}},"target":{"problem":"ILP","variant":{"variable":"bool"},"instance":{"constraints":[{"cmp":"Eq","rhs":1.0,"terms":[[0,1.0],[1,1.0],[2,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[3,1.0],[4,1.0],[5,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[6,1.0],[7,1.0],[8,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[9,1.0],[10,1.0],[11,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[12,1.0],[13,1.0],[14,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[15,1.0],[16,1.0],[17,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[18,1.0],[19,1.0],[20,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[21,1.0],[22,1.0],[23,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[24,1.0],[25,1.0],[26,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[27,1.0],[28,1.0],[29,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[0,1.0],[3,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[1,1.0],[4,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[2,1.0],[5,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[0,1.0],[12,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[1,1.0],[13,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[2,1.0],[14,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[0,1.0],[15,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[1,1.0],[16,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[2,1.0],[17,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[3,1.0],[6,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[4,1.0],[7,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[5,1.0],[8,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[3,1.0],[18,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[4,1.0],[19,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[5,1.0],[20,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[6,1.0],[9,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[7,1.0],[10,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[8,1.0],[11,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[6,1.0],[21,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[7,1.0],[22,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[8,1.0],[23,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[9,1.0],[12,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[10,1.0],[13,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[11,1.0],[14,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[9,1.0],[24,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[10,1.0],[25,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[11,1.0],[26,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[12,1.0],[27,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[13,1.0],[28,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[14,1.0],[29,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[15,1.0],[21,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[16,1.0],[22,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[17,1.0],[23,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[15,1.0],[24,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[16,1.0],[25,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[17,1.0],[26,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[18,1.0],[24,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[19,1.0],[25,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[20,1.0],[26,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[18,1.0],[27,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[19,1.0],[28,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[20,1.0],[29,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[21,1.0],[27,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[22,1.0],[28,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[23,1.0],[29,1.0]]}],"num_vars":30,"objective":[],"sense":"Minimize"}},"solutions":[{"source_config":[0,2,0,1,2,1,1,2,0,0],"target_config":[1,0,0,0,0,1,1,0,0,0,1,0,0,0,1,0,1,0,0,1,0,0,0,1,1,0,0,1,0,0]}]},
     {"source":{"problem":"KColoring","variant":{"graph":"SimpleGraph","k":"KN"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,2,null],[1,3,null],[2,3,null],[2,4,null],[3,4,null]],"node_holes":[],"nodes":[null,null,null,null,null]}},"num_colors":3}},"target":{"problem":"QUBO","variant":{"weight":"f64"},"instance":{"matrix":[[-6.0,12.0,12.0,3.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,-6.0,12.0,0.0,3.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,-6.0,0.0,0.0,3.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,-6.0,12.0,12.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,-6.0,12.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,-6.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,-6.0,12.0,12.0,3.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,-6.0,12.0,0.0,3.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,-6.0,0.0,0.0,3.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,-6.0,12.0,12.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,-6.0,12.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,-6.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,-6.0,12.0,12.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,0.0,-6.0,12.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,0.0,0.0,-6.0]],"num_vars":15}},"solutions":[{"source_config":[1,2,2,1,0],"target_config":[0,1,0,0,0,1,0,0,1,0,1,0,1,0,0]}]},
     {"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,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":[0,0,0,0,0],"target_config":[0,0,0,0,0,1,0,0,0,0,0,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,1],"target_config":[1,1,1,1]}]},
+    {"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":"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]}]},
+    {"source":{"problem":"LongestCommonSubsequence","variant":{},"instance":{"alphabet_size":3,"bound":2,"strings":[[0,1,2],[1,0,2]]}},"target":{"problem":"ILP","variant":{"variable":"bool"},"instance":{"constraints":[{"cmp":"Eq","rhs":1.0,"terms":[[0,1.0],[1,1.0],[2,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[3,1.0],[4,1.0],[5,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[6,1.0],[7,1.0],[8,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[12,1.0],[13,1.0],[14,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[9,1.0],[10,1.0],[11,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[15,1.0],[16,1.0],[17,1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[6,1.0],[0,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[7,1.0],[1,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[8,1.0],[2,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[12,1.0],[3,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[13,1.0],[4,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[14,1.0],[5,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[9,1.0],[1,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[10,1.0],[0,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[11,1.0],[2,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[15,1.0],[4,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[16,1.0],[3,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[17,1.0],[5,-1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[6,1.0],[12,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[7,1.0],[12,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[7,1.0],[13,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[8,1.0],[12,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[8,1.0],[13,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[8,1.0],[14,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[9,1.0],[15,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[10,1.0],[15,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[10,1.0],[16,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[11,1.0],[15,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[11,1.0],[16,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[11,1.0],[17,1.0]]}],"num_vars":18,"objective":[],"sense":"Minimize"}},"solutions":[{"source_config":[0,2],"target_config":[1,0,0,0,0,1,1,0,0,0,1,0,0,0,1,0,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":[0,1,0,1,0,1,0,0,0,1],"target_config":[0,1,0,1,0,1,0,0,0,1]}]},
     {"source":{"problem":"MaximumClique","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,2,null],[0,3,null],[0,4,null],[1,2,null],[1,3,null],[1,5,null],[2,4,null],[2,5,null],[3,4,null],[3,5,null],[4,5,null]],"node_holes":[],"nodes":[null,null,null,null,null,null]}},"weights":[1,1,1,1,1,1]}},"target":{"problem":"ILP","variant":{"variable":"bool"},"instance":{"constraints":[{"cmp":"Le","rhs":1.0,"terms":[[0,1.0],[5,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[1,1.0],[4,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[2,1.0],[3,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":[1,1,1,0,0,0],"target_config":[1,1,1,0,0,0]}]},
     {"source":{"problem":"MaximumClique","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[1,2,null],[2,3,null]],"node_holes":[],"nodes":[null,null,null,null]}},"weights":[1,1,1,1]}},"target":{"problem":"MaximumIndependentSet","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,2,null],[0,3,null],[1,3,null]],"node_holes":[],"nodes":[null,null,null,null]}},"weights":[1,1,1,1]}},"solutions":[{"source_config":[0,1,1,0],"target_config":[0,1,1,0]}]},
-    {"source":{"problem":"MaximumIndependentSet","variant":{"graph":"SimpleGraph","weight":"One"},"instance":{"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]}},"weights":[1,1,1,1,1,1,1,1,1,1]}},"target":{"problem":"MaximumSetPacking","variant":{"weight":"One"},"instance":{"sets":[[0,1,2],[0,3,4],[3,5,6],[5,7,8],[1,7,9],[2,10,11],[4,12,13],[6,10,14],[8,11,12],[9,13,14]],"weights":[1,1,1,1,1,1,1,1,1,1]}},"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]}]},
+    {"source":{"problem":"MaximumIndependentSet","variant":{"graph":"SimpleGraph","weight":"One"},"instance":{"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]}},"weights":[1,1,1,1,1,1,1,1,1,1]}},"target":{"problem":"MaximumSetPacking","variant":{"weight":"One"},"instance":{"sets":[[0,1,2],[0,3,4],[3,5,6],[5,7,8],[1,7,9],[2,10,11],[4,12,13],[6,10,14],[8,11,12],[9,13,14]],"weights":[1,1,1,1,1,1,1,1,1,1]}},"solutions":[{"source_config":[1,0,0,1,0,0,1,1,0,0],"target_config":[1,0,0,1,0,0,1,1,0,0]}]},
     {"source":{"problem":"MaximumIndependentSet","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[1,2,null],[2,3,null],[3,4,null]],"node_holes":[],"nodes":[null,null,null,null,null]}},"weights":[1,1,1,1,1]}},"target":{"problem":"MaximumClique","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,2,null],[0,3,null],[0,4,null],[1,3,null],[1,4,null],[2,4,null]],"node_holes":[],"nodes":[null,null,null,null,null]}},"weights":[1,1,1,1,1]}},"solutions":[{"source_config":[1,0,1,0,1],"target_config":[1,0,1,0,1]}]},
-    {"source":{"problem":"MaximumIndependentSet","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"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]}},"weights":[1,1,1,1,1,1,1,1,1,1]}},"target":{"problem":"MaximumSetPacking","variant":{"weight":"i32"},"instance":{"sets":[[0,1,2],[0,3,4],[3,5,6],[5,7,8],[1,7,9],[2,10,11],[4,12,13],[6,10,14],[8,11,12],[9,13,14]],"weights":[1,1,1,1,1,1,1,1,1,1]}},"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]}]},
-    {"source":{"problem":"MaximumIndependentSet","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"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]}},"weights":[1,1,1,1,1,1,1,1,1,1]}},"target":{"problem":"MinimumVertexCover","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"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]}},"weights":[1,1,1,1,1,1,1,1,1,1]}},"solutions":[{"source_config":[1,0,1,0,0,0,0,0,1,1],"target_config":[0,1,0,1,1,1,1,1,0,0]}]},
+    {"source":{"problem":"MaximumIndependentSet","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"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]}},"weights":[1,1,1,1,1,1,1,1,1,1]}},"target":{"problem":"MaximumSetPacking","variant":{"weight":"i32"},"instance":{"sets":[[0,1,2],[0,3,4],[3,5,6],[5,7,8],[1,7,9],[2,10,11],[4,12,13],[6,10,14],[8,11,12],[9,13,14]],"weights":[1,1,1,1,1,1,1,1,1,1]}},"solutions":[{"source_config":[1,0,0,1,0,0,1,1,0,0],"target_config":[1,0,0,1,0,0,1,1,0,0]}]},
+    {"source":{"problem":"MaximumIndependentSet","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"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]}},"weights":[1,1,1,1,1,1,1,1,1,1]}},"target":{"problem":"MinimumVertexCover","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"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]}},"weights":[1,1,1,1,1,1,1,1,1,1]}},"solutions":[{"source_config":[1,0,0,1,0,0,1,1,0,0],"target_config":[0,1,1,0,1,1,0,0,1,1]}]},
     {"source":{"problem":"MaximumMatching","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":"ILP","variant":{"variable":"bool"},"instance":{"constraints":[{"cmp":"Le","rhs":1.0,"terms":[[0,1.0],[1,1.0],[2,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[0,1.0],[3,1.0],[4,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[3,1.0],[5,1.0],[6,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[5,1.0],[7,1.0],[8,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[1,1.0],[7,1.0],[9,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[2,1.0],[10,1.0],[11,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[4,1.0],[12,1.0],[13,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[6,1.0],[10,1.0],[14,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[8,1.0],[11,1.0],[12,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[9,1.0],[13,1.0],[14,1.0]]}],"num_vars":15,"objective":[[0,1.0],[1,1.0],[2,1.0],[3,1.0],[4,1.0],[5,1.0],[6,1.0],[7,1.0],[8,1.0],[9,1.0],[10,1.0],[11,1.0],[12,1.0],[13,1.0],[14,1.0]],"sense":"Maximize"}},"solutions":[{"source_config":[0,0,1,1,0,0,0,1,0,0,0,0,1,0,1],"target_config":[0,0,1,1,0,0,0,1,0,0,0,0,1,0,1]}]},
     {"source":{"problem":"MaximumMatching","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":"MaximumSetPacking","variant":{"weight":"i32"},"instance":{"sets":[[0,1],[0,4],[0,5],[1,2],[1,6],[2,3],[2,7],[3,4],[3,8],[4,9],[5,7],[5,8],[6,8],[6,9],[7,9]],"weights":[1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]}},"solutions":[{"source_config":[0,0,1,1,0,0,0,1,0,0,0,0,1,0,1],"target_config":[0,0,1,1,0,0,0,1,0,0,0,0,1,0,1]}]},
     {"source":{"problem":"MaximumSetPacking","variant":{"weight":"One"},"instance":{"sets":[[0,1,2],[2,3],[4,5,6],[1,5,7],[3,6]],"weights":[1,1,1,1,1]}},"target":{"problem":"MaximumIndependentSet","variant":{"graph":"SimpleGraph","weight":"One"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,3,null],[1,4,null],[2,3,null],[2,4,null]],"node_holes":[],"nodes":[null,null,null,null,null]}},"weights":[1,1,1,1,1]}},"solutions":[{"source_config":[1,0,0,0,1],"target_config":[1,0,0,0,1]}]},
@@ -80,18 +81,18 @@
     {"source":{"problem":"MinimumDominatingSet","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"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]}},"weights":[1,1,1,1,1,1,1,1,1,1]}},"target":{"problem":"ILP","variant":{"variable":"bool"},"instance":{"constraints":[{"cmp":"Ge","rhs":1.0,"terms":[[0,1.0],[5,1.0],[4,1.0],[1,1.0]]},{"cmp":"Ge","rhs":1.0,"terms":[[1,1.0],[6,1.0],[2,1.0],[0,1.0]]},{"cmp":"Ge","rhs":1.0,"terms":[[2,1.0],[7,1.0],[3,1.0],[1,1.0]]},{"cmp":"Ge","rhs":1.0,"terms":[[3,1.0],[8,1.0],[4,1.0],[2,1.0]]},{"cmp":"Ge","rhs":1.0,"terms":[[4,1.0],[9,1.0],[3,1.0],[0,1.0]]},{"cmp":"Ge","rhs":1.0,"terms":[[5,1.0],[8,1.0],[7,1.0],[0,1.0]]},{"cmp":"Ge","rhs":1.0,"terms":[[6,1.0],[9,1.0],[8,1.0],[1,1.0]]},{"cmp":"Ge","rhs":1.0,"terms":[[7,1.0],[9,1.0],[5,1.0],[2,1.0]]},{"cmp":"Ge","rhs":1.0,"terms":[[8,1.0],[6,1.0],[5,1.0],[3,1.0]]},{"cmp":"Ge","rhs":1.0,"terms":[[9,1.0],[7,1.0],[6,1.0],[4,1.0]]}],"num_vars":10,"objective":[[0,1.0],[1,1.0],[2,1.0],[3,1.0],[4,1.0],[5,1.0],[6,1.0],[7,1.0],[8,1.0],[9,1.0]],"sense":"Minimize"}},"solutions":[{"source_config":[0,0,1,0,0,1,0,0,0,1],"target_config":[0,0,1,0,0,1,0,0,0,1]}]},
     {"source":{"problem":"MinimumFeedbackVertexSet","variant":{"weight":"i32"},"instance":{"graph":{"inner":{"edge_property":"directed","edges":[[0,1,null],[1,2,null],[2,0,null]],"node_holes":[],"nodes":[null,null,null]}},"weights":[1,1,1]}},"target":{"problem":"ILP","variant":{"variable":"i32"},"instance":{"constraints":[{"cmp":"Le","rhs":1.0,"terms":[[0,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[1,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[2,1.0]]},{"cmp":"Le","rhs":2.0,"terms":[[3,1.0]]},{"cmp":"Le","rhs":2.0,"terms":[[4,1.0]]},{"cmp":"Le","rhs":2.0,"terms":[[5,1.0]]},{"cmp":"Ge","rhs":1.0,"terms":[[4,1.0],[3,-1.0],[0,3.0],[1,3.0]]},{"cmp":"Ge","rhs":1.0,"terms":[[5,1.0],[4,-1.0],[1,3.0],[2,3.0]]},{"cmp":"Ge","rhs":1.0,"terms":[[3,1.0],[5,-1.0],[2,3.0],[0,3.0]]}],"num_vars":6,"objective":[[0,1.0],[1,1.0],[2,1.0]],"sense":"Minimize"}},"solutions":[{"source_config":[0,1,0],"target_config":[0,1,0,1,0,0]}]},
     {"source":{"problem":"MinimumSetCovering","variant":{"weight":"i32"},"instance":{"sets":[[0,1,2],[2,3,4],[4,5,6],[6,7,0],[1,3,5],[0,4,7]],"universe_size":8,"weights":[1,1,1,1,1,1]}},"target":{"problem":"ILP","variant":{"variable":"bool"},"instance":{"constraints":[{"cmp":"Ge","rhs":1.0,"terms":[[0,1.0],[3,1.0],[5,1.0]]},{"cmp":"Ge","rhs":1.0,"terms":[[0,1.0],[4,1.0]]},{"cmp":"Ge","rhs":1.0,"terms":[[0,1.0],[1,1.0]]},{"cmp":"Ge","rhs":1.0,"terms":[[1,1.0],[4,1.0]]},{"cmp":"Ge","rhs":1.0,"terms":[[1,1.0],[2,1.0],[5,1.0]]},{"cmp":"Ge","rhs":1.0,"terms":[[2,1.0],[4,1.0]]},{"cmp":"Ge","rhs":1.0,"terms":[[2,1.0],[3,1.0]]},{"cmp":"Ge","rhs":1.0,"terms":[[3,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":"Minimize"}},"solutions":[{"source_config":[0,1,0,1,1,0],"target_config":[0,1,0,1,1,0]}]},
-    {"source":{"problem":"MinimumVertexCover","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"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]}},"weights":[1,1,1,1,1,1,1,1,1,1]}},"target":{"problem":"MaximumIndependentSet","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"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]}},"weights":[1,1,1,1,1,1,1,1,1,1]}},"solutions":[{"source_config":[0,1,0,1,1,1,1,1,0,0],"target_config":[1,0,1,0,0,0,0,0,1,1]}]},
-    {"source":{"problem":"MinimumVertexCover","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"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]}},"weights":[1,1,1,1,1,1,1,1,1,1]}},"target":{"problem":"MinimumSetCovering","variant":{"weight":"i32"},"instance":{"sets":[[0,1,2],[0,3,4],[3,5,6],[5,7,8],[1,7,9],[2,10,11],[4,12,13],[6,10,14],[8,11,12],[9,13,14]],"universe_size":15,"weights":[1,1,1,1,1,1,1,1,1,1]}},"solutions":[{"source_config":[0,1,0,1,1,1,1,1,0,0],"target_config":[0,1,0,1,1,1,1,1,0,0]}]},
+    {"source":{"problem":"MinimumVertexCover","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"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]}},"weights":[1,1,1,1,1,1,1,1,1,1]}},"target":{"problem":"MaximumIndependentSet","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"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]}},"weights":[1,1,1,1,1,1,1,1,1,1]}},"solutions":[{"source_config":[0,1,1,0,1,1,0,0,1,1],"target_config":[1,0,0,1,0,0,1,1,0,0]}]},
+    {"source":{"problem":"MinimumVertexCover","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"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]}},"weights":[1,1,1,1,1,1,1,1,1,1]}},"target":{"problem":"MinimumSetCovering","variant":{"weight":"i32"},"instance":{"sets":[[0,1,2],[0,3,4],[3,5,6],[5,7,8],[1,7,9],[2,10,11],[4,12,13],[6,10,14],[8,11,12],[9,13,14]],"universe_size":15,"weights":[1,1,1,1,1,1,1,1,1,1]}},"solutions":[{"source_config":[0,1,1,0,1,1,0,0,1,1],"target_config":[0,1,1,0,1,1,0,0,1,1]}]},
     {"source":{"problem":"QUBO","variant":{"weight":"f64"},"instance":{"matrix":[[-2.0,1.0,0.0,0.0],[0.0,-3.0,2.0,0.0],[0.0,0.0,-1.0,-1.0],[0.0,0.0,0.0,-4.0]],"num_vars":4}},"target":{"problem":"ILP","variant":{"variable":"bool"},"instance":{"constraints":[{"cmp":"Le","rhs":0.0,"terms":[[4,1.0],[0,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[4,1.0],[1,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[4,1.0],[0,-1.0],[1,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[5,1.0],[1,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[5,1.0],[2,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[5,1.0],[1,-1.0],[2,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[6,1.0],[2,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[6,1.0],[3,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[6,1.0],[2,-1.0],[3,-1.0]]}],"num_vars":7,"objective":[[0,-2.0],[1,-3.0],[2,-1.0],[3,-4.0],[4,1.0],[5,2.0],[6,-1.0]],"sense":"Minimize"}},"solutions":[{"source_config":[1,1,1,1],"target_config":[1,1,1,1,1,1,1]}]},
     {"source":{"problem":"QUBO","variant":{"weight":"f64"},"instance":{"matrix":[[-1.0,2.0,0.0,0.0,-1.5,2.0,0.0,0.0,0.0,0.0],[0.0,-0.8,-1.5,0.0,0.0,0.0,2.0,0.0,0.0,0.0],[0.0,0.0,-0.6,-1.5,0.0,0.0,0.0,2.0,0.0,0.0],[0.0,0.0,0.0,-0.3999999999999999,-1.5,0.0,0.0,0.0,2.0,0.0],[0.0,0.0,0.0,0.0,-0.19999999999999996,0.0,0.0,0.0,0.0,-1.5],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,2.0,-1.5,0.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.20000000000000018,0.0,2.0,-1.5],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.40000000000000013,0.0,2.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.6000000000000001,0.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.8]],"num_vars":10}},"target":{"problem":"SpinGlass","variant":{"graph":"SimpleGraph","weight":"f64"},"instance":{"couplings":[0.5,-0.375,0.5,-0.375,0.5,-0.375,0.5,-0.375,0.5,-0.375,0.5,-0.375,0.5,-0.375,0.5],"fields":[0.125,0.22499999999999998,-0.55,-0.44999999999999996,-1.225,0.625,0.7250000000000001,1.7000000000000002,0.925,0.15000000000000002],"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,1,1,0,1,0,0,1],"target_config":[1,0,1,1,1,0,1,0,0,1]}]},
     {"source":{"problem":"Satisfiability","variant":{},"instance":{"clauses":[{"literals":[1,-2,3]},{"literals":[-1,2]},{"literals":[2,3]}],"num_vars":3}},"target":{"problem":"CircuitSAT","variant":{},"instance":{"circuit":{"assignments":[{"expr":{"op":{"Or":[{"op":{"Var":"x1"}},{"op":{"Not":{"op":{"Var":"x2"}}}},{"op":{"Var":"x3"}}]}},"outputs":["__clause_0"]},{"expr":{"op":{"Or":[{"op":{"Not":{"op":{"Var":"x1"}}}},{"op":{"Var":"x2"}}]}},"outputs":["__clause_1"]},{"expr":{"op":{"Or":[{"op":{"Var":"x2"}},{"op":{"Var":"x3"}}]}},"outputs":["__clause_2"]},{"expr":{"op":{"And":[{"op":{"Var":"__clause_0"}},{"op":{"Var":"__clause_1"}},{"op":{"Var":"__clause_2"}}]}},"outputs":["__out"]},{"expr":{"op":{"Const":true}},"outputs":["__out"]}]},"variables":["__clause_0","__clause_1","__clause_2","__out","x1","x2","x3"]}},"solutions":[{"source_config":[1,1,1],"target_config":[1,1,1,1,1,1,1]}]},
     {"source":{"problem":"Satisfiability","variant":{},"instance":{"clauses":[{"literals":[1]},{"literals":[-3]},{"literals":[5]}],"num_vars":5}},"target":{"problem":"KColoring","variant":{"graph":"SimpleGraph","k":"K3"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,2,null],[1,2,null],[3,2,null],[8,2,null],[3,8,null],[4,2,null],[9,2,null],[4,9,null],[5,2,null],[10,2,null],[5,10,null],[6,2,null],[11,2,null],[6,11,null],[7,2,null],[12,2,null],[7,12,null],[3,2,null],[3,1,null],[10,2,null],[10,1,null],[7,2,null],[7,1,null]],"node_holes":[],"nodes":[null,null,null,null,null,null,null,null,null,null,null,null,null]}},"num_colors":3}},"solutions":[{"source_config":[1,1,0,1,1],"target_config":[2,1,0,2,2,1,2,2,1,1,2,1,1]}]},
-    {"source":{"problem":"Satisfiability","variant":{},"instance":{"clauses":[{"literals":[1]},{"literals":[2,-3]},{"literals":[-1,3,4]},{"literals":[2,-4,5]},{"literals":[1,-2,3,-5]},{"literals":[-1,2,-3,4,5]}],"num_vars":5}},"target":{"problem":"KSatisfiability","variant":{"k":"K3"},"instance":{"clauses":[{"literals":[1,6,7]},{"literals":[1,6,-7]},{"literals":[1,-6,8]},{"literals":[1,-6,-8]},{"literals":[2,-3,9]},{"literals":[2,-3,-9]},{"literals":[-1,3,4]},{"literals":[2,-4,5]},{"literals":[1,-2,10]},{"literals":[-10,3,-5]},{"literals":[-1,2,11]},{"literals":[-11,-3,12]},{"literals":[-12,4,5]}],"num_vars":12}},"solutions":[{"source_config":[1,0,0,1,1],"target_config":[1,0,0,1,1,0,0,0,0,0,1,1]}]},
+    {"source":{"problem":"Satisfiability","variant":{},"instance":{"clauses":[{"literals":[1]},{"literals":[2,-3]},{"literals":[-1,3,4]},{"literals":[2,-4,5]},{"literals":[1,-2,3,-5]},{"literals":[-1,2,-3,4,5]}],"num_vars":5}},"target":{"problem":"KSatisfiability","variant":{"k":"K3"},"instance":{"clauses":[{"literals":[1,6,7]},{"literals":[1,6,-7]},{"literals":[1,-6,8]},{"literals":[1,-6,-8]},{"literals":[2,-3,9]},{"literals":[2,-3,-9]},{"literals":[-1,3,4]},{"literals":[2,-4,5]},{"literals":[1,-2,10]},{"literals":[-10,3,-5]},{"literals":[-1,2,11]},{"literals":[-11,-3,12]},{"literals":[-12,4,5]}],"num_vars":12}},"solutions":[{"source_config":[1,1,1,0,1],"target_config":[1,1,1,0,1,0,0,0,0,1,1,1]}]},
     {"source":{"problem":"Satisfiability","variant":{},"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":"MaximumIndependentSet","variant":{"graph":"SimpleGraph","weight":"One"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,2,null],[1,2,null],[3,4,null],[3,5,null],[4,5,null],[6,7,null],[6,8,null],[7,8,null],[9,10,null],[9,11,null],[10,11,null],[12,13,null],[12,14,null],[13,14,null],[15,16,null],[15,17,null],[16,17,null],[18,19,null],[18,20,null],[19,20,null],[0,3,null],[0,15,null],[1,9,null],[1,16,null],[2,4,null],[2,10,null],[2,18,null],[3,12,null],[4,13,null],[5,7,null],[5,19,null],[6,9,null],[6,16,null],[7,17,null],[8,11,null],[8,20,null],[10,13,null],[11,14,null],[12,15,null],[13,18,null],[14,20,null],[17,19,null]],"node_holes":[],"nodes":[null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null]}},"weights":[1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]}},"solutions":[{"source_config":[1,1,1,1,0],"target_config":[1,0,0,0,1,0,1,0,0,0,0,1,1,0,0,0,0,1,1,0,0]}]},
     {"source":{"problem":"Satisfiability","variant":{},"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":"MinimumDominatingSet","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,2,null],[1,2,null],[3,4,null],[3,5,null],[4,5,null],[6,7,null],[6,8,null],[7,8,null],[9,10,null],[9,11,null],[10,11,null],[12,13,null],[12,14,null],[13,14,null],[0,15,null],[3,15,null],[7,15,null],[1,16,null],[6,16,null],[9,16,null],[3,17,null],[10,17,null],[12,17,null],[4,18,null],[6,18,null],[13,18,null],[0,19,null],[7,19,null],[12,19,null],[1,20,null],[4,20,null],[9,20,null],[6,21,null],[10,21,null],[13,21,null]],"node_holes":[],"nodes":[null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null]}},"weights":[1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]}},"solutions":[{"source_config":[1,0,1,1,1],"target_config":[1,0,0,0,1,0,1,0,0,1,0,0,1,0,0,0,0,0,0,0,0,0]}]},
-    {"source":{"problem":"SpinGlass","variant":{"graph":"SimpleGraph","weight":"f64"},"instance":{"couplings":[1.0,-1.0,1.0,-1.0,1.0,-1.0,1.0,-1.0,1.0,-1.0,1.0,-1.0,1.0,-1.0,1.0],"fields":[0.0,0.0,0.0,0.0,0.0,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]}}}},"target":{"problem":"QUBO","variant":{"weight":"f64"},"instance":{"matrix":[[-2.0,4.0,0.0,0.0,-4.0,4.0,0.0,0.0,0.0,0.0],[0.0,-2.0,-4.0,0.0,0.0,0.0,4.0,0.0,0.0,0.0],[0.0,0.0,2.0,-4.0,0.0,0.0,0.0,4.0,0.0,0.0],[0.0,0.0,0.0,2.0,-4.0,0.0,0.0,0.0,4.0,0.0],[0.0,0.0,0.0,0.0,6.0,0.0,0.0,0.0,0.0,-4.0],[0.0,0.0,0.0,0.0,0.0,-2.0,0.0,4.0,-4.0,0.0],[0.0,0.0,0.0,0.0,0.0,0.0,-2.0,0.0,4.0,-4.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,-6.0,0.0,4.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,2.0]],"num_vars":10}},"solutions":[{"source_config":[0,1,1,0,0,1,0,0,1,0],"target_config":[0,1,1,0,0,1,0,0,1,0]}]},
-    {"source":{"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]}}}},"target":{"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]}}}},"solutions":[{"source_config":[0,1,1,0,0,1,0,0,1,0],"target_config":[0,1,1,0,0,1,0,0,1,0]}]},
-    {"source":{"problem":"TravelingSalesman","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"edge_weights":[10,15,20,35,25,30],"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]}}}},"target":{"problem":"ILP","variant":{"variable":"bool"},"instance":{"constraints":[{"cmp":"Eq","rhs":1.0,"terms":[[0,1.0],[1,1.0],[2,1.0],[3,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[4,1.0],[5,1.0],[6,1.0],[7,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[8,1.0],[9,1.0],[10,1.0],[11,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[12,1.0],[13,1.0],[14,1.0],[15,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[0,1.0],[4,1.0],[8,1.0],[12,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[1,1.0],[5,1.0],[9,1.0],[13,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[2,1.0],[6,1.0],[10,1.0],[14,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[3,1.0],[7,1.0],[11,1.0],[15,1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[16,1.0],[0,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[16,1.0],[5,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[16,1.0],[0,-1.0],[5,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[17,1.0],[4,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[17,1.0],[1,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[17,1.0],[4,-1.0],[1,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[18,1.0],[1,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[18,1.0],[6,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[18,1.0],[1,-1.0],[6,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[19,1.0],[5,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[19,1.0],[2,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[19,1.0],[5,-1.0],[2,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[20,1.0],[2,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[20,1.0],[7,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[20,1.0],[2,-1.0],[7,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[21,1.0],[6,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[21,1.0],[3,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[21,1.0],[6,-1.0],[3,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[22,1.0],[3,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[22,1.0],[4,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[22,1.0],[3,-1.0],[4,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[23,1.0],[7,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[23,1.0],[0,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[23,1.0],[7,-1.0],[0,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[24,1.0],[0,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[24,1.0],[9,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[24,1.0],[0,-1.0],[9,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[25,1.0],[8,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[25,1.0],[1,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[25,1.0],[8,-1.0],[1,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[26,1.0],[1,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[26,1.0],[10,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[26,1.0],[1,-1.0],[10,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[27,1.0],[9,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[27,1.0],[2,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[27,1.0],[9,-1.0],[2,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[28,1.0],[2,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[28,1.0],[11,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[28,1.0],[2,-1.0],[11,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[29,1.0],[10,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[29,1.0],[3,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[29,1.0],[10,-1.0],[3,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[30,1.0],[3,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[30,1.0],[8,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[30,1.0],[3,-1.0],[8,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[31,1.0],[11,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[31,1.0],[0,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[31,1.0],[11,-1.0],[0,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[32,1.0],[0,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[32,1.0],[13,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[32,1.0],[0,-1.0],[13,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[33,1.0],[12,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[33,1.0],[1,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[33,1.0],[12,-1.0],[1,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[34,1.0],[1,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[34,1.0],[14,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[34,1.0],[1,-1.0],[14,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[35,1.0],[13,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[35,1.0],[2,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[35,1.0],[13,-1.0],[2,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[36,1.0],[2,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[36,1.0],[15,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[36,1.0],[2,-1.0],[15,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[37,1.0],[14,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[37,1.0],[3,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[37,1.0],[14,-1.0],[3,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[38,1.0],[3,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[38,1.0],[12,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[38,1.0],[3,-1.0],[12,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[39,1.0],[15,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[39,1.0],[0,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[39,1.0],[15,-1.0],[0,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[40,1.0],[4,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[40,1.0],[9,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[40,1.0],[4,-1.0],[9,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[41,1.0],[8,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[41,1.0],[5,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[41,1.0],[8,-1.0],[5,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[42,1.0],[5,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[42,1.0],[10,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[42,1.0],[5,-1.0],[10,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[43,1.0],[9,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[43,1.0],[6,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[43,1.0],[9,-1.0],[6,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[44,1.0],[6,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[44,1.0],[11,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[44,1.0],[6,-1.0],[11,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[45,1.0],[10,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[45,1.0],[7,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[45,1.0],[10,-1.0],[7,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[46,1.0],[7,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[46,1.0],[8,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[46,1.0],[7,-1.0],[8,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[47,1.0],[11,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[47,1.0],[4,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[47,1.0],[11,-1.0],[4,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[48,1.0],[4,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[48,1.0],[13,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[48,1.0],[4,-1.0],[13,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[49,1.0],[12,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[49,1.0],[5,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[49,1.0],[12,-1.0],[5,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[50,1.0],[5,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[50,1.0],[14,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[50,1.0],[5,-1.0],[14,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[51,1.0],[13,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[51,1.0],[6,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[51,1.0],[13,-1.0],[6,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[52,1.0],[6,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[52,1.0],[15,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[52,1.0],[6,-1.0],[15,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[53,1.0],[14,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[53,1.0],[7,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[53,1.0],[14,-1.0],[7,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[54,1.0],[7,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[54,1.0],[12,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[54,1.0],[7,-1.0],[12,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[55,1.0],[15,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[55,1.0],[4,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[55,1.0],[15,-1.0],[4,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[56,1.0],[8,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[56,1.0],[13,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[56,1.0],[8,-1.0],[13,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[57,1.0],[12,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[57,1.0],[9,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[57,1.0],[12,-1.0],[9,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[58,1.0],[9,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[58,1.0],[14,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[58,1.0],[9,-1.0],[14,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[59,1.0],[13,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[59,1.0],[10,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[59,1.0],[13,-1.0],[10,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[60,1.0],[10,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[60,1.0],[15,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[60,1.0],[10,-1.0],[15,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[61,1.0],[14,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[61,1.0],[11,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[61,1.0],[14,-1.0],[11,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[62,1.0],[11,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[62,1.0],[12,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[62,1.0],[11,-1.0],[12,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[63,1.0],[15,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[63,1.0],[8,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[63,1.0],[15,-1.0],[8,-1.0]]}],"num_vars":64,"objective":[[16,10.0],[17,10.0],[18,10.0],[19,10.0],[20,10.0],[21,10.0],[22,10.0],[23,10.0],[24,15.0],[25,15.0],[26,15.0],[27,15.0],[28,15.0],[29,15.0],[30,15.0],[31,15.0],[32,20.0],[33,20.0],[34,20.0],[35,20.0],[36,20.0],[37,20.0],[38,20.0],[39,20.0],[40,35.0],[41,35.0],[42,35.0],[43,35.0],[44,35.0],[45,35.0],[46,35.0],[47,35.0],[48,25.0],[49,25.0],[50,25.0],[51,25.0],[52,25.0],[53,25.0],[54,25.0],[55,25.0],[56,30.0],[57,30.0],[58,30.0],[59,30.0],[60,30.0],[61,30.0],[62,30.0],[63,30.0]],"sense":"Minimize"}},"solutions":[{"source_config":[1,1,0,0,1,1],"target_config":[0,1,0,0,1,0,0,0,0,0,1,0,0,0,0,1,0,1,0,0,0,0,0,0,0,0,1,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,0,0,0,1,0,0,0,0,1,0,0,0]}]},
-    {"source":{"problem":"TravelingSalesman","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"edge_weights":[1,2,3],"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,2,null],[1,2,null]],"node_holes":[],"nodes":[null,null,null]}}}},"target":{"problem":"QUBO","variant":{"weight":"f64"},"instance":{"matrix":[[-14.0,14.0,14.0,14.0,1.0,1.0,14.0,2.0,2.0],[0.0,-14.0,14.0,1.0,14.0,1.0,2.0,14.0,2.0],[0.0,0.0,-14.0,1.0,1.0,14.0,2.0,2.0,14.0],[0.0,0.0,0.0,-14.0,14.0,14.0,14.0,3.0,3.0],[0.0,0.0,0.0,0.0,-14.0,14.0,3.0,14.0,3.0],[0.0,0.0,0.0,0.0,0.0,-14.0,3.0,3.0,14.0],[0.0,0.0,0.0,0.0,0.0,0.0,-14.0,14.0,14.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,-14.0,14.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,-14.0]],"num_vars":9}},"solutions":[{"source_config":[1,1,1],"target_config":[0,0,1,0,1,0,1,0,0]}]}
+    {"source":{"problem":"SpinGlass","variant":{"graph":"SimpleGraph","weight":"f64"},"instance":{"couplings":[1.0,-1.0,1.0,-1.0,1.0,-1.0,1.0,-1.0,1.0,-1.0,1.0,-1.0,1.0,-1.0,1.0],"fields":[0.0,0.0,0.0,0.0,0.0,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]}}}},"target":{"problem":"QUBO","variant":{"weight":"f64"},"instance":{"matrix":[[-2.0,4.0,0.0,0.0,-4.0,4.0,0.0,0.0,0.0,0.0],[0.0,-2.0,-4.0,0.0,0.0,0.0,4.0,0.0,0.0,0.0],[0.0,0.0,2.0,-4.0,0.0,0.0,0.0,4.0,0.0,0.0],[0.0,0.0,0.0,2.0,-4.0,0.0,0.0,0.0,4.0,0.0],[0.0,0.0,0.0,0.0,6.0,0.0,0.0,0.0,0.0,-4.0],[0.0,0.0,0.0,0.0,0.0,-2.0,0.0,4.0,-4.0,0.0],[0.0,0.0,0.0,0.0,0.0,0.0,-2.0,0.0,4.0,-4.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,-6.0,0.0,4.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,2.0]],"num_vars":10}},"solutions":[{"source_config":[1,0,1,1,1,0,1,0,0,1],"target_config":[1,0,1,1,1,0,1,0,0,1]}]},
+    {"source":{"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]}}}},"target":{"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]}}}},"solutions":[{"source_config":[1,0,1,1,1,0,1,0,0,1],"target_config":[1,0,1,1,1,0,1,0,0,1]}]},
+    {"source":{"problem":"TravelingSalesman","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"edge_weights":[10,15,20,35,25,30],"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]}}}},"target":{"problem":"ILP","variant":{"variable":"bool"},"instance":{"constraints":[{"cmp":"Eq","rhs":1.0,"terms":[[0,1.0],[1,1.0],[2,1.0],[3,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[4,1.0],[5,1.0],[6,1.0],[7,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[8,1.0],[9,1.0],[10,1.0],[11,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[12,1.0],[13,1.0],[14,1.0],[15,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[0,1.0],[4,1.0],[8,1.0],[12,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[1,1.0],[5,1.0],[9,1.0],[13,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[2,1.0],[6,1.0],[10,1.0],[14,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[3,1.0],[7,1.0],[11,1.0],[15,1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[16,1.0],[0,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[16,1.0],[5,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[16,1.0],[0,-1.0],[5,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[17,1.0],[4,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[17,1.0],[1,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[17,1.0],[4,-1.0],[1,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[18,1.0],[1,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[18,1.0],[6,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[18,1.0],[1,-1.0],[6,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[19,1.0],[5,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[19,1.0],[2,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[19,1.0],[5,-1.0],[2,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[20,1.0],[2,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[20,1.0],[7,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[20,1.0],[2,-1.0],[7,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[21,1.0],[6,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[21,1.0],[3,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[21,1.0],[6,-1.0],[3,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[22,1.0],[3,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[22,1.0],[4,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[22,1.0],[3,-1.0],[4,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[23,1.0],[7,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[23,1.0],[0,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[23,1.0],[7,-1.0],[0,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[24,1.0],[0,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[24,1.0],[9,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[24,1.0],[0,-1.0],[9,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[25,1.0],[8,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[25,1.0],[1,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[25,1.0],[8,-1.0],[1,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[26,1.0],[1,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[26,1.0],[10,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[26,1.0],[1,-1.0],[10,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[27,1.0],[9,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[27,1.0],[2,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[27,1.0],[9,-1.0],[2,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[28,1.0],[2,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[28,1.0],[11,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[28,1.0],[2,-1.0],[11,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[29,1.0],[10,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[29,1.0],[3,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[29,1.0],[10,-1.0],[3,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[30,1.0],[3,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[30,1.0],[8,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[30,1.0],[3,-1.0],[8,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[31,1.0],[11,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[31,1.0],[0,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[31,1.0],[11,-1.0],[0,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[32,1.0],[0,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[32,1.0],[13,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[32,1.0],[0,-1.0],[13,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[33,1.0],[12,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[33,1.0],[1,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[33,1.0],[12,-1.0],[1,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[34,1.0],[1,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[34,1.0],[14,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[34,1.0],[1,-1.0],[14,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[35,1.0],[13,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[35,1.0],[2,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[35,1.0],[13,-1.0],[2,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[36,1.0],[2,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[36,1.0],[15,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[36,1.0],[2,-1.0],[15,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[37,1.0],[14,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[37,1.0],[3,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[37,1.0],[14,-1.0],[3,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[38,1.0],[3,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[38,1.0],[12,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[38,1.0],[3,-1.0],[12,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[39,1.0],[15,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[39,1.0],[0,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[39,1.0],[15,-1.0],[0,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[40,1.0],[4,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[40,1.0],[9,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[40,1.0],[4,-1.0],[9,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[41,1.0],[8,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[41,1.0],[5,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[41,1.0],[8,-1.0],[5,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[42,1.0],[5,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[42,1.0],[10,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[42,1.0],[5,-1.0],[10,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[43,1.0],[9,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[43,1.0],[6,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[43,1.0],[9,-1.0],[6,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[44,1.0],[6,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[44,1.0],[11,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[44,1.0],[6,-1.0],[11,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[45,1.0],[10,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[45,1.0],[7,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[45,1.0],[10,-1.0],[7,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[46,1.0],[7,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[46,1.0],[8,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[46,1.0],[7,-1.0],[8,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[47,1.0],[11,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[47,1.0],[4,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[47,1.0],[11,-1.0],[4,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[48,1.0],[4,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[48,1.0],[13,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[48,1.0],[4,-1.0],[13,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[49,1.0],[12,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[49,1.0],[5,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[49,1.0],[12,-1.0],[5,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[50,1.0],[5,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[50,1.0],[14,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[50,1.0],[5,-1.0],[14,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[51,1.0],[13,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[51,1.0],[6,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[51,1.0],[13,-1.0],[6,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[52,1.0],[6,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[52,1.0],[15,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[52,1.0],[6,-1.0],[15,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[53,1.0],[14,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[53,1.0],[7,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[53,1.0],[14,-1.0],[7,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[54,1.0],[7,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[54,1.0],[12,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[54,1.0],[7,-1.0],[12,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[55,1.0],[15,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[55,1.0],[4,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[55,1.0],[15,-1.0],[4,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[56,1.0],[8,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[56,1.0],[13,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[56,1.0],[8,-1.0],[13,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[57,1.0],[12,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[57,1.0],[9,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[57,1.0],[12,-1.0],[9,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[58,1.0],[9,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[58,1.0],[14,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[58,1.0],[9,-1.0],[14,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[59,1.0],[13,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[59,1.0],[10,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[59,1.0],[13,-1.0],[10,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[60,1.0],[10,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[60,1.0],[15,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[60,1.0],[10,-1.0],[15,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[61,1.0],[14,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[61,1.0],[11,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[61,1.0],[14,-1.0],[11,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[62,1.0],[11,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[62,1.0],[12,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[62,1.0],[11,-1.0],[12,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[63,1.0],[15,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[63,1.0],[8,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[63,1.0],[15,-1.0],[8,-1.0]]}],"num_vars":64,"objective":[[16,10.0],[17,10.0],[18,10.0],[19,10.0],[20,10.0],[21,10.0],[22,10.0],[23,10.0],[24,15.0],[25,15.0],[26,15.0],[27,15.0],[28,15.0],[29,15.0],[30,15.0],[31,15.0],[32,20.0],[33,20.0],[34,20.0],[35,20.0],[36,20.0],[37,20.0],[38,20.0],[39,20.0],[40,35.0],[41,35.0],[42,35.0],[43,35.0],[44,35.0],[45,35.0],[46,35.0],[47,35.0],[48,25.0],[49,25.0],[50,25.0],[51,25.0],[52,25.0],[53,25.0],[54,25.0],[55,25.0],[56,30.0],[57,30.0],[58,30.0],[59,30.0],[60,30.0],[61,30.0],[62,30.0],[63,30.0]],"sense":"Minimize"}},"solutions":[{"source_config":[1,1,0,0,1,1],"target_config":[1,0,0,0,0,1,0,0,0,0,0,1,0,0,1,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,1,0,0]}]},
+    {"source":{"problem":"TravelingSalesman","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"edge_weights":[1,2,3],"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,2,null],[1,2,null]],"node_holes":[],"nodes":[null,null,null]}}}},"target":{"problem":"QUBO","variant":{"weight":"f64"},"instance":{"matrix":[[-14.0,14.0,14.0,14.0,1.0,1.0,14.0,2.0,2.0],[0.0,-14.0,14.0,1.0,14.0,1.0,2.0,14.0,2.0],[0.0,0.0,-14.0,1.0,1.0,14.0,2.0,2.0,14.0],[0.0,0.0,0.0,-14.0,14.0,14.0,14.0,3.0,3.0],[0.0,0.0,0.0,0.0,-14.0,14.0,3.0,14.0,3.0],[0.0,0.0,0.0,0.0,0.0,-14.0,3.0,3.0,14.0],[0.0,0.0,0.0,0.0,0.0,0.0,-14.0,14.0,14.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,-14.0,14.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,-14.0]],"num_vars":9}},"solutions":[{"source_config":[1,1,1],"target_config":[0,0,1,1,0,0,0,1,0]}]}
   ]
 }
diff --git a/src/models/misc/longest_common_subsequence.rs b/src/models/misc/longest_common_subsequence.rs
index 70b404247..517891007 100644
--- a/src/models/misc/longest_common_subsequence.rs
+++ b/src/models/misc/longest_common_subsequence.rs
@@ -1,12 +1,12 @@
 //! Longest Common Subsequence (LCS) problem implementation.
 //!
-//! Given a set of strings over a finite alphabet, find the longest string
-//! that is a subsequence of every input string. Polynomial-time for 2 strings
-//! via dynamic programming, but NP-hard for k >= 3 strings (Maier, 1978).
+//! Given a finite alphabet, a set of strings over that alphabet, and a bound
+//! `K`, determine whether there exists a common subsequence of length exactly
+//! `K`. This fixed-length witness model is equivalent to the standard
+//! "length at least `K`" decision formulation.
 
 use crate::registry::{FieldInfo, ProblemSchemaEntry};
-use crate::traits::{OptimizationProblem, Problem};
-use crate::types::{Direction, SolutionSize};
+use crate::traits::{Problem, SatisfactionProblem};
 use serde::{Deserialize, Serialize};
 
 inventory::submit! {
@@ -16,174 +16,171 @@ inventory::submit! {
         aliases: &["LCS"],
         dimensions: &[],
         module_path: module_path!(),
-        description: "Find the longest string that is a subsequence of every input string",
+        description: "Find a common subsequence of bounded length for a set of strings",
         fields: &[
-            FieldInfo { name: "strings", type_name: "Vec<Vec<u8>>", description: "The input strings" },
+            FieldInfo { name: "alphabet_size", type_name: "usize", description: "Size of the alphabet" },
+            FieldInfo { name: "strings", type_name: "Vec<Vec<usize>>", description: "Input strings over the alphabet {0, ..., alphabet_size-1}" },
+            FieldInfo { name: "bound", type_name: "usize", description: "Required length of the common subsequence witness" },
         ],
     }
 }
 
 /// The Longest Common Subsequence problem.
 ///
-/// Given `k` strings `s_1, ..., s_k` over a finite alphabet, find a longest
-/// string `w` that is a subsequence of every `s_i`.
-///
-/// A string `w` is a **subsequence** of `s` if `w` can be obtained by deleting
-/// zero or more characters from `s` without changing the order of the remaining
-/// characters.
+/// Given an alphabet of size `k`, a set of strings over `{0, ..., k-1}`, and a
+/// bound `K`, determine whether there exists a string `w` of length exactly `K`
+/// such that `w` is a subsequence of every input string. This is equivalent to
+/// the standard decision version with `|w| >= K`, because any longer witness has
+/// a length-`K` prefix that is also a common subsequence.
 ///
 /// # Representation
 ///
-/// The configuration is a binary vector of length equal to the shortest string.
-/// Each entry indicates whether the corresponding character of the shortest
-/// string is included in the candidate subsequence.
-///
-/// # Example
-///
-/// ```
-/// use problemreductions::models::misc::LongestCommonSubsequence;
-/// use problemreductions::{Problem, Solver, BruteForce};
-///
-/// let problem = LongestCommonSubsequence::new(vec![
-///     vec![b'A', b'B', b'C'],
-///     vec![b'A', b'C', b'B'],
-/// ]);
-/// let solver = BruteForce::new();
-/// let solution = solver.find_best(&problem);
-/// assert!(solution.is_some());
-/// ```
+/// The configuration is a vector of length `bound`, where each entry is a
+/// symbol in `{0, ..., alphabet_size-1}`. The instance is satisfiable iff that
+/// candidate witness is a subsequence of every input string.
 #[derive(Debug, Clone, Serialize, Deserialize)]
 pub struct LongestCommonSubsequence {
-    /// The input strings.
-    strings: Vec<Vec<u8>>,
+    alphabet_size: usize,
+    strings: Vec<Vec<usize>>,
+    bound: usize,
 }
 
 impl LongestCommonSubsequence {
-    /// Create a new LCS instance from a list of strings.
+    /// Create a new LongestCommonSubsequence instance.
     ///
     /// # Panics
-    /// Panics if fewer than 2 strings are provided.
-    pub fn new(strings: Vec<Vec<u8>>) -> Self {
+    ///
+    /// Panics if `alphabet_size == 0` while the witness length is positive or
+    /// any input string is non-empty, or if an input symbol is outside the
+    /// declared alphabet.
+    pub fn new(alphabet_size: usize, strings: Vec<Vec<usize>>, bound: usize) -> Self {
+        assert!(
+            alphabet_size > 0 || (bound == 0 && strings.iter().all(|s| s.is_empty())),
+            "alphabet_size must be > 0 when bound > 0 or any input string is non-empty"
+        );
         assert!(
-            strings.len() >= 2,
-            "LCS requires at least 2 strings, got {}",
-            strings.len()
+            strings
+                .iter()
+                .flat_map(|s| s.iter())
+                .all(|&symbol| symbol < alphabet_size),
+            "input symbols must be less than alphabet_size"
         );
-        Self { strings }
+        Self {
+            alphabet_size,
+            strings,
+            bound,
+        }
     }
 
-    /// Get the input strings.
-    pub fn strings(&self) -> &[Vec<u8>] {
+    /// Returns the alphabet size.
+    pub fn alphabet_size(&self) -> usize {
+        self.alphabet_size
+    }
+
+    /// Returns the input strings.
+    pub fn strings(&self) -> &[Vec<usize>] {
         &self.strings
     }
 
-    /// Get the number of strings.
+    /// Returns the witness-length bound.
+    pub fn bound(&self) -> usize {
+        self.bound
+    }
+
+    /// Returns the number of input strings.
     pub fn num_strings(&self) -> usize {
         self.strings.len()
     }
 
-    /// Get the total length of all strings.
+    /// Returns the total input length across all strings.
     pub fn total_length(&self) -> usize {
         self.strings.iter().map(|s| s.len()).sum()
     }
 
-    /// Get the length of the first string.
-    pub fn num_chars_first(&self) -> usize {
-        self.strings[0].len()
+    /// Returns the sum of squared string lengths.
+    pub fn sum_squared_lengths(&self) -> usize {
+        self.strings.iter().map(|s| s.len() * s.len()).sum()
     }
 
-    /// Get the length of the second string.
-    pub fn num_chars_second(&self) -> usize {
-        self.strings[1].len()
-    }
-
-    /// Index of the shortest string.
-    fn shortest_index(&self) -> usize {
+    /// Returns the sum of triangular numbers len * (len + 1) / 2 across strings.
+    pub fn sum_triangular_lengths(&self) -> usize {
         self.strings
             .iter()
-            .enumerate()
-            .min_by_key(|(_, s)| s.len())
-            .map(|(i, _)| i)
-            .unwrap()
+            .map(|s| s.len() * (s.len() + 1) / 2)
+            .sum()
     }
 
-    /// Length of the shortest string.
-    pub fn min_string_length(&self) -> usize {
-        self.strings[self.shortest_index()].len()
+    /// Returns the number of adjacent witness-position transitions.
+    pub fn num_transitions(&self) -> usize {
+        self.bound.saturating_sub(1)
     }
 }
 
-/// Check if `candidate` is a subsequence of `target`.
-fn is_subsequence(candidate: &[u8], target: &[u8]) -> bool {
-    let mut ti = 0;
-    for &ch in candidate {
-        while ti < target.len() && target[ti] != ch {
-            ti += 1;
-        }
-        if ti >= target.len() {
-            return false;
+/// Check whether `candidate` is a subsequence of `target` using greedy
+/// left-to-right matching.
+fn is_subsequence(candidate: &[usize], target: &[usize]) -> bool {
+    let mut it = target.iter();
+    for &symbol in candidate {
+        loop {
+            match it.next() {
+                Some(&next) if next == symbol => break,
+                Some(_) => continue,
+                None => return false,
+            }
         }
-        ti += 1;
     }
     true
 }
 
 impl Problem for LongestCommonSubsequence {
     const NAME: &'static str = "LongestCommonSubsequence";
-    type Metric = SolutionSize<i32>;
+    type Metric = bool;
 
     fn variant() -> Vec<(&'static str, &'static str)> {
         crate::variant_params![]
     }
 
     fn dims(&self) -> Vec<usize> {
-        vec![2; self.min_string_length()]
+        vec![self.alphabet_size; self.bound]
     }
 
-    fn evaluate(&self, config: &[usize]) -> SolutionSize<i32> {
-        let shortest_idx = self.shortest_index();
-        let shortest = &self.strings[shortest_idx];
-
-        if config.len() != shortest.len() {
-            return SolutionSize::Invalid;
-        }
-        if config.iter().any(|&v| v >= 2) {
-            return SolutionSize::Invalid;
+    fn evaluate(&self, config: &[usize]) -> bool {
+        if config.len() != self.bound {
+            return false;
         }
-
-        // Build candidate subsequence from selected positions of shortest string
-        let candidate: Vec<u8> = config
-            .iter()
-            .enumerate()
-            .filter(|(_, &x)| x == 1)
-            .map(|(i, _)| shortest[i])
-            .collect();
-
-        // Check that candidate is a subsequence of ALL strings
-        for (i, s) in self.strings.iter().enumerate() {
-            if i == shortest_idx {
-                // The candidate is always a subsequence of the string it was built from
-                continue;
-            }
-            if !is_subsequence(&candidate, s) {
-                return SolutionSize::Invalid;
-            }
+        if config.iter().any(|&symbol| symbol >= self.alphabet_size) {
+            return false;
         }
-
-        SolutionSize::Valid(candidate.len() as i32)
+        self.strings.iter().all(|s| is_subsequence(config, s))
     }
 }
 
-impl OptimizationProblem for LongestCommonSubsequence {
-    type Value = i32;
+impl SatisfactionProblem for LongestCommonSubsequence {}
 
-    fn direction(&self) -> Direction {
-        Direction::Maximize
-    }
+crate::declare_variants! {
+    default sat LongestCommonSubsequence => "alphabet_size ^ bound",
 }
 
-crate::declare_variants! {
-    default opt LongestCommonSubsequence => "2^min_string_length",
+#[cfg(feature = "example-db")]
+pub(crate) fn canonical_model_example_specs() -> Vec<crate::example_db::specs::ModelExampleSpec> {
+    vec![crate::example_db::specs::ModelExampleSpec {
+        id: "longest_common_subsequence",
+        build: || {
+            let problem = LongestCommonSubsequence::new(
+                2,
+                vec![
+                    vec![0, 1, 0, 1, 1, 0],
+                    vec![1, 0, 0, 1, 0, 1],
+                    vec![0, 0, 1, 0, 1, 1],
+                    vec![1, 1, 0, 0, 1, 0],
+                    vec![0, 1, 0, 1, 0, 1],
+                    vec![1, 0, 1, 0, 1, 0],
+                ],
+                3,
+            );
+            crate::example_db::specs::satisfaction_example(problem, vec![vec![0, 1, 0]])
+        },
+    }]
 }
 
 #[cfg(test)]
diff --git a/src/models/misc/mod.rs b/src/models/misc/mod.rs
index 24b28125d..17ea89847 100644
--- a/src/models/misc/mod.rs
+++ b/src/models/misc/mod.rs
@@ -46,6 +46,7 @@ pub use subset_sum::SubsetSum;
 pub(crate) fn canonical_model_example_specs() -> Vec<crate::example_db::specs::ModelExampleSpec> {
     let mut specs = Vec::new();
     specs.extend(factoring::canonical_model_example_specs());
+    specs.extend(longest_common_subsequence::canonical_model_example_specs());
     specs.extend(multiprocessor_scheduling::canonical_model_example_specs());
     specs.extend(paintshop::canonical_model_example_specs());
     specs.extend(sequencing_within_intervals::canonical_model_example_specs());
diff --git a/src/rules/longestcommonsubsequence_ilp.rs b/src/rules/longestcommonsubsequence_ilp.rs
index 3394c73a6..b6ecf4433 100644
--- a/src/rules/longestcommonsubsequence_ilp.rs
+++ b/src/rules/longestcommonsubsequence_ilp.rs
@@ -1,19 +1,13 @@
 //! Reduction from LongestCommonSubsequence to ILP (Integer Linear Programming).
 //!
-//! Uses the match-pair formulation (Blum et al., 2021; Althaus et al., 2006).
-//! For 2 strings s1 (length n1) and s2 (length n2):
+//! The source problem is the decision version of LCS with a fixed witness
+//! length `K`. The ILP builds a binary feasibility model:
+//! - `x_(p,a)` selects symbol `a` at witness position `p`
+//! - `y_(r,p,j)` selects the matching position `j` in source string `r`
 //!
-//! ## Variables
-//! For each pair (j1, j2) where s1[j1] == s2[j2], a binary variable m_{j1,j2}.
-//!
-//! ## Constraints
-//! 1. Each position in s1 matched at most once
-//! 2. Each position in s2 matched at most once
-//! 3. Order preservation (no crossings): for (j1,j2),(j1',j2') with j1 < j1' and j2 > j2':
-//!    m_{j1,j2} + m_{j1',j2'} <= 1
-//!
-//! ## Objective
-//! Maximize sum of all match variables.
+//! The constraints enforce exactly one symbol per witness position, exactly one
+//! matched source position per `(r, p)`, character consistency, and strictly
+//! increasing matched positions within each source string.
 
 use crate::models::algebraic::{LinearConstraint, ObjectiveSense, ILP};
 use crate::models::misc::LongestCommonSubsequence;
@@ -24,12 +18,14 @@ use crate::rules::traits::{ReduceTo, ReductionResult};
 #[derive(Debug, Clone)]
 pub struct ReductionLCSToILP {
     target: ILP<bool>,
-    /// The match pairs: (j1, j2) for each variable index.
-    match_pairs: Vec<(usize, usize)>,
-    /// Number of characters in the first string.
-    n1: usize,
-    /// Number of characters in the second string.
-    n2: usize,
+    alphabet_size: usize,
+    bound: usize,
+}
+
+impl ReductionLCSToILP {
+    fn symbol_var(&self, position: usize, symbol: usize) -> usize {
+        position * self.alphabet_size + symbol
+    }
 }
 
 impl ReductionResult for ReductionLCSToILP {
@@ -40,122 +36,104 @@ impl ReductionResult for ReductionLCSToILP {
         &self.target
     }
 
-    /// Extract solution from ILP back to LCS.
-    ///
-    /// The ILP solution has binary variables for match pairs. We extract the
-    /// matched positions, build the LCS, and map back to a binary selection
-    /// on the shortest source string.
     fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
-        // The source problem's dims() is based on the shortest string.
-        // We build match pairs on s1=strings[0], s2=strings[1].
-        // If shortest is s1, we use j1 positions; if s2, we use j2 positions.
-        let shortest_len = std::cmp::min(self.n1, self.n2);
-        let shortest_is_first = self.n1 <= self.n2;
-
-        let matched_positions: Vec<usize> = self
-            .match_pairs
-            .iter()
-            .enumerate()
-            .filter(|(i, _)| target_solution.get(*i).copied().unwrap_or(0) == 1)
-            .map(|(_, &(j1, j2))| if shortest_is_first { j1 } else { j2 })
-            .collect();
-
-        let mut config = vec![0usize; shortest_len];
-        for pos in matched_positions {
-            if pos < config.len() {
-                config[pos] = 1;
-            }
+        let mut witness = Vec::with_capacity(self.bound);
+        for position in 0..self.bound {
+            let selected = (0..self.alphabet_size)
+                .find(|&symbol| target_solution.get(self.symbol_var(position, symbol)) == Some(&1))
+                .unwrap_or(0);
+            witness.push(selected);
         }
-        config
+        witness
     }
 }
 
 #[reduction(
     overhead = {
-    num_vars = "num_chars_first * num_chars_second",
-    num_constraints = "num_chars_first + num_chars_second + (num_chars_first * num_chars_second) ^ 2",
+        num_vars = "bound * alphabet_size + bound * total_length",
+        num_constraints = "bound + bound * num_strings + bound * total_length + num_transitions * sum_triangular_lengths",
     }
 )]
 impl ReduceTo<ILP<bool>> for LongestCommonSubsequence {
     type Result = ReductionLCSToILP;
 
     fn reduce_to(&self) -> Self::Result {
+        let alphabet_size = self.alphabet_size();
+        let bound = self.bound();
         let strings = self.strings();
-        assert!(
-            strings.len() == 2,
-            "LCS to ILP reduction is defined for exactly 2 strings, got {}",
-            strings.len()
-        );
-
-        let s1 = &strings[0];
-        let s2 = &strings[1];
-        let n1 = s1.len();
-        let n2 = s2.len();
-
-        // Build match pairs: (j1, j2) where s1[j1] == s2[j2]
-        let mut match_pairs: Vec<(usize, usize)> = Vec::new();
-        for (j1, &c1) in s1.iter().enumerate() {
-            for (j2, &c2) in s2.iter().enumerate() {
-                if c1 == c2 {
-                    match_pairs.push((j1, j2));
-                }
-            }
+        let total_length = self.total_length();
+
+        let symbol_var_count = bound * alphabet_size;
+        let mut string_offsets = Vec::with_capacity(strings.len());
+        let mut running_offset = 0usize;
+        for string in strings {
+            string_offsets.push(running_offset);
+            running_offset += string.len();
         }
 
-        let num_vars = match_pairs.len();
+        let match_var = |string_index: usize, position: usize, char_index: usize| -> usize {
+            symbol_var_count + position * total_length + string_offsets[string_index] + char_index
+        };
+
         let mut constraints = Vec::new();
 
-        // Constraint 1: Each position in s1 matched at most once
-        for j1 in 0..n1 {
-            let terms: Vec<(usize, f64)> = match_pairs
-                .iter()
-                .enumerate()
-                .filter(|(_, &(a, _))| a == j1)
-                .map(|(idx, _)| (idx, 1.0))
+        // Exactly one symbol per witness position.
+        for position in 0..bound {
+            let terms = (0..alphabet_size)
+                .map(|symbol| (position * alphabet_size + symbol, 1.0))
                 .collect();
-            if !terms.is_empty() {
-                constraints.push(LinearConstraint::le(terms, 1.0));
-            }
+            constraints.push(LinearConstraint::eq(terms, 1.0));
         }
 
-        // Constraint 2: Each position in s2 matched at most once
-        for j2 in 0..n2 {
-            let terms: Vec<(usize, f64)> = match_pairs
-                .iter()
-                .enumerate()
-                .filter(|(_, &(_, b))| b == j2)
-                .map(|(idx, _)| (idx, 1.0))
-                .collect();
-            if !terms.is_empty() {
-                constraints.push(LinearConstraint::le(terms, 1.0));
+        // For every string and witness position, choose exactly one matching source position.
+        for (string_index, string) in strings.iter().enumerate() {
+            for position in 0..bound {
+                let terms = (0..string.len())
+                    .map(|char_index| (match_var(string_index, position, char_index), 1.0))
+                    .collect();
+                constraints.push(LinearConstraint::eq(terms, 1.0));
             }
         }
 
-        // Constraint 3: Order preservation (no crossings)
-        // For all pairs (j1, j2) and (j1', j2') with j1 < j1' and j2 > j2':
-        //   m_{j1,j2} + m_{j1',j2'} <= 1
-        for (i, &(j1, j2)) in match_pairs.iter().enumerate() {
-            for (k, &(j1p, j2p)) in match_pairs.iter().enumerate() {
-                if i < k && j1 < j1p && j2 > j2p {
-                    constraints.push(LinearConstraint::le(vec![(i, 1.0), (k, 1.0)], 1.0));
-                }
-                // Also check the reverse: j1 > j1p and j2 < j2p
-                if i < k && j1 > j1p && j2 < j2p {
-                    constraints.push(LinearConstraint::le(vec![(i, 1.0), (k, 1.0)], 1.0));
+        // A chosen source position can only realize the selected witness symbol.
+        for (string_index, string) in strings.iter().enumerate() {
+            for position in 0..bound {
+                for (char_index, &symbol) in string.iter().enumerate() {
+                    constraints.push(LinearConstraint::le(
+                        vec![
+                            (match_var(string_index, position, char_index), 1.0),
+                            (position * alphabet_size + symbol, -1.0),
+                        ],
+                        0.0,
+                    ));
                 }
             }
         }
 
-        // Objective: maximize sum of all match variables
-        let objective: Vec<(usize, f64)> = (0..num_vars).map(|i| (i, 1.0)).collect();
+        // Consecutive witness positions must map to strictly increasing source positions.
+        for (string_index, string) in strings.iter().enumerate() {
+            for position in 0..bound.saturating_sub(1) {
+                for previous in 0..string.len() {
+                    for next in 0..=previous {
+                        constraints.push(LinearConstraint::le(
+                            vec![
+                                (match_var(string_index, position, previous), 1.0),
+                                (match_var(string_index, position + 1, next), 1.0),
+                            ],
+                            1.0,
+                        ));
+                    }
+                }
+            }
+        }
 
-        let ilp = ILP::<bool>::new(num_vars, constraints, objective, ObjectiveSense::Maximize);
+        let num_vars = symbol_var_count + bound * total_length;
+        let target = ILP::<bool>::new(num_vars, constraints, vec![], ObjectiveSense::Minimize);
 
         ReductionLCSToILP {
-            target: ilp,
-            match_pairs,
-            n1,
-            n2,
+            target,
+            alphabet_size,
+            bound,
         }
     }
 }
@@ -165,11 +143,11 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "longestcommonsubsequence_to_ilp",
         build: || {
-            let source = LongestCommonSubsequence::new(vec![
-                vec![b'A', b'B', b'A', b'C'],
-                vec![b'B', b'A', b'C', b'A'],
-            ]);
-            crate::example_db::specs::direct_ilp_example::<_, bool, _>(source, |_, _| true)
+            let source = LongestCommonSubsequence::new(3, vec![vec![0, 1, 2], vec![1, 0, 2]], 2);
+            crate::example_db::specs::direct_ilp_example::<_, bool, _>(
+                source,
+                crate::example_db::specs::keep_bool_source,
+            )
         },
     }]
 }
diff --git a/src/unit_tests/models/misc/longest_common_subsequence.rs b/src/unit_tests/models/misc/longest_common_subsequence.rs
index 33d4a0e90..edc660b2a 100644
--- a/src/unit_tests/models/misc/longest_common_subsequence.rs
+++ b/src/unit_tests/models/misc/longest_common_subsequence.rs
@@ -1,19 +1,48 @@
 use super::*;
 use crate::solvers::{BruteForce, Solver};
-use crate::traits::{OptimizationProblem, Problem};
-use crate::types::Direction;
+use crate::traits::Problem;
+
+fn issue_yes_instance() -> LongestCommonSubsequence {
+    LongestCommonSubsequence::new(
+        2,
+        vec![
+            vec![0, 1, 0, 1, 1, 0],
+            vec![1, 0, 0, 1, 0, 1],
+            vec![0, 0, 1, 0, 1, 1],
+            vec![1, 1, 0, 0, 1, 0],
+            vec![0, 1, 0, 1, 0, 1],
+            vec![1, 0, 1, 0, 1, 0],
+        ],
+        3,
+    )
+}
+
+fn issue_no_instance() -> LongestCommonSubsequence {
+    LongestCommonSubsequence::new(
+        2,
+        vec![
+            vec![0, 0, 0],
+            vec![1, 1, 1],
+            vec![0, 1, 0],
+            vec![1, 0, 1],
+            vec![0, 0, 1],
+            vec![1, 1, 0],
+        ],
+        1,
+    )
+}
 
 #[test]
 fn test_lcs_basic() {
-    let problem = LongestCommonSubsequence::new(vec![
-        vec![b'A', b'B', b'C', b'D', b'A', b'B'],
-        vec![b'B', b'D', b'C', b'A', b'B', b'A'],
-    ]);
-    assert_eq!(problem.num_strings(), 2);
-    assert_eq!(problem.total_length(), 12);
-    assert_eq!(problem.num_chars_first(), 6);
-    assert_eq!(problem.num_chars_second(), 6);
-    assert_eq!(problem.direction(), Direction::Maximize);
+    let problem = issue_yes_instance();
+    assert_eq!(problem.alphabet_size(), 2);
+    assert_eq!(problem.num_strings(), 6);
+    assert_eq!(problem.bound(), 3);
+    assert_eq!(problem.total_length(), 36);
+    assert_eq!(problem.sum_squared_lengths(), 216);
+    assert_eq!(problem.sum_triangular_lengths(), 126);
+    assert_eq!(problem.num_transitions(), 2);
+    assert_eq!(problem.dims(), vec![2; 3]);
     assert_eq!(
         <LongestCommonSubsequence as Problem>::NAME,
         "LongestCommonSubsequence"
@@ -22,136 +51,94 @@ fn test_lcs_basic() {
 }
 
 #[test]
-fn test_lcs_dims() {
-    // Shortest string has 4 chars
-    let problem = LongestCommonSubsequence::new(vec![
-        vec![b'A', b'B', b'A', b'C'],
-        vec![b'B', b'A', b'C', b'A', b'B', b'C'],
-    ]);
-    assert_eq!(problem.dims(), vec![2; 4]);
-}
-
-#[test]
-fn test_lcs_evaluate_valid() {
-    // s1 = "ABC", s2 = "ACB"
-    // Selecting positions 0,2 of s1 (shorter) gives "AC" which is subseq of "ACB"
-    let problem =
-        LongestCommonSubsequence::new(vec![vec![b'A', b'B', b'C'], vec![b'A', b'C', b'B']]);
-    let result = problem.evaluate(&[1, 0, 1]); // "AC"
-    assert!(result.is_valid());
-    assert_eq!(result.unwrap(), 2);
+fn test_lcs_evaluate_issue_yes() {
+    let problem = issue_yes_instance();
+    assert!(problem.evaluate(&[0, 1, 0]));
+    assert!(!problem.evaluate(&[1, 1, 0]));
 }
 
 #[test]
-fn test_lcs_evaluate_invalid_subsequence() {
-    // s1 = "ABC", s2 = "CAB"
-    // Selecting positions 1,2 of s1 gives "BC" - is "BC" a subseq of "CAB"? No
-    let problem =
-        LongestCommonSubsequence::new(vec![vec![b'A', b'B', b'C'], vec![b'C', b'A', b'B']]);
-    let result = problem.evaluate(&[0, 1, 1]); // "BC"
-    assert!(!result.is_valid());
+fn test_lcs_evaluate_issue_no() {
+    let problem = issue_no_instance();
+    assert!(!problem.evaluate(&[0]));
+    assert!(!problem.evaluate(&[1]));
 }
 
 #[test]
-fn test_lcs_evaluate_empty_selection() {
-    let problem =
-        LongestCommonSubsequence::new(vec![vec![b'A', b'B', b'C'], vec![b'X', b'Y', b'Z']]);
-    let result = problem.evaluate(&[0, 0, 0]); // empty
-    assert!(result.is_valid());
-    assert_eq!(result.unwrap(), 0);
+fn test_lcs_out_of_range_symbol() {
+    let problem = LongestCommonSubsequence::new(2, vec![vec![0, 1, 0], vec![1, 0, 1]], 3);
+    assert!(!problem.evaluate(&[0, 2, 1]));
 }
 
 #[test]
-fn test_lcs_evaluate_wrong_config_length() {
-    let problem = LongestCommonSubsequence::new(vec![vec![b'A', b'B'], vec![b'A', b'B', b'C']]);
-    assert!(!problem.evaluate(&[1]).is_valid());
-    assert!(!problem.evaluate(&[1, 0, 0]).is_valid());
+fn test_lcs_wrong_length() {
+    let problem = LongestCommonSubsequence::new(2, vec![vec![0, 1, 0], vec![1, 0, 1]], 3);
+    assert!(!problem.evaluate(&[0, 1]));
+    assert!(!problem.evaluate(&[0, 1, 0, 1]));
 }
 
 #[test]
-fn test_lcs_evaluate_invalid_variable_value() {
-    let problem = LongestCommonSubsequence::new(vec![vec![b'A', b'B'], vec![b'A', b'B']]);
-    assert!(!problem.evaluate(&[2, 0]).is_valid());
-}
-
-#[test]
-fn test_lcs_brute_force_two_strings() {
-    // s1 = "ABAC", s2 = "BACA"
-    // LCS = "BAC" or "AAC" or "ABA", length 3
-    let problem = LongestCommonSubsequence::new(vec![
-        vec![b'A', b'B', b'A', b'C'],
-        vec![b'B', b'A', b'C', b'A'],
-    ]);
+fn test_lcs_bruteforce_yes() {
+    let problem = issue_yes_instance();
     let solver = BruteForce::new();
-    let solution = solver.find_best(&problem).expect("should find a solution");
-    let metric = problem.evaluate(&solution);
-    assert!(metric.is_valid());
-    assert_eq!(metric.unwrap(), 3);
+    let solution = solver
+        .find_satisfying(&problem)
+        .expect("expected a common subsequence witness");
+    assert!(problem.evaluate(&solution));
 }
 
 #[test]
-fn test_lcs_identical_strings() {
-    let problem =
-        LongestCommonSubsequence::new(vec![vec![b'A', b'B', b'C'], vec![b'A', b'B', b'C']]);
+fn test_lcs_bruteforce_no() {
+    let problem = issue_no_instance();
     let solver = BruteForce::new();
-    let solution = solver.find_best(&problem).expect("should find a solution");
-    let metric = problem.evaluate(&solution);
-    assert_eq!(metric.unwrap(), 3);
+    assert!(solver.find_satisfying(&problem).is_none());
 }
 
 #[test]
-fn test_lcs_no_common_chars() {
-    let problem = LongestCommonSubsequence::new(vec![vec![b'A', b'B'], vec![b'C', b'D']]);
+fn test_lcs_find_all_satisfying_contains_issue_witness() {
+    let problem = issue_yes_instance();
     let solver = BruteForce::new();
-    let solution = solver.find_best(&problem).expect("should find a solution");
-    let metric = problem.evaluate(&solution);
-    assert_eq!(metric.unwrap(), 0);
+    let satisfying = solver.find_all_satisfying(&problem);
+    assert!(satisfying.iter().any(|config| config == &vec![0, 1, 0]));
 }
 
 #[test]
-fn test_lcs_single_char_alphabet() {
-    // All same character - LCS is length of shortest string
-    let problem = LongestCommonSubsequence::new(vec![vec![b'A', b'A', b'A'], vec![b'A', b'A']]);
-    let solver = BruteForce::new();
-    let solution = solver.find_best(&problem).expect("should find a solution");
-    let metric = problem.evaluate(&solution);
-    assert_eq!(metric.unwrap(), 2);
+fn test_lcs_empty_bound() {
+    let problem = LongestCommonSubsequence::new(1, vec![vec![0, 0, 0], vec![0, 0]], 0);
+    assert_eq!(problem.dims(), Vec::<usize>::new());
+    assert_eq!(problem.sum_triangular_lengths(), 9);
+    assert_eq!(problem.num_transitions(), 0);
+    assert!(problem.evaluate(&[]));
 }
 
 #[test]
-fn test_lcs_three_strings() {
-    // Example from issue #108
-    let problem = LongestCommonSubsequence::new(vec![
-        vec![b'A', b'B', b'C', b'D', b'A', b'B'],
-        vec![b'B', b'D', b'C', b'A', b'B', b'A'],
-        vec![b'B', b'C', b'A', b'D', b'B', b'A'],
-    ]);
+fn test_lcs_paper_example() {
+    let problem = issue_yes_instance();
+    assert!(problem.evaluate(&[0, 1, 0]));
+
     let solver = BruteForce::new();
-    let solution = solver.find_best(&problem).expect("should find a solution");
-    let metric = problem.evaluate(&solution);
-    assert!(metric.is_valid());
-    assert_eq!(metric.unwrap(), 4); // "BCAB" or equivalent
+    let satisfying = solver.find_all_satisfying(&problem);
+    assert!(!satisfying.is_empty());
 }
 
 #[test]
 fn test_lcs_serialization() {
-    let problem =
-        LongestCommonSubsequence::new(vec![vec![b'A', b'B', b'C'], vec![b'A', b'C', b'B']]);
+    let problem = issue_yes_instance();
     let json = serde_json::to_value(&problem).unwrap();
     let restored: LongestCommonSubsequence = serde_json::from_value(json).unwrap();
+    assert_eq!(restored.alphabet_size(), problem.alphabet_size());
     assert_eq!(restored.strings(), problem.strings());
+    assert_eq!(restored.bound(), problem.bound());
 }
 
 #[test]
-fn test_lcs_empty_string_in_input() {
-    let problem = LongestCommonSubsequence::new(vec![vec![], vec![b'A', b'B', b'C']]);
-    assert_eq!(problem.dims(), Vec::<usize>::new());
-    assert!(problem.evaluate(&[]).is_valid());
-    assert_eq!(problem.evaluate(&[]).unwrap(), 0);
+#[should_panic(expected = "alphabet_size must be > 0 when bound > 0")]
+fn test_lcs_zero_alphabet_with_positive_bound_panics() {
+    LongestCommonSubsequence::new(0, vec![vec![]], 1);
 }
 
 #[test]
-#[should_panic(expected = "LCS requires at least 2 strings")]
-fn test_lcs_single_string_panics() {
-    LongestCommonSubsequence::new(vec![vec![b'A', b'B']]);
+#[should_panic(expected = "input symbols must be less than alphabet_size")]
+fn test_lcs_symbol_out_of_range_panics() {
+    LongestCommonSubsequence::new(2, vec![vec![0, 2]], 1);
 }
diff --git a/src/unit_tests/rules/longestcommonsubsequence_ilp.rs b/src/unit_tests/rules/longestcommonsubsequence_ilp.rs
index 7762d2349..90cf2aa71 100644
--- a/src/unit_tests/rules/longestcommonsubsequence_ilp.rs
+++ b/src/unit_tests/rules/longestcommonsubsequence_ilp.rs
@@ -1,163 +1,83 @@
 use super::*;
+use crate::models::algebraic::ILP;
 use crate::solvers::{BruteForce, ILPSolver, Solver};
 use crate::traits::Problem;
 
 #[test]
-fn test_lcs_to_ilp_issue_example() {
-    // From issue #110: s1 = "ABAC", s2 = "BACA"
-    let problem = LongestCommonSubsequence::new(vec![
-        vec![b'A', b'B', b'A', b'C'],
-        vec![b'B', b'A', b'C', b'A'],
-    ]);
+fn test_lcs_to_ilp_yes_instance() {
+    let problem = LongestCommonSubsequence::new(3, vec![vec![0, 1, 2], vec![1, 0, 2]], 2);
     let reduction: ReductionLCSToILP = ReduceTo::<ILP<bool>>::reduce_to(&problem);
     let ilp = reduction.target_problem();
 
-    // 6 match pairs as described in the issue
-    assert_eq!(ilp.num_vars, 6);
+    assert_eq!(ilp.num_vars, 18);
 
-    // Solve ILP
     let ilp_solver = ILPSolver::new();
-    let ilp_solution = ilp_solver.solve(ilp).expect("ILP should be solvable");
-
-    // Extract solution back to LCS config
+    let ilp_solution = ilp_solver.solve(ilp).expect("ILP should be feasible");
     let extracted = reduction.extract_solution(&ilp_solution);
 
-    // Verify the solution is valid and optimal (length 3)
-    let metric = problem.evaluate(&extracted);
-    assert!(metric.is_valid());
-    assert_eq!(metric.unwrap(), 3);
-}
-
-#[test]
-fn test_lcs_to_ilp_closed_loop() {
-    // Compare brute force LCS with ILP-based solution
-    let problem = LongestCommonSubsequence::new(vec![
-        vec![b'A', b'B', b'A', b'C'],
-        vec![b'B', b'A', b'C', b'A'],
-    ]);
-
-    // Brute force optimal
-    let bf = BruteForce::new();
-    let bf_solution = bf.find_best(&problem).expect("should find a solution");
-    let bf_metric = problem.evaluate(&bf_solution);
-    assert!(bf_metric.is_valid());
-    let bf_value = bf_metric.unwrap();
-
-    // ILP optimal
-    let reduction: ReductionLCSToILP = ReduceTo::<ILP<bool>>::reduce_to(&problem);
-    let ilp = reduction.target_problem();
-    let ilp_solver = ILPSolver::new();
-    let ilp_solution = ilp_solver.solve(ilp).expect("ILP should be solvable");
-    let extracted = reduction.extract_solution(&ilp_solution);
-    let ilp_metric = problem.evaluate(&extracted);
-    assert!(ilp_metric.is_valid());
-    let ilp_value = ilp_metric.unwrap();
-
-    // Both should give the same optimal value
-    assert_eq!(
-        bf_value, ilp_value,
-        "BF optimal {} != ILP optimal {}",
-        bf_value, ilp_value
-    );
+    assert_eq!(extracted.len(), problem.bound());
+    assert!(problem.evaluate(&extracted));
 }
 
 #[test]
-fn test_lcs_to_ilp_identical_strings() {
-    // LCS of identical strings = the string itself
-    let problem =
-        LongestCommonSubsequence::new(vec![vec![b'A', b'B', b'C'], vec![b'A', b'B', b'C']]);
+fn test_lcs_to_ilp_no_instance() {
+    let problem = LongestCommonSubsequence::new(2, vec![vec![0, 1], vec![1, 0]], 2);
     let reduction: ReductionLCSToILP = ReduceTo::<ILP<bool>>::reduce_to(&problem);
     let ilp = reduction.target_problem();
 
     let ilp_solver = ILPSolver::new();
-    let ilp_solution = ilp_solver.solve(ilp).expect("ILP should be solvable");
-    let extracted = reduction.extract_solution(&ilp_solution);
-
-    let metric = problem.evaluate(&extracted);
-    assert!(metric.is_valid());
-    assert_eq!(metric.unwrap(), 3);
+    assert!(ilp_solver.solve(ilp).is_none());
 }
 
 #[test]
-fn test_lcs_to_ilp_no_common_chars() {
-    let problem = LongestCommonSubsequence::new(vec![vec![b'A', b'B'], vec![b'C', b'D']]);
-    let reduction: ReductionLCSToILP = ReduceTo::<ILP<bool>>::reduce_to(&problem);
-    let ilp = reduction.target_problem();
-
-    // No match pairs → 0 variables
-    assert_eq!(ilp.num_vars, 0);
-
-    let ilp_solver = ILPSolver::new();
-    let ilp_solution = ilp_solver.solve(ilp).expect("ILP should be solvable");
-    let extracted = reduction.extract_solution(&ilp_solution);
-
-    let metric = problem.evaluate(&extracted);
-    assert!(metric.is_valid());
-    assert_eq!(metric.unwrap(), 0);
-}
+fn test_lcs_to_ilp_closed_loop_three_strings() {
+    let problem = LongestCommonSubsequence::new(
+        2,
+        vec![vec![0, 1, 0], vec![1, 0, 1, 0], vec![0, 0, 1, 0]],
+        2,
+    );
 
-#[test]
-fn test_lcs_to_ilp_single_char_alphabet() {
-    // All same chars → LCS = min length
-    let problem = LongestCommonSubsequence::new(vec![vec![b'A', b'A', b'A'], vec![b'A', b'A']]);
     let reduction: ReductionLCSToILP = ReduceTo::<ILP<bool>>::reduce_to(&problem);
     let ilp = reduction.target_problem();
 
     let ilp_solver = ILPSolver::new();
-    let ilp_solution = ilp_solver.solve(ilp).expect("ILP should be solvable");
+    let ilp_solution = ilp_solver.solve(ilp).expect("ILP should be feasible");
     let extracted = reduction.extract_solution(&ilp_solution);
 
-    let metric = problem.evaluate(&extracted);
-    assert!(metric.is_valid());
-    assert_eq!(metric.unwrap(), 2);
+    assert!(problem.evaluate(&extracted));
+
+    let brute_force = BruteForce::new();
+    let witness = brute_force
+        .find_satisfying(&problem)
+        .expect("bruteforce should also find a witness");
+    assert!(problem.evaluate(&witness));
 }
 
 #[test]
-fn test_lcs_to_ilp_asymmetric_lengths() {
-    // s1 = "AB", s2 = "AABB"
-    let problem =
-        LongestCommonSubsequence::new(vec![vec![b'A', b'B'], vec![b'A', b'A', b'B', b'B']]);
-
-    // BF optimal
-    let bf = BruteForce::new();
-    let bf_solution = bf.find_best(&problem).unwrap();
-    let bf_value = problem.evaluate(&bf_solution).unwrap();
-
-    // ILP optimal
+fn test_lcs_to_ilp_extracts_exact_witness_symbols() {
+    let problem = LongestCommonSubsequence::new(2, vec![vec![0, 1, 0], vec![1, 0, 1, 0]], 2);
     let reduction: ReductionLCSToILP = ReduceTo::<ILP<bool>>::reduce_to(&problem);
     let ilp = reduction.target_problem();
+
     let ilp_solver = ILPSolver::new();
-    let ilp_solution = ilp_solver.solve(ilp).unwrap();
+    let ilp_solution = ilp_solver.solve(ilp).expect("ILP should be feasible");
     let extracted = reduction.extract_solution(&ilp_solution);
-    let ilp_value = problem.evaluate(&extracted).unwrap();
 
-    assert_eq!(bf_value, ilp_value);
-    assert_eq!(ilp_value, 2); // "AB" is subseq of both
+    assert_eq!(extracted.len(), 2);
+    assert!(extracted.iter().all(|&symbol| symbol < 2));
+    assert!(problem.evaluate(&extracted));
 }
 
 #[test]
-fn test_lcs_to_ilp_constraint_structure() {
-    // Verify basic ILP structure for a small example
-    let problem = LongestCommonSubsequence::new(vec![vec![b'A', b'B'], vec![b'B', b'A']]);
+fn test_lcs_to_ilp_zero_bound() {
+    let problem = LongestCommonSubsequence::new(1, vec![vec![0, 0], vec![0]], 0);
     let reduction: ReductionLCSToILP = ReduceTo::<ILP<bool>>::reduce_to(&problem);
     let ilp = reduction.target_problem();
 
-    // Match pairs: (0,1)=A, (1,0)=B → 2 variables
-    assert_eq!(ilp.num_vars, 2);
-
-    // Constraints:
-    // - s1 pos 0: m_{0,1} <= 1 (1 constraint)
-    // - s1 pos 1: m_{1,0} <= 1 (1 constraint)
-    // - s2 pos 0: m_{1,0} <= 1 (1 constraint)
-    // - s2 pos 1: m_{0,1} <= 1 (1 constraint)
-    // - Crossing: j1=0 < j1'=1 and j2=1 > j2'=0 → m_{0,1} + m_{1,0} <= 1 (1 constraint)
-    // Total: 5
-    assert_eq!(ilp.constraints.len(), 5);
-
-    // Optimal: can only pick one of the two → LCS length 1
     let ilp_solver = ILPSolver::new();
-    let ilp_solution = ilp_solver.solve(ilp).unwrap();
+    let ilp_solution = ilp_solver.solve(ilp).expect("ILP should be feasible");
     let extracted = reduction.extract_solution(&ilp_solution);
-    let metric = problem.evaluate(&extracted);
-    assert_eq!(metric.unwrap(), 1);
+
+    assert_eq!(extracted, Vec::<usize>::new());
+    assert!(problem.evaluate(&extracted));
 }