Describe optimization problems in English. Get mathematically guaranteed solutions.
Savanty pipes a natural-language description through an LLM that translates it into Answer Set Programming (ASP), then hands the encoding to the Clingo solver. Clingo searches exhaustively. If a valid assignment exists, you get one. If it does not, you get a proof of infeasibility — not a guess.
English in. ASP out. Answer set guaranteed.
Is this a discrete constraint problem? If not, Savanty suggests scipy, cvxpy, sklearn, or pandas and stops.
Missing entities, counts, or constraints surface as clarifying questions before any code is generated.
Emits strict JSON: facts, rules, optimize. All decisions land in one canonical relation: assign(Var, Value).
The solver grounds the program and finds an answer set — or reports unsat with a minimal conflicting core.
On syntax_error, unsat, or empty, the solver feeds typed diagnostics back to the LLM and re-tries.
The novel piece is step 5: a solver-grounded self-repair loop. When clingo finds the
encoding unsatisfiable, Savanty computes a minimal unsatisfiable core — the
smallest subset of integrity constraints that are jointly contradictory — and asks the LLM
to revise exactly those. A baseline generic mode reproduces Logic-LM-style
refinement (raw error message only) for comparison.
LLMs hallucinate solutions. Solvers don’t parse English. Savanty uses each for what it’s good at.
LLMs are great at translation
GPT-4o (or any OpenAI-compatible model — Ollama Cloud is supported via OLLAMA_API_KEY) is excellent at turning “schedule 4 nurses across 5 days” into formal entities, domains, and constraints. That is a language task and they do it well.
LLMs are bad at search
Ask the same model to also solve the problem and it will confidently emit an assignment that violates a constraint. There is no internal mechanism that proves the answer is consistent. That is not a prompt-engineering problem.
Clingo is great at search
Answer Set Programming is sound and complete for finite-domain constraint problems. If Clingo returns a model, every integrity constraint holds. If it returns UNSAT, no assignment exists.
Clingo can’t parse a Slack message
ASP is a formal language. Stakeholders do not type it. The whole point of Savanty is that the “OR consultant” layer — figuring out what relation, choice rule, and aggregate encodes your shift policy — runs automatically and gets debugged automatically too.
Graph colouring, end to end.
Three regions, three colours, two adjacency constraints. The LLM emits this JSON, Savanty assembles it, clingo solves it.
{
"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": ""
}
Every requirement is an integrity constraint (a rule starting with :-).
Every decision lands in assign(Var, Value). The harness appends
#show assign/2. automatically. This canonical contract is what makes
the unsat-core repair loop possible: the solver can reason about your
constraints, not just its own internal clauses.
Discrete constraint satisfaction. That is the whole job.
| Good fit | Wrong tool |
|---|---|
| Shift scheduling, timetabling | Continuous optimization — try cvxpy or scipy |
| Task and resource assignment | Statistical / ML modelling — try sklearn |
| Route planning over a small graph | Streaming / real-time data |
| Seating, team formation, allocation | Pure arithmetic — just use a calculator |
| Logic puzzles, graph colouring, n-queens | Numerical simulation |
The suitability check is the first LLM call. If your problem doesn’t fit ASP, Savanty
returns not_suitable=True with suggested_tool populated, instead
of pretending to solve it.
Install, run, solve.
pip install savanty
export OPENAI_API_KEY=sk-... # or OLLAMA_API_KEY for Ollama Cloud
# Python API
from savanty import solve_optimization_problem
result = solve_optimization_problem("""
Schedule 4 nurses (Alice, Bob, Carol, Dave) for morning/evening shifts
over 5 days. Each shift needs 1 nurse. Max 4 shifts per person.
""")
print(result.solution) # parsed assign/2 atoms
print(result.asp_code) # the generated encoding, for debugging
# CLI
savanty -p "Assign 5 tasks to 3 workers, balance workload"
# REST (FastAPI + /docs)
savanty --web --port 8000
The Python package ships a CLI and a FastAPI server. Optional extras: savanty[desktop]
installs a Slint GUI; the repo also includes a Vue.js frontend in frontend/.
-
The promise of 'mathematically guaranteed' — what it actually means here
Marketing copy makes the phrase do a lot of work. Inside the pipeline, the guarantee has a precise scope, a precise boundary, and an honest gap. This is where each one lives.
-
From English to model: where translation breaks
The LLM is a translator. Translators get things wrong. The interesting question is which kinds of wrong are recoverable from inside the loop — and how.
-
Why LLMs alone don't solve optimization problems
A large language model can describe a shift schedule. Asking it to produce one is a different request entirely — and the failure mode is invisible until you look.
Two narrow, fair comparisons against the tools you might already reach for.
-
savanty vs. ChatGPT writing OR-Tools code
You can paste your problem into a chat window and ask for an OR-Tools script. What you give up by doing that.
-
savanty vs. writing OR-Tools by hand
If you can already model in CP-SAT, you do not need Savanty. Here is when you do.