About Savanty

What it is

Savanty is an open-source Python package from Skelf-Research. Install it with pip install savanty; it requires Python 3.10+ and an OpenAI-compatible LLM credential (OPENAI_API_KEY or OLLAMA_API_KEY against Ollama Cloud’s v1 endpoint). The package ships a Python API, a CLI (savanty -p "..."), and a FastAPI server (savanty --web).

What is actually inside

The repository contains exactly these components — nothing more, nothing less:

• solver.py — orchestrates the pipeline, the self-repair loop, and produces a typed ProblemSolverResult.
• asp_runtime.py — wraps Clingo, parses answer sets, exposes parse_assign_atoms and run_clingo.
• dspy_modules.py — the LLM signatures: ProblemSuitabilityCheck, ProblemAnalysis, GapIdentification, ProgramGeneration, ASPRepair (typed-core mode), ASPRepairGeneric (Logic-LM baseline mode), SolutionVisualization, and an interactive composite module.
• cli.py — the CLI and the FastAPI app (POST /solve, GET /health, GET /ready, OpenAPI at /docs).
• frontend/ — a Vue.js web UI for the REST server.
• desktop/ — an optional Slint desktop GUI (pip install savanty[desktop]).
• benchmark/ — problem generators, a verifier, and JSON fixtures for graph colouring, scheduling, and other constraint families used to evaluate repair quality.

The canonical decision contract

Every problem Savanty handles must be expressible as: each decision variable takes exactly one value from a finite domain. The generator is constrained to emit exactly one relation, assign(Var, Value), and at least one choice rule of the form:

1 { assign(V, a); assign(V, b); assign(V, c) } 1 :- var(V).

Requirements are encoded as integrity constraints — rules starting with :-. “No two adjacent regions share a colour” is literally :- assign(n1,C), assign(n2,C). The harness appends #show assign/2. for you. This is not aesthetic discipline; it is what makes the rest of the pipeline tractable.

The repair loop — the novel piece

When Clingo returns something other than ok, Savanty classifies the failure into one of three types and constructs typed, localized feedback:

• syntax_error — Clingo could not ground or parse the program. Feedback: the parse error, plus an instruction to fix the offending rule.
• unsat — the program is well-formed but no answer set exists. Savanty runs a deletion-filtering minimal unsatisfiable core over the integrity constraints: it iteratively removes constraints and re-solves until the smallest jointly-conflicting subset remains. That core is fed to the LLM with the instruction to decide whether one of those constraints misformalizes the problem (then correct it) or whether the problem is genuinely infeasible (then leave it unchanged so infeasibility is reported faithfully).
• empty — Clingo found an answer set but it contained no assign/2 atoms. Feedback: add the choice rule, surface decisions as assign/2.

For comparison, a generic repair mode is also implemented (the ASPRepairGeneric DSPy signature) which feeds the raw solver message back to the LLM with no taxonomy and no core. That reproduces the Logic-LM-style refinement baseline. The benchmark harness in benchmark/ measures whether typed cores actually beat raw messages on repair success rate; running it yourself is encouraged.

What it does not do

Savanty does not handle continuous variables, gradient-based optimization, statistical modelling, simulation, or real-time data. The very first LLM call is a suitability check — if your problem looks continuous it returns not_suitable=True with suggested_tool pointing at scipy, cvxpy, sklearn, or pandas, instead of producing nonsense ASP.

It also does not claim to be a general theorem prover. It is a finite-domain CSP / combinatorial optimization front-end. Within that domain, the correctness guarantee is genuine: a returned assignment satisfies every emitted integrity constraint by construction (Clingo’s job). What is not guaranteed is that the constraints faithfully model your verbal description — the LLM might mis-translate. That is the failure mode the repair loop is designed to catch.

Tech stack

• Clingo — the ASP grounder/solver. The correctness guarantee.
• DSPy — LLM orchestration via typed Signature classes and Predict modules.
• FastAPI — the REST surface.
• Vue.js — the optional web UI.
• Slint — the optional desktop GUI.

License and source

MIT. The source of truth is github.com/skelf-research/savanty. Authoritative documentation lives at docs.skelfresearch.com/savanty/. Releases are on PyPI.

Who built it

Skelf-Research is a small research group publishing practical, narrowly-scoped tooling. Savanty is one of those tools. Issues and pull requests on the GitHub repository are the canonical channel for questions and contributions.