Replace reduction size contracts and add path size reporting (#1130)

* feat: add exact symbolic size maps

* feat: add certified symbolic size bounds

* feat: replace reduction size metadata with explicit contracts

* fix: separate symbolic path discovery from size contracts

* refactor: simplify symbolic path reporting

* feat: execute path analysis on complete instances

* docs: simplify reduction prompt language

* docs: simplify user-facing size analysis language

* refactor: remove undefined coefficient size field

* fix: unify symbolic path reporting

* test: align LongestCircuit MCP expectations

Author: isPANN

Makefile

@@ -295,17 +295,12 @@ cli-demo: cli
 	$$PRED from QUBO --hops 1; \
 	\
 	echo ""; \
-	echo "--- 5. path: asymptotic Pareto front ---"; \
+	echo "--- 5. path: symbolic path enumeration ---"; \
 	$$PRED path MIS QUBO; \
 	$$PRED path Factoring SpinGlass; \
-	echo "--- 5b. explicitly choose one semantic route from the Pareto front ---"; \
-	$$PRED path MIS QUBO -o $(CLI_DEMO_DIR)/front_mis_qubo.json; \
-	jq -e 'first(.front[] | select(([.path[0].from.name] + [.path[].to.name]) == ["MaximumIndependentSet", "MaximumIndependentSet", "MaximumSetPacking", "MaximumSetPacking", "QUBO"]))' $(CLI_DEMO_DIR)/front_mis_qubo.json > $(CLI_DEMO_DIR)/path_mis_qubo.json; \
-	\
-	echo ""; \
-	echo "--- 6. path --all: enumerate all paths ---"; \
-	$$PRED path MIS QUBO --all; \
-	$$PRED path MIS QUBO --all -o $(CLI_DEMO_DIR)/all_paths/; \
+	echo "--- 5b. explicitly choose one route from the path set ---"; \
+	$$PRED path MIS QUBO -o $(CLI_DEMO_DIR)/paths_mis_qubo.json; \
+	jq -e 'first(.paths[] | select(([.path[0].from.name] + [.path[].to.name]) == ["MaximumIndependentSet", "MaximumIndependentSet", "MaximumSetPacking", "MaximumSetPacking", "QUBO"]))' $(CLI_DEMO_DIR)/paths_mis_qubo.json > $(CLI_DEMO_DIR)/path_mis_qubo.json; \
 	\
 	echo ""; \
 	echo "--- 7. export-graph: full reduction graph ---"; \
@@ -314,7 +309,7 @@ cli-demo: cli
 	echo ""; \
 	echo "--- 8. create: build problem instances ---"; \
 	$$PRED create MIS --graph 0-1,1-2,2-3,3-4,4-0 -o $(CLI_DEMO_DIR)/mis.json; \
-	$$PRED create MIS --graph 0-1,1-2,2-3 --weights 2,1,3,1 -o $(CLI_DEMO_DIR)/mis_weighted.json; \
+	$$PRED create MaximumIndependentSet/SimpleGraph/i32 --graph 0-1,1-2,2-3 --weights 2,1,3,1 -o $(CLI_DEMO_DIR)/mis_weighted.json; \
 	$$PRED create SAT --num-vars 3 --clauses "1,2;-1,3;2,-3" -o $(CLI_DEMO_DIR)/sat.json; \
 	$$PRED create 3SAT --num-vars 4 --clauses "1,2,3;-1,2,-3;1,-2,3" -o $(CLI_DEMO_DIR)/3sat.json; \
 	$$PRED create QUBO --matrix "1,-0.5;-0.5,2" -o $(CLI_DEMO_DIR)/qubo.json; \
@@ -347,7 +342,7 @@ cli-demo: cli
 	$$PRED solve $(CLI_DEMO_DIR)/mis_weighted.json; \
 	\
 	echo ""; \
-	echo "--- 13. reduce: MIS → QUBO along the chosen Pareto route ---"; \
+	echo "--- 13. reduce: MIS → QUBO along the explicitly chosen route ---"; \
 	$$PRED reduce $(CLI_DEMO_DIR)/mis.json --via $(CLI_DEMO_DIR)/path_mis_qubo.json -o $(CLI_DEMO_DIR)/bundle_qubo.json; \
 	\
 	echo ""; \
@@ -360,8 +355,8 @@ cli-demo: cli
 	\
 	echo ""; \
 	echo "--- 16. solve bundle with ILP: MIS → MVC → ILP ---"; \
-	$$PRED path MIS MVC -o $(CLI_DEMO_DIR)/front_mis_mvc.json; \
-	jq -e 'first(.front[] | select(([.path[0].from.name] + [.path[].to.name]) == ["MaximumIndependentSet", "MaximumIndependentSet", "MinimumVertexCover"]))' $(CLI_DEMO_DIR)/front_mis_mvc.json > $(CLI_DEMO_DIR)/path_mis_mvc.json; \
+	$$PRED path MIS MVC -o $(CLI_DEMO_DIR)/paths_mis_mvc.json; \
+	jq -e 'first(.paths[] | select(([.path[0].from.name] + [.path[].to.name]) == ["MaximumIndependentSet", "MaximumIndependentSet", "MinimumVertexCover"]))' $(CLI_DEMO_DIR)/paths_mis_mvc.json > $(CLI_DEMO_DIR)/path_mis_mvc.json; \
 	$$PRED reduce $(CLI_DEMO_DIR)/mis.json --via $(CLI_DEMO_DIR)/path_mis_mvc.json -o $(CLI_DEMO_DIR)/bundle_mvc.json; \
 	$$PRED solve $(CLI_DEMO_DIR)/bundle_mvc.json --solver ilp; \
 	\

docs/agent-profiles/FEATURES.md

@@ -6,5 +6,5 @@
 - [Reduction Graph] — Automatic shortest-path search through registered reductions between problem types
 - [BruteForce Solver] — Enumerate all configurations to find optimal or satisfying solutions
 - [Variant System] — Graph/weight type parameterization with compile-time complexity registration
-- [Overhead System] — Symbolic expressions describing how target problem size relates to source after reduction
+- [Size Analysis] — Explain how problem size changes along a path and measure complete instances
 - [Serialization] — JSON schema export and serde-based serialization for all problem types

docs/agent-profiles/pred-sym-prof-yuki-tanaka.md

@@ -6,7 +6,7 @@ pred-sym (symbolic expression CLI)
 ## Use Case
 Three combined scenarios:
 1. **Complexity comparison** — Compare algorithm complexity expressions to determine asymptotic equivalence (e.g., O(n^2 + n) == O(n^2), O(n log n) != O(n^2)).
-2. **Reduction overhead audit** — Parse and simplify overhead expressions from reduction rules to verify they match expected growth (e.g., '3*num_vertices + num_edges^2').
+2. **Reduction size-contract audit** — Parse and simplify exact maps and certified bounds from reduction rules, and verify them against constructed examples.
 3. **Teaching complexity notation** — Use pred-sym as a learning/demonstration tool to explore how expressions simplify, evaluate at concrete sizes, and compare growth rates.
 
 ## Expected Outcome

docs/paper/reductions.typ

@@ -8,7 +8,8 @@
   target: e.target,
   source-name: graph-data.nodes.at(e.source).name,
   target-name: graph-data.nodes.at(e.target).name,
-  overhead: e.overhead,
+  size-fields: e.size_fields,
+  size-contract-error: e.size_contract_error,
 ))
 
 #let _edges-by-source-name = {
@@ -552,10 +553,14 @@
   if parts.len() > 0 { [#base (#parts.join(", "))] } else { base }
 }
 
-// Format overhead fields as inline text
-#let format-overhead(overhead) = {
-  let parts = overhead.map(o => raw(o.field + " = " + o.formula))
-  [_Overhead:_ #parts.join(", ").]
+// Format explicitly classified size fields as inline text.
+#let format-size-contract(fields) = {
+  let parts = fields.map(o => {
+    if o.contract == "exact" { raw(o.field + " = " + o.formula) }
+    else if o.contract == "bound-only" { raw(o.field + " <= " + o.formula) }
+    else { raw(o.field + " unavailable: " + o.reason) }
+  })
+  [_Size contract:_ #parts.join(", ").]
 }
 
 // Unified function for reduction rules: theorem + proof + optional example
@@ -576,15 +581,15 @@
                  else { display-name.at(target) }
   let src-lbl = label("def:" + source)
   let tgt-lbl = label("def:" + target)
-  let overhead = if edge != none and edge.overhead.len() > 0 { edge.overhead } else { none }
+  let size-fields = if edge != none and edge.size-fields.len() > 0 { edge.size-fields } else { none }
   let thm-lbl = label("thm:" + source + "-to-" + target)
   covered-rules.update(old => old + ((source, target),))
 
   [
     #v(1em)
     #theorem[
     *(*#context { if query(src-lbl).len() > 0 { link(src-lbl)[#src-disp] } else [#src-disp] }* #arrow *#context { if query(tgt-lbl).len() > 0 { link(tgt-lbl)[#tgt-disp] } else [#tgt-disp] }*)* #theorem-body
-    #if overhead != none { linebreak(); format-overhead(overhead) }
+    #if size-fields != none { linebreak(); format-size-contract(size-fields) }
   ] #thm-lbl]
 
   proof[#proof-body]
@@ -11426,10 +11431,10 @@ In all graph problems below, $G = (V, E)$ denotes an undirected graph with $|V|
 
 = Reductions <sec:reductions>
 
-Each reduction is presented as a *Rule* (with linked problem names and overhead from the graph data), followed by a *Proof* (construction, correctness, variable mapping, solution extraction), and optionally a *Concrete Example* (a small instance with verified solution). Problem names in the rule title link back to their definitions in @sec:problems.
+Each reduction is presented as a *Rule* (with linked problem names and explicit size contracts from the graph data), followed by a *Proof* (construction, correctness, variable mapping, solution extraction), and optionally a *Concrete Example* (a small instance with verified solution). Problem names in the rule title link back to their definitions in @sec:problems.
 
 The command blocks assume `route.json` contains the explicitly chosen direct route for
-the displayed rule, extracted from the corresponding `pred path` Pareto-front item.
+the displayed rule, extracted from the corresponding `pred path` entry.
 
 
 #let max2sat_mc = load-example("Maximum2Satisfiability", "MaxCut")
@@ -12110,7 +12115,7 @@ the displayed rule, extracted from the corresponding `pred path` Pareto-front it
       $ w_(i,p) = 2^p quad (0 <= p < L_i - 1), quad w_(i,L_i-1) = r_i + 1 - 2^(L_i - 1) $
       so that every bit vector represents an offset in ${0, dots, r_i}$. Then
       $ x_i = ell_i + sum_(p=0)^(L_i-1) w_(i,p) z_(i,p) $
-      and the total number of QUBO variables is $N = sum_i L_i$, exactly the exported overhead `num_vars = num_encoding_bits`.
+      and the total number of QUBO variables is $N = sum_i L_i$, exactly the exported size map `num_vars = num_encoding_bits`.
 
       Let $G = A^top A$ and $h = A^top bold(t)$. Writing $bold(x) = bold(ell) + B bold(z)$ for the encoding matrix $B in RR^(n times N)$ gives
       $ norm(A bold(x) - bold(t))_2^2 = bold(z)^top (B^top G B) bold(z) + 2 bold(z)^top B^top (G bold(ell) - h) + "const" $
@@ -16757,10 +16762,10 @@ See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples
 
 == Variant Cast Reductions
 
-Problems parameterized by graph type, weight type, or clause-width ($k$) admit identity reductions between specialised and general variants. Each cast preserves the problem structure exactly (same number of vertices/variables, same constraints), converting only the type parameter to a more general one. These are registered as self-edges in the reduction graph with identity overhead.
+Problems parameterized by graph type, weight type, or clause-width ($k$) admit identity reductions between specialised and general variants. Each cast preserves the problem structure exactly (same number of vertices/variables, same constraints), converting only the type parameter to a more general one. These are registered as self-edges in the reduction graph with exact identity size maps.
 
 #reduction-rule("MaximumIndependentSet", "MaximumIndependentSet")[
-  The graph hierarchy $"KingsSubgraph" subset "UnitDiskGraph" subset "SimpleGraph"$ and weight hierarchy $"One" subset ZZ subset RR$ induce identity-overhead casts between MIS variants. Graph casts discard geometric information (grid coordinates $arrow.r$ Euclidean coordinates $arrow.r$ adjacency list); weight casts embed unit weights into integers ($1 arrow.r 1_ZZ$) or integers into floats ($w arrow.r w_RR$). All edges and weights are preserved verbatim.
+  The graph hierarchy $"KingsSubgraph" subset "UnitDiskGraph" subset "SimpleGraph"$ and weight hierarchy $"One" subset ZZ subset RR$ induce exact identity size maps between MIS variants. Graph casts discard geometric information (grid coordinates $arrow.r$ Euclidean coordinates $arrow.r$ adjacency list); weight casts embed unit weights into integers ($1 arrow.r 1_ZZ$) or integers into floats ($w arrow.r w_RR$). All edges and weights are preserved verbatim.
 ][
   _Construction._ Given $"MIS"(G, bold(w))$ with graph type $G_"sub"$ and weight type $W_"sub"$, construct $"MIS"(G', bold(w)')$ where $G' = "cast"(G_"sub")$ lifts the graph to its parent type and $bold(w)' = "cast"(bold(w))$ lifts each weight. The `CastToParent` trait defines the concrete maps:
   - _KingsSubgraph $arrow.r$ UnitDiskGraph:_ integer grid positions $(i, j)$ map to float coordinates with radius $r = 1.5$.
@@ -16849,7 +16854,7 @@ Problems parameterized by graph type, weight type, or clause-width ($k$) admit i
 
 == Resource Estimation from Examples
 
-The following table shows concrete variable overhead for example instances, taken directly from the canonical fixture examples.
+The following table shows concrete target-variable counts for example instances, taken directly from the canonical fixture examples.
 
 #let example-files = (
   (source: "MaximumIndependentSet", target: "MinimumVertexCover"),
@@ -19727,7 +19732,7 @@ The following table shows concrete variable overhead for example instances, take
       "pred reduce pcsf.json --via route.json -o bundle.json",
       "pred solve bundle.json",
     )
-    The canonical PCSF source has $beta = #pcsf_st.source.instance.beta$, $omega = #pcsf_st.source.instance.omega$, and prizes $p = (#pcsf_st_prizes.at(0), #pcsf_st_prizes.at(1), #pcsf_st_prizes.at(2))$. The target SteinerTree has $|V_H| = n + k + 1 = #(pcsf_st_n + pcsf_st_k + 1)$ vertices, $|E_H| = m + n + 2 k = #(pcsf_st_m + pcsf_st_n + 2 * pcsf_st_k)$ edges, and $|T_H| = k + 1 = #(pcsf_st_k + 1)$ terminals, matching the registered overhead formulas.
+    The canonical PCSF source has $beta = #pcsf_st.source.instance.beta$, $omega = #pcsf_st.source.instance.omega$, and prizes $p = (#pcsf_st_prizes.at(0), #pcsf_st_prizes.at(1), #pcsf_st_prizes.at(2))$. The target SteinerTree has $|V_H| = n + k + 1 = #(pcsf_st_n + pcsf_st_k + 1)$ vertices, $|E_H| = m + n + 2 k = #(pcsf_st_m + pcsf_st_n + 2 * pcsf_st_k)$ edges, and $|T_H| = k + 1 = #(pcsf_st_k + 1)$ terminals, matching the registered exact size formulas.
   ],
 )[
   Bienstock, Goemans, Simchi-Levi, Williamson @BienstockGoemansSimchiLeviWilliamson1993 introduced the prize/penalty framework for prize-collecting network design; Tuncbag and coauthors @TuncbagEtAl2013PCSF @TuncbagEtAl2012RECOMB used the same artificial-root idea to translate PCSF into a rooted prize-collecting Steiner tree on biological networks. The combined construction recorded here adds a per-vertex auxiliary-terminal gadget that compiles the remaining omitted-prize term `beta * p(v)` into ordinary Steiner-tree edge costs, so the target is a plain (unweighted-prize) Steiner Tree instance.

docs/src/cli.md

@@ -80,7 +80,7 @@ pred solve lbdp.json --solver brute-force
 # Evaluate a specific configuration (shows the aggregate value, e.g. Max(2) or Min(None))
 pred evaluate problem.json --config 1,0,1,0
 
-# Reduce along an explicitly chosen Pareto-front route and solve via brute-force
+# Reduce along an explicitly chosen route and solve via brute-force
 pred reduce problem.json --via route.json -o reduced.json
 pred solve reduced.json --solver brute-force
 
@@ -138,7 +138,7 @@ Explore which problems the given problem can reduce to, starting **from** it:
 
 ### `pred path` — Find reduction paths
 
-Find the symbolic Pareto front between two problems:
+Enumerate paths between two problems:
 
 ```text
 {{#include generated/pred-path-mis-qubo.txt}}
@@ -150,21 +150,21 @@ Multi-step paths are discovered automatically:
 {{#include generated/pred-path-factoring-spinglass.txt}}
 ```
 
-Show all paths or save for later use with `pred reduce --via`:
+Inspect reduction paths or save the path set for later route selection:
 
 ```bash
-pred path MIS QUBO --all                    # all paths (up to 20)
-pred path MIS QUBO --all --max-paths 50     # increase limit
-pred path MIS QUBO -o front.json            # save the Pareto front
-pred path MIS QUBO --all -o paths/          # save all paths to a folder
+pred path MIS QUBO                           # paths (up to 20)
+pred path MIS QUBO --max-paths 50            # increase the cap
+pred path MIS MaximumClique mis.json         # execute paths on a complete instance
+pred path MIS QUBO -o paths.json             # save the path set
 ```
 
-When using `--all`, the output is capped at `--max-paths` (default: 20). If more paths exist, the output indicates truncation.
-
-Every front item contains its complete route. The envelope does not select a
-winner; extract the route you want before passing it to `pred reduce --via`.
-Paths with unknown symbolic growth are excluded from the front and listed with
-their analysis-failure reason.
+Without an instance file, each route explains how problem size changes. With a
+problem JSON file, every returned path is executed on the complete source instance
+and the actual size of each constructed intermediate is reported. Discovery never
+ranks or Pareto-prunes routes. Output is capped by `--max-paths` (default: 20);
+extract one route from the path-set envelope before passing it to
+`pred reduce --via`.
 
 ### `pred export-graph` — Export the reduction graph
 
@@ -411,7 +411,7 @@ This is useful for scripting and piping:
 
 ```bash
 pred list --json | jq '.variants[].name'
-pred path MIS QUBO --json | jq '.front[] | {growth, path}'
+pred path MIS QUBO --json | jq '.paths[] | {overall_size, path}'
 ```
 
 ## Problem Name Aliases