# Savanty — Full reference for language models

> Natural-language to constraint solver. Describe optimization problems in English; the LLM translates to Answer Set Programming (ASP), Clingo searches exhaustively for a valid solution, and a typed self-repair loop closes the gap between English and a sound encoding. Open-source MIT, from Skelf-Research.

This file is the comprehensive, grounded reference. It avoids speculation. Every claim here is traceable to the README (https://github.com/skelf-research/savanty), the source code in `savanty/`, or the documentation site (https://docs.skelfresearch.com/savanty/).

## What Savanty is

Savanty is a Python 3.10+ package (`pip install savanty`) and an optional FastAPI service. It is also distributable with a Vue.js web frontend (in `frontend/`) and a Slint desktop GUI (`pip install savanty[desktop]`).

The runtime pipeline:

1. **Suitability check** — DSPy signature `ProblemSuitabilityCheck`. The first LLM call classifies the problem as one of: constraint_satisfaction, combinatorial_optimization, continuous_optimization, statistical, arithmetic, simulation, or other. If ASP is the wrong tool, it returns `not_suitable=True` with a `suggested_tool` (one of: scipy, cvxpy, calculator, pandas, none).
2. **Gap identification** — DSPy signature `GapIdentification`. Surfaces missing information as a list of questions. If the problem has gaps and you have no `additional_info`, Savanty returns `needs_more_info=True` with `questions` populated.
3. **Problem analysis** — DSPy signature `ProblemAnalysis`. Extracts structured domain, variables, constraints, and objective.
4. **Program generation** — DSPy signature `ProgramGeneration`. Emits STRICT JSON: `{facts: [...], rules: [...], optimize: "..."}` over the canonical decision contract (every decision is `assign(Var, Value)`).
5. **Compile and solve** — `assemble_program` joins facts, rules, optimize, and appends `#show assign/2.`. `run_clingo` (in `asp_runtime.py`) executes the program. The outcome is classified as `ok`, `syntax_error`, `unsat`, or `empty`.
6. **Repair loop** — on any non-`ok` outcome, the runtime constructs typed feedback and re-runs `ASPRepair` (typed-core mode) or `ASPRepairGeneric` (Logic-LM-style baseline). For the `unsat` case, the typed mode also computes a minimal unsatisfiable core via deletion filtering.

## The canonical decision contract

Every problem is encoded as a single relation:

  assign(Var, Value)

…where `Var` is a decision-variable identifier from the problem text and `Value` is an allowed domain value. A choice rule generates candidates; integrity constraints (rules starting with `:-`) eliminate invalid ones. The generator is prompted with explicit `decision_schema` text built by `build_decision_schema(variables, domains)` so that the LLM uses the exact identifiers from the problem and does not rename them.

Example (graph colouring, three nodes, three colours, two adjacency constraints):

  {
    "facts":    ["node(n1).", "node(n2).", "node(n3)."],
    "rules":    [
      "1 { assign(N,c1); assign(N,c2); assign(N,c3) } 1 :- node(N).",
      ":- assign(n1,C), assign(n2,C).",
      ":- assign(n2,C), assign(n3,C)."
    ],
    "optimize": ""
  }

Example (knapsack):

  {
    "facts":    ["w(item1,5).","w(item2,6).","val(item1,10).","val(item2,12)."],
    "rules":    [
      "1 { assign(I,in); assign(I,out) } 1 :- w(I,_).",
      ":- #sum{ W,I : assign(I,in), w(I,W) } > 10."
    ],
    "optimize": "#maximize{ V,I : assign(I,in), val(I,V) }."
  }

## The repair loop in detail

The function `minimal_unsat_core(components)` in `solver.py` implements deletion filtering over the integrity constraints. It starts with all constraints, repeatedly tries removing one and re-running Clingo, and keeps removing only those whose removal still leaves the program unsatisfiable. A parse error during a candidate run is treated as "satisfiable" to avoid wrongly blaming a constraint for a parse failure elsewhere.

The `_build_feedback(outcome, repair_mode)` function builds three different feedback strings depending on `failure_type`:

- `syntax_error`: includes the literal Clingo parse error plus an instruction to fix the offending rule.
- `unsat`: lists the minimal conflicting subset of integrity constraints and instructs the LLM to either correct/remove one of them or, if the problem is genuinely infeasible, leave the encoding unchanged so the infeasibility is reported faithfully.
- `empty`: instructs the LLM to add a choice rule that emits `assign/2` for every decision variable.

In `generic` mode (`ASPRepairGeneric`), the LLM receives only the raw Clingo message with no taxonomy, no core, no contract reminder. This reproduces Logic-LM-style refinement and is implemented specifically as a baseline for the benchmark harness.

## Public API surface

Python:

  from savanty import solve_optimization_problem
  result = solve_optimization_problem(problem_description, additional_info=None)

`ProblemSolverResult` fields: `solution`, `asp_code`, `visualization_html`, `needs_more_info`, `questions`, `error`, `not_suitable`, `suggested_tool`, `suitability_reason`, `assignment` (dict of Var to Value), `infeasible`, `repair_trace`, `repair_iters`, `final_failure_type`.

CLI:

  savanty -p "Assign 5 tasks to 3 workers, balance workload"

FastAPI server:

  savanty --web --port 8000
  POST /solve  { "problem_description": "..." }
  GET  /health
  GET  /ready    # verifies API key is present
  /docs          # OpenAPI

## Configuration

- `OPENAI_API_KEY` — used when `OLLAMA_API_KEY` is absent.
- `OLLAMA_API_KEY` — preferred when present; routes through `https://ollama.com/v1` via DSPy/LiteLLM's `openai/<model>` provider format.
- `SAVANTY_LLM_MODEL` — model tag. Defaults: `openai/gpt-4o` (OpenAI) or `gemma4:31b` (Ollama Cloud).
- `SAVANTY_PORT` — REST server port. Default `8000`.
- `SAVANTY_LOG_LEVEL` — `DEBUG | INFO | WARNING | ERROR`.
- `SAVANTY_SOLVE_TIMEOUT` — seconds. Default `120`.
- `SAVANTY_MAX_TOKENS` — output budget for reasoning models. Default `16000`.

## Domain fit

Good fit (discrete, finite-domain constraint problems):

- Shift scheduling, nurse rostering, timetabling
- Task and worker assignment
- Resource allocation with discrete units
- Seating arrangements, team formation
- Route planning over small graphs
- Logic puzzles, n-queens, graph colouring, Sudoku
- Knapsack and bin-packing style combinatorial optimization

Wrong tool (Savanty returns `not_suitable` with a redirect):

- Continuous optimization → cvxpy, scipy
- Statistical / ML → sklearn, pytorch
- Simple arithmetic → calculator
- Real-time streaming → not Savanty
- Numerical simulation → not Savanty

## What is guaranteed and what is not

Guaranteed: every returned `assign(Var, Value)` mapping satisfies every integrity constraint in the encoding sent to Clingo. This is Clingo's soundness under stable model semantics. Completeness within the time budget is also guaranteed: if a model exists and the timeout is not hit, Clingo finds one.

Not guaranteed: that the LLM's translation faithfully captures the user's intent. The LLM can omit, over-constrain, or mistranslate. The repair loop catches three structural failures (syntax_error, unsat, empty) and the suitability check redirects unfit problems, but a quietly omitted constraint remains a risk. The mitigations are: returning the generated ASP as `result.asp_code` for inspection, the canonical decision contract that makes constraints unusually easy to skim, and the benchmark harness for evaluating repair quality on your problem family.

## Repository layout

- `savanty/solver.py` — pipeline orchestration, `assemble_program`, `compile_and_solve`, `minimal_unsat_core`, `_build_feedback`, `solve_optimization_problem`.
- `savanty/asp_runtime.py` — `run_clingo`, `parse_assign_atoms`.
- `savanty/dspy_modules.py` — all DSPy `Signature` classes and the `InteractiveProblemSolver` module.
- `savanty/cli.py` — Click-style CLI and the FastAPI app.
- `savanty/logging_config.py` — logging setup.
- `frontend/` — Vue.js web UI.
- `desktop/` — Slint desktop GUI.
- `tests/` — pytest suite.
- `benchmark/problems/` — JSON fixtures (graph colouring, scheduling, etc.) used to evaluate repair quality.
- `benchmark/build_dataset.py`, `generators.py`, `reference.py`, `verify.py` — benchmark harness.

## References

- GitHub: https://github.com/skelf-research/savanty
- PyPI: https://pypi.org/project/savanty/
- Documentation: https://docs.skelfresearch.com/savanty/
- Clingo / Potassco: https://potassco.org/clingo/
- DSPy: https://github.com/stanfordnlp/dspy
- FastAPI: https://fastapi.tiangolo.com/
- Vue.js: https://vuejs.org/
- Slint: https://slint.dev/

## Page index

Every content page on https://savanty.skelfresearch.com, grouped by section.

Core:

- [Home](https://savanty.skelfresearch.com/): hero, what-is, problem→solution, worked ASP example, features, fit/not-fit.
- [Features](https://savanty.skelfresearch.com/features/): translate, solve, repair — the full capability set.
- [How it works](https://savanty.skelfresearch.com/how-it-works/): the five-step pipeline with a diagram.
- [Quickstart](https://savanty.skelfresearch.com/quickstart/): install, solve in Python, CLI, and REST.
- [FAQ](https://savanty.skelfresearch.com/faq/): what "guaranteed" means, scope, honest caveats.
- [Glossary](https://savanty.skelfresearch.com/glossary/): ASP, Clingo, answer set, integrity constraint, unsat core, DSPy.
- [About](https://savanty.skelfresearch.com/about/): what is in the repo, the decision contract, the repair loop.

Use cases:

- [Use cases index](https://savanty.skelfresearch.com/use-cases/): the discrete constraint problems Savanty fits.
- [Shift scheduling & rostering](https://savanty.skelfresearch.com/use-cases/shift-scheduling/): staff-to-shift assignment under coverage, availability, and fairness rules.
- [Task & resource assignment](https://savanty.skelfresearch.com/use-cases/task-assignment/): tasks-to-workers matching under skill, capacity, and balance rules.
- [Seating & timetabling](https://savanty.skelfresearch.com/use-cases/seating-timetabling/): placement in slots under adjacency, conflict, and capacity rules.
- [Graph colouring](https://savanty.skelfresearch.com/use-cases/graph-colouring/): the canonical worked example — no two adjacent nodes share a colour.
- [Logic puzzles](https://savanty.skelfresearch.com/use-cases/logic-puzzles/): zebra puzzles, n-queens, sudoku-style clues as integrity constraints.

Guides:

- [Guides index](https://savanty.skelfresearch.com/guides/): practical how-tos for statements, configuration, and solver output.
- [Writing a good English problem statement](https://savanty.skelfresearch.com/guides/writing-a-good-problem-statement/): describe a problem so Savanty translates it faithfully.
- [Using Ollama Cloud instead of GPT-4o](https://savanty.skelfresearch.com/guides/using-ollama-cloud/): route translation to an OpenAI-compatible endpoint via OLLAMA_API_KEY.
- [Reading a minimal unsatisfiable core](https://savanty.skelfresearch.com/guides/reading-an-unsat-core/): read the smallest conflicting constraint set when Clingo returns UNSAT.

Compare:

- [Compare index](https://savanty.skelfresearch.com/compare/): where Savanty fits against hand-written solvers, ChatGPT, and continuous-optimization tools.
- [vs writing OR-Tools by hand](https://savanty.skelfresearch.com/compare/raw-or-tools/): when the trade flips for someone who can already model in CP-SAT.
- [vs ChatGPT writing OR-Tools](https://savanty.skelfresearch.com/compare/chatgpt-or-tools/): both use an LLM; only one closes the loop with a solver.
- [vs cvxpy](https://savanty.skelfresearch.com/compare/cvxpy/): a scope comparison — Savanty redirects continuous problems to cvxpy.

Blog:

- [Blog index](https://savanty.skelfresearch.com/blog/): field notes on LLM-to-solver translation.
- [Why LLMs alone don't solve optimization problems](https://savanty.skelfresearch.com/blog/llms-alone-dont-solve-optimization/): describing a schedule versus producing a valid one.
- [From English to model: where translation breaks](https://savanty.skelfresearch.com/blog/from-english-to-model-where-translation-breaks/): which translation errors are recoverable inside the repair loop.
- [The promise of "mathematically guaranteed"](https://savanty.skelfresearch.com/blog/mathematically-guaranteed-what-it-means/): the precise scope, boundary, and honest gap of the guarantee.

Optional:

- [Contact](https://savanty.skelfresearch.com/contact/): reach the Savanty team.

## License

MIT.