About Savanty

What it is

Savanty is an open-source Python package from Skelf Research. Install it with pip install savanty; it needs 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) with OpenAPI docs at /docs.

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), and a solution visualization 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 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. 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:

• syntax_error — Clingo could not ground or parse the program. The parse error is fed back with 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, then asks the LLM to decide whether a constraint misformalizes the problem (correct it) or the problem is genuinely infeasible (leave it, so infeasibility is reported faithfully).
• empty — Clingo found an answer set but it contained no assign/2 atoms. Feedback: add the choice rule and surface decisions as assign/2.

A generic repair mode (the ASPRepairGeneric signature) feeds the raw solver message back with no taxonomy and no core — reproducing the Logic-LM-style baseline. The benchmark harness measures whether typed cores actually beat raw messages; 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 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.

The correctness guarantee is genuine within its scope: 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.
• 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. Documentation lives at docs.skelfresearch.com/savanty/; releases are on PyPI. Savanty is one of Skelf Research's narrowly-scoped, open tools.