Make solve deterministic with registered solver backends

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))

problemreductions-cli/src/cli.rs

@@ -1220,12 +1220,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 +1241,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,

problemreductions-cli/src/commands/inspect.rs

@@ -1,4 +1,6 @@
-use crate::dispatch::{load_problem, read_input, ProblemJson, ReductionBundle};
+use crate::dispatch::{
+    load_problem, read_input, solver_capabilities_view, ProblemJson, ReductionBundle,
+};
 use crate::output::OutputConfig;
 use anyhow::Result;
 use problemreductions::rules::ReductionGraph;
@@ -40,19 +42,21 @@ fn inspect_problem(pj: &ProblemJson, out: &OutputConfig) -> Result<()> {
     }
     text.push_str(&format!("Variables: {}\n", problem.num_variables_dyn()));
 
-    let solvers = problem.available_solvers();
-    let solver_summary = solvers
-        .iter()
-        .map(|solver| {
-            if *solver == "ilp" {
-                "ilp (default)".to_string()
-            } else {
-                (*solver).to_string()
-            }
-        })
-        .collect::<Vec<_>>()
-        .join(", ");
-    text.push_str(&format!("Solvers: {solver_summary}\n"));
+    let solver_view = solver_capabilities_view(&problem)?;
+    text.push_str(&format!("Default solver: {}\n", solver_view.default_solver));
+    text.push_str(&format!("Solvers: {}\n", solver_view.solvers.join(", ")));
+    if let Some(native) = solver_view.capabilities.native.as_ref() {
+        text.push_str(&format!(
+            "Native implementation: {}\n",
+            native.implementation
+        ));
+    }
+    if let Some(ilp) = solver_view.capabilities.ilp.as_ref() {
+        text.push_str(&format!(
+            "ILP pipeline: {}\n",
+            ilp.reduction_path.join(" -> ")
+        ));
+    }
 
     // Reductions
     let outgoing = graph.outgoing_reductions(name);
@@ -67,7 +71,9 @@ fn inspect_problem(pj: &ProblemJson, out: &OutputConfig) -> Result<()> {
         "variant": variant,
         "size_fields": size_fields,
         "num_variables": problem.num_variables_dyn(),
-        "solvers": solvers,
+        "solvers": solver_view.solvers,
+        "default_solver": solver_view.default_solver,
+        "solver_capabilities": solver_view.capabilities,
         "reduces_to": targets,
     });