Describe it in English.
Solve it with a guarantee.
Savanty is a natural-language to constraint solver. An LLM translates your problem into Answer Set Programming; the Clingo solver searches exhaustively for a valid answer set — or proves none exists. Not a guess: a proof.
pip install savanty node(n1). node(n2). node(n3).
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).What is Savanty?
Savanty is an open-source Python package and FastAPI service that turns a plain-English description of a discrete constraint problem into a solved answer — by putting an LLM where LLMs are good (translation) and a solver where solvers are good (search), with a typed feedback loop between them.
Translates English → ASP
A DSPy-orchestrated model (GPT-4o by default, or any OpenAI-compatible endpoint including Ollama Cloud)
emits facts, choice rules, and integrity constraints over a canonical assign(Var, Value) contract. That is a language task, and LLMs do it well.
Searches, soundly
Answer Set Programming is sound and complete over finite domains. If Clingo returns a model, every
integrity constraint holds. If it returns UNSAT, no valid assignment exists.
The guarantee lives here.
Repairs, with typed cores
When the solver rejects the program, Savanty classifies the failure and — on UNSAT — computes a minimal unsatisfiable core so the LLM revises exactly the constraints that conflict, instead of re-reading a raw error.
Read the full pipeline on how it works, or the honest scope on the FAQ.
The problems Savanty solves
Use each tool for what it is good at. English in, a guaranteed answer set out.
LLMs hallucinate solutions
The problem
Ask a model to schedule four nurses and it returns a plausible table. Plausible is not valid — nothing proved the schedule satisfies every constraint.
Savanty's approach
Savanty never lets the LLM answer. The LLM only translates; Clingo produces the assignment, and a returned assignment satisfies every integrity constraint by construction.
Solvers do not read English
The problem
ASP and CP-SAT are formal languages. Stakeholders do not type them, and hiring an OR modeller for a one-off scheduling question is expensive.
Savanty's approach
The LLM front-end does the "OR consultant" work automatically: picking the relation, the choice rule, and the integrity constraints that encode your policy.
Translation breaks silently
The problem
A mis-formalized constraint yields a wrong-but-consistent answer, or an UNSAT you cannot diagnose. The failure hides until someone checks by hand.
Savanty's approach
A typed self-repair loop classifies each failure and, on UNSAT, extracts a minimal unsatisfiable core so the exact conflicting constraints get revised — or infeasibility is reported faithfully.
Not every problem fits a solver
The problem
Point a constraint solver at a continuous or statistical problem and you get nonsense. Most tools try anyway.
Savanty's approach
The first LLM call is a suitability check. If your problem is continuous, statistical, or streaming, Savanty returns a suggested_tool (scipy, cvxpy, sklearn, pandas) and stops.
One canonical contract. Every decision is assign(Var, Value).
Requirements become integrity constraints (rules starting with :-). That uniform
encoding is what makes the unsat-core repair loop possible — the solver reasons about your constraints.
% domains
nurse(alice; bob; carol; dave).
slot(d1_am; d1_pm; d2_am; d2_pm; d3_am; d3_pm).
% exactly one nurse per slot
1 { assign(S, N) : nurse(N) } 1 :- slot(S).
% no nurse works both shifts of a day
:- assign(d1_am, N), assign(d1_pm, N).
:- assign(d2_am, N), assign(d2_pm, N).
:- assign(d3_am, N), assign(d3_pm, N).
% harness appends automatically
#show assign/2.
The generated encoding is returned as result.asp_code next to the solution, so you can audit it.
Translate, solve, repair
A small pipeline with a clear division of labour. 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 →Discrete constraint satisfaction. That is the whole job.
The suitability check is the first thing Savanty runs. If your problem does not fit ASP, it says so — honestly.
Good fit
- Shift scheduling, rostering, timetabling
- Task and resource assignment
- Seating, team formation, allocation
- Route planning over a small graph
- Logic puzzles, graph colouring, n-queens
Wrong tool — Savanty redirects you
- Continuous optimization
cvxpy / scipy - Statistical / ML modelling
sklearn / pytorch - Data analysis over large tables
pandas - Simulation or streaming data
— - Pure arithmetic
a calculator
Explore Savanty
Everything from the pipeline internals to worked problems and honest comparisons.
Features
Translate, solve, repair — the full capability set, each part inspectable.
Explore →How it works
The five-step pipeline from English to a solved answer set, with a diagram.
Explore →Quickstart
Install from PyPI and solve your first problem in Python, the CLI, or REST.
Explore →Use cases
Scheduling, assignment, timetabling, graph colouring, and logic puzzles.
Explore →Guides
Writing good problem statements, configuring the LLM, reading an unsat core.
Explore →Compare
How Savanty sits against hand-written OR-Tools, ChatGPT, and cvxpy.
Explore →Blog
Field notes on the boundary between LLM translation and sound solving.
Explore →FAQ
What "guaranteed" precisely means, the scope, and the honest caveats.
Explore →Glossary
ASP, Clingo, answer set, integrity constraint, unsat core, DSPy — defined.
Explore →Bring us a problem you can describe but can't reliably solve
Savanty is open source (MIT). Install it from PyPI, describe your problem in English, and get a guaranteed answer set — or a faithful proof that none exists.
Part of Skelf Research
Savanty is one of Skelf Research's narrowly-scoped, open tools.