CodingThrust
diff --git a/‎.claude/CLAUDE.md‎
Lines changed: 3 additions & 0 deletions b/‎.claude/CLAUDE.md‎
Lines changed: 3 additions & 0 deletions
diff --git a/‎docs/paper/reductions.typ‎
Lines changed: 526 additions & 9 deletions b/‎docs/paper/reductions.typ‎
Lines changed: 526 additions & 9 deletions
diff --git a/‎docs/paper/references.bib‎
Lines changed: 33 additions & 0 deletions b/‎docs/paper/references.bib‎
Lines changed: 33 additions & 0 deletions
diff --git a/‎problemreductions-cli/tests/cli_tests.rs‎
Lines changed: 12 additions & 4 deletions b/‎problemreductions-cli/tests/cli_tests.rs‎
Lines changed: 12 additions & 4 deletions
@@ -176,6 +176,7 @@ impl ReduceTo<Target> for Source { ... }
 - Expression strings are parsed at compile time by a Pratt parser in the proc macro crate
 - Variable names are validated against actual getter methods on the source type — typos cause compile errors
 - Each problem type provides inherent getter methods (e.g., `num_vertices()`, `num_edges()`) that the overhead expressions reference
+- **Overhead expressions describe scaling (asymptotic upper bounds), not exact sizes.** To determine the actual target problem size for a specific instance, read the `reduce_to()` construction code and count the actual variables/constraints/vertices built.
 - `ReductionOverhead` stores `Vec<(&'static str, Expr)>` — field name to symbolic expression mappings
 - `ReductionEntry` has both symbolic (`overhead_fn`) and compiled (`overhead_eval_fn`) evaluation — the compiled version calls getters directly
 - `VariantEntry` has both a complexity string and compiled `complexity_eval_fn` — same pattern
@@ -226,6 +227,8 @@ Reduction graph nodes use variant key-value pairs from `Problem::variant()`:
 
 ## Testing Requirements
 
+**No single test should take more than 5 seconds.** If a test requires solving a large instance (e.g., ILP with thousands of variables), use a smaller test instance or a faster solver. Tests that exceed 5s block CI and must be refactored.
+
 **Reference implementations — read these first:**
 - **Reduction test:** `src/unit_tests/rules/minimumvertexcover_maximumindependentset.rs` — closed-loop pattern
 - **Model test:** `src/unit_tests/models/graph/maximum_independent_set.rs` — evaluation, serialization
 
@@ -164,6 +164,17 @@ @article{brucker1977
   doi     = {10.1016/S0167-5060(08)70743-X}
 }
 
+@incollection{brucker1978clustering,
+  author    = {Peter Brucker},
+  title     = {On the Complexity of Clustering Problems},
+  booktitle = {Optimization and Operations Research},
+  series    = {Lecture Notes in Economics and Mathematical Systems},
+  volume    = {157},
+  pages     = {45--54},
+  publisher = {Springer},
+  year      = {1978}
+}
+
 @article{lawler1977,
   author  = {Eugene L. Lawler},
   title   = {A pseudopolynomial algorithm for sequencing jobs to minimize total tardiness},
@@ -242,6 +253,28 @@ @book{garey1979
   year      = {1979}
 }
 
+@article{orlin1977,
+  author  = {James B. Orlin},
+  title   = {Contentment in Graph Theory: Covering Graphs with Cliques},
+  journal = {Indagationes Mathematicae (Proceedings)},
+  volume  = {80},
+  number  = {5},
+  pages   = {406--424},
+  year    = {1977},
+  doi     = {10.1016/1385-7258(77)90055-5}
+}
+
+@article{kouStockmeyerWong1978,
+  author  = {Lawrence T. Kou and Larry J. Stockmeyer and C. K. Wong},
+  title   = {Covering Edges by Cliques with Regard to Keyword Conflicts and Intersection Graphs},
+  journal = {Communications of the ACM},
+  volume  = {21},
+  number  = {2},
+  pages   = {135--139},
+  year    = {1978},
+  doi     = {10.1145/359340.359346}
+}
+
 @article{galilMegiddo1977,
   author  = {Zvi Galil and Nimrod Megiddo},
   title   = {Cyclic Ordering is NP-Complete},
 
@@ -7642,7 +7642,15 @@ fn test_show_ksat_works() {
 fn test_path_all_max_paths_truncates() {
     // With --max-paths 3, should limit to 3 paths and indicate truncation
     let output = pred()
-        .args(["path", "MIS", "QUBO", "--all", "--max-paths", "3", "--json"])
+        .args([
+            "path",
+            "KSat",
+            "QUBO",
+            "--all",
+            "--max-paths",
+            "3",
+            "--json",
+        ])
         .output()
         .unwrap();
     assert!(
@@ -7661,17 +7669,17 @@ fn test_path_all_max_paths_truncates() {
         paths.len()
     );
     assert_eq!(envelope["max_paths"], 3);
-    // MIS -> QUBO has many paths, so truncation is expected
+    // KSat -> QUBO has many paths, so truncation is expected
     assert_eq!(
         envelope["truncated"], true,
-        "should be truncated since MIS->QUBO has many paths"
+        "should be truncated since KSat->QUBO has many paths"
     );
 }
 
 #[test]
 fn test_path_all_max_paths_text_truncation_note() {
     let output = pred()
-        .args(["path", "MIS", "QUBO", "--all", "--max-paths", "2"])
+        .args(["path", "KSat", "QUBO", "--all", "--max-paths", "2"])
         .output()
         .unwrap();
     assert!(output.status.success());