zeechimp/solver-assistant-v3

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

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.