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