Features
Savanty is a small pipeline with a clear division of labour: an LLM translates English into Answer Set Programming, Clingo searches for a guaranteed answer set, and a typed loop repairs the encoding when the solver rejects it. Every part is inspectable.
Translate — LLM front-end
Turn English into a formal ASP encoding, and refuse the problems that do not fit.
English → ASP translation
A DSPy-orchestrated LLM (GPT-4o by default; any OpenAI-compatible endpoint, including Ollama Cloud) turns a plain-English problem into facts, choice rules, and integrity constraints over a canonical assign(Var, Value) contract.
Learn more →Suitability check
The first LLM call decides whether your problem is a discrete constraint problem at all. If it looks continuous, statistical, or streaming, Savanty returns not_suitable with a suggested_tool (scipy, cvxpy, sklearn, pandas) instead of pretending to solve it.
Learn more →Gap identification
Before any code is generated, a dedicated step surfaces missing entities, counts, or constraints as clarifying questions — so under-specified problems get clarified, not guessed.
Learn more →Solve — the correctness guarantee
Clingo searches finite domains exhaustively: a valid answer set, or a proof there is none.
Clingo sound & complete search
The generated encoding is handed to the Clingo ASP solver. Over finite domains, ASP is sound and complete: if Clingo returns an answer set, every integrity constraint holds; if it returns UNSAT, no valid assignment exists.
Learn more →Guaranteed-consistent answers
A returned assign/2 assignment satisfies every emitted integrity constraint by construction. The guarantee is genuine within the finite-domain scope — the honest caveat is that the LLM must translate faithfully, which the repair loop exists to check.
Learn more →Repair — closing the loop
Typed failure handling and minimal cores turn solver rejections into targeted fixes.
Typed self-repair loop
When Clingo rejects the program, Savanty classifies the failure into syntax_error, unsat, or empty and feeds typed, localized diagnostics back to the LLM — instead of pasting a raw error message and hoping.
Learn more →Minimal unsatisfiable core
On UNSAT, a deletion-filtering pass finds the smallest subset of integrity constraints that are jointly contradictory, and asks the LLM to either fix a misformalized constraint or report faithful infeasibility.
Learn more →DSPy orchestration
Every LLM step is a typed DSPy Signature (suitability, analysis, gap identification, generation, repair). A generic repair mode reproduces a Logic-LM-style baseline for honest comparison.
Learn more →Interfaces
One solver, three ways to call it — library, CLI, and REST — with inspectable output.
Python library, CLI & FastAPI
Install with pip install savanty. Call solve_optimization_problem() from Python, run savanty -p "..." on the CLI, or start the FastAPI server with savanty --web for a REST /solve endpoint with OpenAPI docs.
Learn more →Inspectable encodings
The generated ASP is returned next to the solution (result.asp_code). The canonical assign(Var, Value) contract makes constraints unusually easy to skim and audit.
Learn more →See the pipeline end to end
Follow a problem from English to a solved answer set.