Symbolic growth, exact Pareto path search, and deterministic solver backends

Makefile

@@ -289,10 +289,11 @@ cli-demo: cli
 	$$PRED from QUBO --hops 1; \
 	\
 	echo ""; \
-	echo "--- 5. path: find reduction paths ---"; \
+	echo "--- 5. path: asymptotic Pareto front (no --size) ---"; \
 	$$PRED path MIS QUBO; \
-	$$PRED path MIS QUBO -o $(CLI_DEMO_DIR)/path_mis_qubo.json; \
 	$$PRED path Factoring SpinGlass; \
+	echo "--- 5b. path --cost: single concrete path (for reduce --via) ---"; \
+	$$PRED path MIS QUBO --cost minimize-steps -o $(CLI_DEMO_DIR)/path_mis_qubo.json; \
 	$$PRED path MIS QUBO --cost minimize:num_variables; \
 	\
 	echo ""; \

docs/src/cli.md

@@ -163,7 +163,7 @@ Show all paths or save for later use with `pred reduce --via`:
 ```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 path.json             # save path for `pred reduce --via`
+pred path MIS QUBO -o path.json             # save front + best path for `pred reduce --via`
 pred path MIS QUBO --all -o paths/          # save all paths to a folder
 ```
 

docs/src/design.md

@@ -321,7 +321,7 @@ pub trait Solver {
 | Solver | Description |
 |--------|-------------|
 | **BruteForce** | Enumerates all configurations. `solve()` works for any aggregate problem; `find_witness()`, `find_all_witnesses()`, and `solve_with_witnesses()` are available when `P::Value` supports witnesses. Used for testing and verification. |
-| **ILPSolver** | Enabled by default. Solves ILP instances directly with HiGHS via `good_lp`. Also provides `solve_reduced()` for witness-capable problems that implement `ReduceTo<ILP<bool>>`. |
+| **ILPSolver** | Enabled by default. Solves `ILP<bool>` and `ILP<i32>` instances directly with HiGHS via `good_lp`. Also provides `solve_reduced::<V, _>()` for witness-capable problems that implement `ReduceTo<ILP<V>>`. |
 
 ## JSON Serialization
 

docs/src/getting-started.md

@@ -100,10 +100,17 @@ For convenience, `ILPSolver::solve_reduced` combines reduce + solve + extract
 in a single call:
 
 ```rust,ignore
-let solution = ILPSolver::new().solve_reduced(&problem).unwrap();
+let solution = ILPSolver::new()
+    .solve_reduced::<bool, _>(&problem)
+    .unwrap();
 assert!(problem.evaluate(&solution).is_valid());
 ```
 
+The ILP domain is explicit because a source type may provide more than one
+direct ILP reduction. Both `bool` and `i32` are supported. `solve` and
+`solve_reduced` return `ILPSolveError`, which distinguishes infeasibility,
+timeout, unboundedness, unsupported dynamic input, and backend failure.
+
 ### Example 2: Reduction path search — integer factoring to spin glass
 
 Real-world problems often require **chaining** multiple reductions. Here we factor the integer 6 by reducing `Factoring` through the reduction graph to `SpinGlass`, through automatic reduction path search. ([full source](https://github.com/CodingThrust/problem-reductions/blob/main/examples/chained_reduction_factoring_to_spinglass.rs))

examples/chained_reduction_factoring_to_spinglass.rs

@@ -27,7 +27,9 @@ pub fn run() {
             &dst_var,                  // target variant map
             &ProblemSize::new(vec![]), // input size (empty = unknown)
             &MinimizeSteps,            // cost function: fewest hops
+            problemreductions::rules::SearchMode::Exact,
         )
+        .value
         .unwrap();
     println!("  {}", rpath);
     // ANCHOR_END: step1

problemreductions-cli/src/bin/pred_sym.rs

@@ -1,5 +1,5 @@
 use clap::{Parser, Subcommand};
-use problemreductions::{big_o_normal_form, canonical_form, Expr, ProblemSize};
+use problemreductions::{big_o_normal_form, Expr, ProblemSize};
 
 #[derive(Parser)]
 #[command(
@@ -19,11 +19,6 @@ enum Commands {
         /// Expression string
         expr: String,
     },
-    /// Compute exact canonical form
-    Canon {
-        /// Expression string
-        expr: String,
-    },
     /// Compute Big-O normal form
     BigO {
         /// Expression string
@@ -33,7 +28,7 @@ enum Commands {
         #[arg(long)]
         raw: bool,
     },
-    /// Compare two expressions (exits with code 1 if neither exact nor Big-O equal)
+    /// Compare two expressions for Big-O equivalence (exits 1 if not equal)
     Compare {
         /// First expression
         a: String,
@@ -69,16 +64,6 @@ fn main() {
             let parsed = parse_expr_or_exit(&expr);
             println!("{parsed}");
         }
-        Commands::Canon { expr } => {
-            let parsed = parse_expr_or_exit(&expr);
-            match canonical_form(&parsed) {
-                Ok(result) => println!("{result}"),
-                Err(e) => {
-                    eprintln!("Error: {e}");
-                    std::process::exit(1);
-                }
-            }
-        }
         Commands::BigO { expr, raw } => {
             let parsed = parse_expr_or_exit(&expr);
             match big_o_normal_form(&parsed) {
@@ -98,29 +83,31 @@ fn main() {
         Commands::Compare { a, b } => {
             let expr_a = parse_expr_or_exit(&a);
             let expr_b = parse_expr_or_exit(&b);
-            let canon_a = canonical_form(&expr_a);
-            let canon_b = canonical_form(&expr_b);
             let big_o_a = big_o_normal_form(&expr_a);
             let big_o_b = big_o_normal_form(&expr_b);
 
             println!("Expression A: {a}");
             println!("Expression B: {b}");
-            let mut exact_equal = false;
-            let mut big_o_equal = false;
-            if let (Ok(ca), Ok(cb)) = (&canon_a, &canon_b) {
-                exact_equal = ca == cb;
-                println!("Canonical A:  {ca}");
-                println!("Canonical B:  {cb}");
-                println!("Exact equal:  {exact_equal}");
-            }
-            if let (Ok(ba), Ok(bb)) = (&big_o_a, &big_o_b) {
-                big_o_equal = ba == bb;
-                println!("Big-O A:      O({ba})");
-                println!("Big-O B:      O({bb})");
-                println!("Big-O equal:  {big_o_equal}");
-            }
-            if !exact_equal && !big_o_equal {
-                std::process::exit(1);
+            match (&big_o_a, &big_o_b) {
+                (Ok(ba), Ok(bb)) => {
+                    // Rendering is canonical, so equal growth ⇒ equal Big-O expr.
+                    let big_o_equal = ba == bb;
+                    println!("Big-O A:      O({ba})");
+                    println!("Big-O B:      O({bb})");
+                    println!("Big-O equal:  {big_o_equal}");
+                    if !big_o_equal {
+                        std::process::exit(1);
+                    }
+                }
+                _ => {
+                    if let Err(e) = &big_o_a {
+                        println!("Big-O A:      <unsupported: {e}>");
+                    }
+                    if let Err(e) = &big_o_b {
+                        println!("Big-O B:      <unsupported: {e}>");
+                    }
+                    std::process::exit(1);
+                }
             }
         }
         Commands::Eval { expr, vars } => {

problemreductions-cli/src/cli.rs

@@ -1,3 +1,4 @@
+use crate::util::{build_search_mode, SearchLimitOverrides};
 use clap::{CommandFactory, Parser, Subcommand, ValueEnum};
 use std::collections::HashMap;
 use std::path::PathBuf;
@@ -46,6 +47,54 @@ pub struct Cli {
     pub command: Commands,
 }
 
+#[derive(Clone, Copy, Debug, Eq, PartialEq, ValueEnum)]
+pub enum SearchModeArg {
+    Exact,
+    Approximate,
+}
+
+/// Completeness and resource policy shared by path-discovery commands.
+#[derive(clap::Args, Clone, Debug)]
+pub struct SearchArgs {
+    /// Search completeness: exact elementary-path enumeration or bounded best-effort.
+    #[arg(long, value_enum, default_value_t = SearchModeArg::Approximate)]
+    pub search_mode: SearchModeArg,
+    /// Maximum reduction hops in approximate mode (default: 16).
+    #[arg(long)]
+    pub max_hops: Option<usize>,
+    /// Maximum live labels per node in approximate mode (default: 32).
+    #[arg(long)]
+    pub max_labels_per_node: Option<usize>,
+    /// Maximum expanded states in approximate mode.
+    #[arg(long)]
+    pub max_expanded_states: Option<usize>,
+    /// Wall-clock search timeout in seconds in approximate mode.
+    #[arg(long = "timeout")]
+    pub timeout: Option<u64>,
+}
+
+impl SearchArgs {
+    pub fn mode(&self) -> anyhow::Result<problemreductions::rules::SearchMode> {
+        build_search_mode(
+            self.search_mode == SearchModeArg::Exact,
+            SearchLimitOverrides {
+                max_hops: self.max_hops,
+                max_labels_per_node: self.max_labels_per_node,
+                max_expanded_states: self.max_expanded_states,
+                timeout_seconds: self.timeout,
+            },
+        )
+    }
+
+    pub fn has_nondefault_policy(&self) -> bool {
+        self.search_mode != SearchModeArg::Approximate
+            || self.max_hops.is_some()
+            || self.max_labels_per_node.is_some()
+            || self.max_expanded_states.is_some()
+            || self.timeout.is_some()
+    }
+}
+
 #[derive(Subcommand)]
 pub enum Commands {
     /// List all registered problem types (or reduction rules with --rules)
@@ -112,11 +161,11 @@ Use `pred to <problem>` for incoming neighbors (what reduces to this).")]
     /// Find the cheapest reduction path between two problems
     #[command(after_help = "\
 Examples:
-  pred path MIS QUBO                              # cheapest path
+  pred path MIS QUBO                              # asymptotic Pareto front (Big-O per size field)
   pred path MIS QUBO --all                        # all paths
-  pred path MIS QUBO -o path.json                 # save for `pred reduce --via`
+  pred path MIS QUBO -o path.json                 # save front + best path for `pred reduce --via`
   pred path MIS QUBO --all -o paths/              # save all paths to a folder
-  pred path MIS QUBO --cost minimize:num_variables
+  pred path MIS QUBO --cost minimize:num_variables  # single cheapest path by a scalar cost (also -o for --via)
 
 Use `pred list` to see available problems.")]
     Path {
@@ -126,15 +175,18 @@ Use `pred list` to see available problems.")]
         /// Target problem (e.g., QUBO)
         #[arg(value_parser = crate::problem_name::ProblemNameParser)]
         target: String,
-        /// Cost function [default: minimize-steps]
-        #[arg(long, default_value = "minimize-steps")]
-        cost: String,
+        /// Scalar cost function ('minimize-steps' or 'minimize:<field>') for a single
+        /// best path. Omit to get the instance-free asymptotic Pareto front.
+        #[arg(long)]
+        cost: Option<String>,
         /// Show all paths instead of just the cheapest
         #[arg(long)]
         all: bool,
         /// Maximum paths to return in --all mode
         #[arg(long, default_value_t = 20)]
         max_paths: usize,
+        #[command(flatten)]
+        search: SearchArgs,
     },
 
     /// Export the reduction graph to JSON
@@ -1220,12 +1272,12 @@ impl CreateArgs {
 #[derive(clap::Args)]
 #[command(after_help = "\
 Examples:
-  pred solve problem.json                        # ILP solver (default, auto-reduces to ILP)
+  pred solve problem.json                        # deterministic registered backend or fallback
   pred solve problem.json --solver brute-force   # brute-force (exhaustive search)
-  pred solve problem.json --solver customized    # customized (structure-exploiting exact solver)
+  pred solve problem.json --solver ilp           # require the registered fixed ILP pipeline
   pred solve reduced.json                        # solve a reduction bundle
   pred solve reduced.json -o solution.json       # save result to file
-  pred create MIS --graph 0-1,1-2 | pred solve - # read from stdin when an ILP path exists
+  pred create MIS --graph 0-1,1-2 | pred solve - # read from stdin
   pred create GroupingBySwapping --string \"0,1,2,0,1,2\" --bound 5 | pred solve - --solver brute-force
   pred create StringToStringCorrection --source-string \"0,1,2,3,1,0\" --target-string \"0,1,3,2,1\" --bound 2 | pred solve - --solver brute-force
   pred create TwoDimensionalConsecutiveSets --alphabet-size 6 --sets \"0,1,2;3,4,5;1,3;2,4;0,5\" | pred solve - --solver brute-force
@@ -1241,24 +1293,19 @@ Solve via explicit reduction:
 
 Input: a problem JSON from `pred create`, or a reduction bundle from `pred reduce`.
 When given a bundle, the target is solved and the solution is mapped back to the source.
-The ILP solver auto-reduces non-ILP problems before solving.
-Problems without an ILP reduction path, such as `GroupingBySwapping`,
-`LengthBoundedDisjointPaths`, `MinMaxMulticenter`, and `StringToStringCorrection`,
-currently need `--solver brute-force`.
-
-Customized solver: exact witness recovery for select problems via structure-exploiting
-backends. Currently supports MinimumCardinalityKey, AdditionalKey, PrimeAttributeName,
-BoyceCoddNormalFormViolation, PartialFeedbackEdgeSet, and RootedTreeArrangement.
+By default, solve deterministically selects the exact variant's registered native
+backend, then its fixed ILP pipeline, and otherwise brute force. `--solver ilp`
+requires a registered ILP pipeline; it never searches the reduction graph.
 
 ILP backend (default: HiGHS). To use CPLEX instead:
   cargo install problemreductions-cli --features cplex
 (Requires CPLEX to be installed on your system.)")]
 pub struct SolveArgs {
     /// Problem JSON file (from `pred create`) or reduction bundle (from `pred reduce`). Use - for stdin.
     pub input: PathBuf,
-    /// Solver: ilp (default), brute-force, or customized
-    #[arg(long, default_value = "ilp")]
-    pub solver: String,
+    /// Solver override: ilp or brute-force. Omit for deterministic default dispatch.
+    #[arg(long)]
+    pub solver: Option<String>,
     /// Timeout in seconds (0 = no limit)
     #[arg(long, default_value = "0")]
     pub timeout: u64,
@@ -1273,7 +1320,8 @@ Examples:
   pred create MIS --graph 0-1,1-2 | pred reduce - --to QUBO  # read from stdin
 
 Input: a problem JSON from `pred create`. Use - to read from stdin.
-The --via path file is from `pred path <SRC> <DST> -o path.json`.
+The --via path file is from `pred path <SRC> <DST> -o path.json` (its
+top-level `path` is the best path; add --cost to pick a scalar-optimal one).
 When --via is given, --to is inferred from the path file.
 Output is a reduction bundle with source, target, and path.
 Use `pred solve reduced.json` to solve and map the solution back.")]
@@ -1286,6 +1334,8 @@ pub struct ReduceArgs {
     /// Reduction route file (from `pred path ... -o`)
     #[arg(long)]
     pub via: Option<PathBuf>,
+    #[command(flatten)]
+    pub search: SearchArgs,
 }
 
 #[derive(clap::Args)]