Fix #298: [Model] LengthBoundedDisjointPaths

docs/paper/reductions.typ

@@ -67,6 +67,7 @@
   "MaxCut": [Max-Cut],
   "GraphPartitioning": [Graph Partitioning],
   "HamiltonianPath": [Hamiltonian Path],
+  "LengthBoundedDisjointPaths": [Length-Bounded Disjoint Paths],
   "IsomorphicSpanningTree": [Isomorphic Spanning Tree],
   "KColoring": [$k$-Coloring],
   "MinimumDominatingSet": [Minimum Dominating Set],
@@ -531,6 +532,67 @@ Graph Partitioning is a core NP-hard problem arising in VLSI design, parallel co
   caption: [Graph with $n = 6$ vertices partitioned into $A = {v_0, v_1, v_2}$ (blue) and $B = {v_3, v_4, v_5}$ (red). The 3 crossing edges $(v_1, v_3)$, $(v_2, v_3)$, $(v_2, v_4)$ are shown in bold red; internal edges are gray.],
 ) <fig:graph-partitioning>
 ]
+#{
+  let x = load-model-example("LengthBoundedDisjointPaths")
+  let nv = graph-num-vertices(x.instance)
+  let ne = graph-num-edges(x.instance)
+  let edges = x.instance.graph.inner.edges.map(e => (e.at(0), e.at(1)))
+  let s = x.instance.source
+  let t = x.instance.sink
+  let J = x.instance.num_paths_required
+  let K = x.instance.max_length
+  let chosen-verts = (0, 1, 2, 3, 6)
+  let chosen-edges = ((0, 1), (1, 6), (0, 2), (2, 3), (3, 6))
+  [
+    #problem-def("LengthBoundedDisjointPaths")[
+      Given an undirected graph $G = (V, E)$, distinct terminals $s, t in V$, and positive integers $J, K$, determine whether $G$ contains at least $J$ pairwise internally vertex-disjoint paths from $s$ to $t$, each using at most $K$ edges.
+    ][
+      Length-Bounded Disjoint Paths is the bounded-routing version of the classical disjoint-path problem, with applications in network routing and VLSI where multiple connections must fit simultaneously under quality-of-service limits. Garey & Johnson list it as ND41 and summarize the sharp threshold proved by Itai, Perl, and Shiloach: the problem is NP-complete for every fixed $K >= 5$, polynomial-time solvable for $K <= 4$, and becomes polynomial again when the length bound is removed entirely @garey1979. The implementation here uses the natural $J dot |V|$ binary membership encoding, so brute-force search over configurations runs in $O^*(2^(J dot |V|))$.
+
+      *Example.* Consider the graph $G$ with $n = #nv$ vertices, $|E| = #ne$ edges, terminals $s = v_#s$, $t = v_#t$, $J = #J$, and $K = #K$. The two paths $P_1 = v_0 arrow v_1 arrow v_6$ and $P_2 = v_0 arrow v_2 arrow v_3 arrow v_6$ are both of length at most 3, and their internal vertex sets ${v_1}$ and ${v_2, v_3}$ are disjoint. Hence this instance is satisfying. The third branch $v_0 arrow v_4 arrow v_5 arrow v_6$ is available but unused, so the instance has multiple satisfying path-slot assignments.
+
+      #figure(
+        canvas(length: 1cm, {
+          let blue = graph-colors.at(0)
+          let gray = luma(180)
+          let verts = (
+            (0, 1),    // v0 = s
+            (1.3, 1.8),
+            (1.3, 1.0),
+            (2.6, 1.0),
+            (1.3, 0.2),
+            (2.6, 0.2),
+            (3.9, 1),  // v6 = t
+          )
+          for (u, v) in edges {
+            let selected = chosen-edges.any(e =>
+              (e.at(0) == u and e.at(1) == v) or (e.at(0) == v and e.at(1) == u)
+            )
+            g-edge(verts.at(u), verts.at(v),
+              stroke: if selected { 2pt + blue } else { 1pt + gray })
+          }
+          for (k, pos) in verts.enumerate() {
+            let active = chosen-verts.contains(k)
+            g-node(pos, name: "v" + str(k),
+              fill: if active { blue } else { white },
+              label: if active {
+                text(fill: white)[
+                  #if k == s { $s$ }
+                  else if k == t { $t$ }
+                  else { $v_#k$ }
+                ]
+              } else [
+                #if k == s { $s$ }
+                else if k == t { $t$ }
+                else { $v_#k$ }
+              ])
+          }
+        }),
+        caption: [A satisfying Length-Bounded Disjoint Paths instance with $s = v_0$, $t = v_6$, $J = 2$, and $K = 3$. The highlighted paths are $v_0 arrow v_1 arrow v_6$ and $v_0 arrow v_2 arrow v_3 arrow v_6$; the lower branch through $v_4, v_5$ remains unused.],
+      ) <fig:length-bounded-disjoint-paths>
+    ]
+  ]
+}
 #{
   let x = load-model-example("HamiltonianPath")
   let nv = graph-num-vertices(x.instance)

docs/src/cli.md

@@ -15,7 +15,8 @@ Or build from source:
 ```bash
 git clone https://github.com/CodingThrust/problem-reductions
 cd problem-reductions
-make cli    # builds target/release/pred
+cargo build -p problemreductions-cli --release   # builds target/release/pred
+cargo install --path problemreductions-cli       # optional: installs `pred` to ~/.cargo/bin
 ```
 
 Verify the installation:
@@ -24,6 +25,12 @@ Verify the installation:
 pred --version
 ```
 
+For a workspace-local run without installing globally, use:
+
+```bash
+cargo run -p problemreductions-cli --bin pred -- --version
+```
+
 ### ILP Backend
 
 The default ILP backend is HiGHS. To use a different backend:
@@ -48,6 +55,9 @@ pred create MIS --graph 0-1,1-2,2-3 --weights 3,1,2,1 -o weighted.json
 # Create a Steiner Tree instance
 pred create SteinerTree --graph 0-1,0-3,1-2,1-3,2-3,2-4,3-4 --edge-weights 2,5,2,1,5,6,1 --terminals 0,2,4 -o steiner.json
 
+# Create a Length-Bounded Disjoint Paths instance
+pred create LengthBoundedDisjointPaths --graph 0-1,1-6,0-2,2-3,3-6,0-4,4-5,5-6 --source 0 --sink 6 --num-paths-required 2 --bound 3 -o lbdp.json
+
 # Or start from a canonical model example
 pred create --example MIS/SimpleGraph/i32 -o example.json
 
@@ -57,12 +67,18 @@ pred create --example MVC/SimpleGraph/i32 --to MIS/SimpleGraph/i32 -o example.js
 # Inspect what's inside a problem file
 pred inspect problem.json
 
+# Inspect the new path problem
+pred inspect lbdp.json
+
 # Solve it (auto-reduces to ILP)
 pred solve problem.json
 
 # Or solve with brute-force
 pred solve problem.json --solver brute-force
 
+# LengthBoundedDisjointPaths currently needs brute-force
+pred solve lbdp.json --solver brute-force
+
 # Evaluate a specific configuration (shows Valid(N) or Invalid)
 pred evaluate problem.json --config 1,0,1,0
 
@@ -276,12 +292,16 @@ pred create KColoring --k 3 --graph 0-1,1-2,2-0 -o kcol.json
 pred create SpinGlass --graph 0-1,1-2 -o sg.json
 pred create MaxCut --graph 0-1,1-2,2-0 -o maxcut.json
 pred create SteinerTree --graph 0-1,0-3,1-2,1-3,2-3,2-4,3-4 --edge-weights 2,5,2,1,5,6,1 --terminals 0,2,4 -o steiner.json
+pred create LengthBoundedDisjointPaths --graph 0-1,1-6,0-2,2-3,3-6,0-4,4-5,5-6 --source 0 --sink 6 --num-paths-required 2 --bound 3 -o lbdp.json
 pred create Factoring --target 15 --bits-m 4 --bits-n 4 -o factoring.json
 pred create Factoring --target 21 --bits-m 3 --bits-n 3 -o factoring2.json
 pred create X3C --universe 9 --sets "0,1,2;0,2,4;3,4,5;3,5,7;6,7,8;1,4,6;2,5,8" -o x3c.json
 pred create MinimumTardinessSequencing --n 5 --deadlines 5,5,5,3,3 --precedence-pairs "0>3,1>3,1>4,2>4" -o mts.json
 ```
 
+For `LengthBoundedDisjointPaths`, the CLI flag `--bound` maps to the JSON field
+`max_length`.
+
 Canonical examples are useful when you want a known-good instance from the paper/example database.
 For model examples, `pred create --example <PROBLEM_SPEC>` emits the canonical instance for that
 graph node.
@@ -418,8 +438,9 @@ Source evaluation: Valid(2)
 ```
 
 > **Note:** The ILP solver requires a reduction path from the target problem to ILP.
-> Some problems (e.g., QUBO, SpinGlass, MaxCut, CircuitSAT) do not have this path yet.
-> Use `--solver brute-force` for these, or reduce to a problem that supports ILP first.
+> `LengthBoundedDisjointPaths` does not currently have one, so use
+> `pred solve lbdp.json --solver brute-force`.
+> For other problems, use `pred path <PROBLEM> ILP` to check whether an ILP reduction path exists.
 
 ## Shell Completions
 

docs/src/reductions/problem_schemas.json

@@ -259,6 +259,37 @@
       }
     ]
   },
+  {
+    "name": "LengthBoundedDisjointPaths",
+    "description": "Find J internally vertex-disjoint s-t paths of length at most K",
+    "fields": [
+      {
+        "name": "graph",
+        "type_name": "G",
+        "description": "The underlying graph G=(V,E)"
+      },
+      {
+        "name": "source",
+        "type_name": "usize",
+        "description": "The shared source vertex s"
+      },
+      {
+        "name": "sink",
+        "type_name": "usize",
+        "description": "The shared sink vertex t"
+      },
+      {
+        "name": "num_paths_required",
+        "type_name": "usize",
+        "description": "Required number J of disjoint s-t paths"
+      },
+      {
+        "name": "max_length",
+        "type_name": "usize",
+        "description": "Maximum path length K in edges"
+      }
+    ]
+  },
   {
     "name": "LongestCommonSubsequence",
     "description": "Find the longest string that is a subsequence of every input string",