Frequently asked questions
What Savanty guarantees, what it deliberately does not, and how to run it.
General
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. An LLM translates the English into Answer Set Programming, and the Clingo solver searches for a valid answer set — or proves none exists.
Is Savanty an LLM that solves optimization problems?
No. The LLM never solves the problem; it only translates English into a formal ASP encoding. Clingo does the search. This split is deliberate: LLMs are good at language and bad at proving an assignment is consistent, while Clingo is sound and complete over finite domains.
What language and license is Savanty?
Savanty is written in Python (3.10+) and is MIT licensed. Source is at github.com/skelf-research/savanty; releases are on PyPI at pypi.org/project/savanty/.
Which LLM does Savanty use?
It defaults to GPT-4o via OpenAI, but any OpenAI-compatible endpoint works — including Ollama Cloud via OLLAMA_API_KEY. LLM orchestration is handled by DSPy typed signatures.
The guarantee & the repair loop
Is the answer really mathematically guaranteed?
Within a precise scope, yes. Clingo is sound and complete over finite domains, so a returned assign/2 assignment satisfies every emitted integrity constraint by construction. The honest caveat: the guarantee covers the encoding, not the translation. The LLM might mis-formalize your English description — that is the failure mode the typed self-repair loop and the suitability check exist to catch, not something Clingo can detect.
What happens if my problem has no solution?
Clingo returns UNSAT. Savanty then computes a minimal unsatisfiable core — the smallest subset of integrity constraints that are jointly contradictory — and asks the LLM to decide whether a constraint misformalizes the problem (correct it) or the problem is genuinely infeasible (report it faithfully). You get a diagnosable answer, not a silent failure.
How does Savanty handle solver failures?
It classifies every failure into one of three types — syntax_error, unsat, or empty — and feeds typed, localized diagnostics back to the LLM through a dedicated repair signature. A generic mode (raw error only) reproduces a Logic-LM-style baseline for comparison.
What is the canonical decision contract?
Every decision variable must take exactly one value from a finite domain, encoded as a single relation assign(Var, Value) plus at least one choice rule. Requirements become integrity constraints (rules starting with :-). This uniformity is what makes the unsat-core repair loop possible.
Scope — what fits, what doesn't
What kinds of problems fit Savanty?
Discrete constraint satisfaction: shift scheduling, timetabling, task and resource assignment, seating, team formation, route planning over small graphs, logic puzzles, and graph colouring.
What does Savanty NOT do?
It does not handle continuous optimization (use cvxpy or scipy), machine learning (sklearn/pytorch), statistical analysis (pandas), simulation, or streaming data. The first LLM call is a suitability check that returns not_suitable with a suggested_tool when your problem does not fit ASP, instead of producing nonsense.
Is Savanty a general theorem prover?
No. It is a finite-domain constraint satisfaction and combinatorial optimization front-end. Within that domain the correctness guarantee is genuine; outside it, Savanty redirects you to the right tool.
Using Savanty
How do I install and run it?
pip install savanty, then set OPENAI_API_KEY (or OLLAMA_API_KEY). Call solve_optimization_problem() from Python, run savanty -p "..." on the CLI, or savanty --web to start the FastAPI server. See the Quickstart.
Can I inspect the generated ASP?
Yes. The generated encoding is returned as result.asp_code next to the solution. The canonical assign(Var, Value) contract makes the constraints unusually easy to skim and audit.
Where is the documentation and source?
Docs are at docs.skelfresearch.com/savanty/, source at github.com/skelf-research/savanty, and releases on PyPI. Savanty is built by Skelf Research (skelfresearch.com).