| --- |
| language: |
| - en |
| license: apache-2.0 |
| library_name: custom |
| tags: |
| - optimization |
| - solver |
| - max-cut |
| - sat |
| - tsp |
| - subset-sum |
| - combinatorial |
| - exact-solver |
| - verification |
| - branch-and-bound |
| - dpll |
| - held-karp |
| - meet-in-the-middle |
| pipeline_tag: text-generation |
| datasets: [] |
| metrics: [] |
| model-index: |
| - name: solver-assistant-v3 |
| results: |
| - task: |
| type: optimization |
| name: MAX-CUT |
| dataset: |
| name: Analytic bench (K_n, C_n, P_n, K_{m,n}) |
| type: synthetic |
| metrics: |
| - name: Pass rate |
| type: accuracy |
| value: "19/19" |
| - task: |
| type: satisfiability |
| name: 3-SAT |
| dataset: |
| name: Analytic bench (PHP, small 3-SAT) |
| type: synthetic |
| metrics: |
| - name: Pass rate |
| type: accuracy |
| value: "6/6" |
| - task: |
| type: optimization |
| name: Subset Sum |
| dataset: |
| name: Analytic bench (powers of 2, 1..10) |
| type: synthetic |
| metrics: |
| - name: Pass rate |
| type: accuracy |
| value: "8/8" |
| - task: |
| type: optimization |
| name: TSP |
| dataset: |
| name: Analytic bench (rectangles, collinear) |
| type: synthetic |
| metrics: |
| - name: Pass rate |
| type: accuracy |
| value: "6/6" |
| --- |
| |
| # Solver-Backed Optimization Assistant v3 |
|
|
| A natural-language front-end over four exact combinatorial solvers, with |
| a JSON schema interface for LLM integration, an analytic bench, and an |
| independent cross-verifier. |
|
|
| No downloads. No network. Pure Python standard library. |
|
|
| ## Model Details |
|
|
| ### Model Description |
|
|
| This is **not a neural network**. It is a deterministic parser that maps |
| natural-language problem descriptions (or JSON schemas) to structured |
| instances, then calls exact solvers and verifies every answer from |
| scratch. |
|
|
| - **Developed by:** [your name / org] |
| - **Model type:** Rule-based parser + exact solver suite |
| - **Language(s):** English |
| - **License:** Apache 2.0 |
| - **Finetuned from:** N/A |
|
|
| ### Model Sources |
|
|
| - **Repository:** [this Hub repo] |
| - **Paper:** N/A |
| - **Demo:** Run `python3 solver_assistant_v3.py` locally. |
|
|
| ## Uses |
|
|
| ### Direct Use |
|
|
| The assistant accepts four problem classes in natural language or JSON: |
|
|
| | Class | NL Example | JSON Schema | |
| |---|---|---| |
| | MAX-CUT | `max cut on A-B:3, B-C:5, C-A:2` | `{"type":"maxcut","edges":[["A","B",3]]}` | |
| | 3-SAT | `sat (x1 or -x2 or x3) and (x2 or x3)` | `{"type":"sat","n_vars":3,"clauses":[[1,-2,3],[2,3]]}` | |
| | Subset Sum | `subset sum [3,7,1,8] target 11` | `{"type":"subset_sum","numbers":[3,7,1,8],"target":11}` | |
| | TSP | `tsp (0,0) (10,0) (10,10) (0,10)` | `{"type":"tsp","points":[[0,0],[10,0],[10,10],[0,10]]}` | |
|
|
| ### Downstream Use |
|
|
| The JSON schema interface (`dispatch_from_json`) is the intended adapter |
| point for an LLM front-end. A model that emits a schema dict can call the |
| same solvers without touching the parser. |
|
|
| ### Out-of-Scope Use |
|
|
| - Not a general-purpose optimizer. Four problem classes only. |
| - Not a replacement for industrial solvers (Gurobi, CPLEX, MiniSat, Kissat). |
| - Not competitive on large instances. MAX-CUT B&B is exact but exhaustive. |
| - Not a trained model. No weights, no inference, no gradients. |
|
|
| ## Bias, Risks, and Limitations |
|
|
| - **Parser brittleness.** The NL front-end is regex-based. Unusual |
| phrasing, typos, or implicit constraints will not parse. |
| - **Scale limits.** MAX-CUT exact at n<=35 with time limit. SAT DPLL |
| times out beyond ~100 variables at phase transition. Subset-sum |
| meet-in-the-middle caps around n=44. TSP Held-Karp caps at n=18. |
| - **No heuristic fallback.** If the exact solver times out, the answer is |
| a lower bound, not a best-effort guess. The status line says so. |
| - **Verification is per-solver.** The `verify` flag checks the returned |
| witness, not the optimality proof. Optimality is claimed only when the |
| solver reports `OPTIMAL (proven)`. |
|
|
| ### Recommendations |
|
|
| - Treat the JSON schema as the stable API. The NL parser is convenience. |
| - Always check the `status` field. `TIMEOUT` means lower bound only. |
| - Use `--cross` to validate any new solver before trusting it. |
|
|
| ## How to Get Started with the Model |
|
|
| ```bash |
| python3 solver_assistant_v3.py "max cut on A-B:3, B-C:5, C-A:2" |
| python3 solver_assistant_v3.py --demo |
| python3 solver_assistant_v3.py --bench |
| python3 solver_assistant_v3.py --cross --sizes 14,16,18,20 |
| python3 solver_assistant_v3.py --stress --trials 50 |
| python3 solver_assistant_v3.py --json '{"type":"maxcut","edges":[["A","B",3]]}' |
| |
| ## Training Details |
| |
| N/A. No training. The solvers are exact algorithms implemented from |
| scratch. |
| |
| ## Evaluation |
| |
| ### Testing Data, Factors & Metrics |
| |
| **Testing Data:** Analytic bench instances with optima derivable by hand. |
| |
| **Metrics:** Exact match against the analytically-known optimum. |
| |
| ### Results |
| |
| | Problem class | Instances | Passed | Source of truth | |
| |---|---|---|---| |
| | MAX-CUT | 19 | 19 | K_n, C_n, P_n, K_{m,n} formulas | |
| | 3-SAT | 6 | 6 | Pigeonhole principle, explicit models | |
| | Subset Sum | 8 | 8 | Binary encoding, total bounds | |
| | TSP | 6 | 6 | Rectangle perimeter, collinear formula | |
| |
| Cross-verification: B&B vs independent exhaustive DFS on MAX-CUT, |
| n = 14, 16, 18, 20, 22. All AGREE, zero disagreements. |
| |
| Stress: 14,000 randomized trials at `--stress 2000`. Zero failures. |
| |
| ## Technical Specifications |
| |
| - **Runtime:** Python 3.8+ |
| - **Dependencies:** Standard library only |
| - **Hardware:** CPU only |
| - **Model size:** ~50 KB (single Python file) |
| |
| ## Citation |
| |
| ```bibtex |
| @misc{solver-assistant-v3, |
| title = {Solver-Backed Optimization Assistant v3}, |
| author = {zeechimp}, |
| year = {2026}, |
| note = {Natural-language front-end over exact combinatorial solvers} |
| } |
| ``` |
| |
| ## Glossary |
| |
| - **B&B:** Branch and bound. Exact MAX-CUT solver with upper-bound pruning. |
| - **DPLL:** Davis-Putnam-Logemann-Loveland. Exact SAT solver. |
| - **Held-Karp:** Exact TSP dynamic programming, O(n^2 * 2^n). |
| - **Meet-in-the-middle:** Exact subset-sum, O(2^(n/2)). |
| - **Cross-verifier:** Independent exact solver used to validate another. |
