How it works

Savanty is a five-step pipeline. The LLM handles language; Clingo handles search; a typed loop handles the seam between them. Here is the whole thing.

  English problem
        │
        ▼
  ┌───────────────┐   not suitable → suggested_tool (scipy / cvxpy / sklearn / pandas)
  │ 1. Suitability│ ─────────────────────────────────────────────────────────────►
  └──────┬────────┘
         ▼
  ┌───────────────┐   gaps → clarifying questions
  │ 2. Gap ID     │ ──────────────────────────────►
  └──────┬────────┘
         ▼
  ┌───────────────┐   emits { facts, rules, optimize } over assign(Var, Value)
  │ 3. Generate   │
  └──────┬────────┘
         ▼
  ┌───────────────┐   answer set ──► SOLUTION (guaranteed consistent)
  │ 4. Clingo     │
  └──────┬────────┘
         │ syntax_error │ unsat │ empty
         ▼
  ┌───────────────┐   unsat → minimal unsatisfiable core → revise exact constraints
  │ 5. Repair loop│ ──┐
  └───────────────┘   │  (typed feedback back to step 3)
         ▲────────────┘

LLM

Suitability check

The first call decides whether this is a discrete constraint problem. If it looks continuous, statistical, or streaming, Savanty returns not_suitable with a suggested_tool (scipy, cvxpy, sklearn, pandas) and stops.

LLM

Gap identification

Missing entities, counts, or constraints surface as clarifying questions before any code is generated. You answer via additional_info.

LLM

Program generation

The model emits strict JSON — facts, rules, optimize — over the canonical assign(Var, Value) contract, with at least one choice rule and integrity constraints for every requirement.

Clingo

Exhaustive search

Clingo grounds the program and searches for an answer set. Over finite domains ASP is sound and complete: a returned model satisfies every constraint; UNSAT means no assignment exists.

Loop

Typed self-repair

On syntax_error, unsat, or empty, Savanty builds typed feedback. For unsat it extracts a minimal unsatisfiable core and asks the LLM to fix a misformalized constraint or report faithful infeasibility.

Why the canonical contract matters

Because every decision is assign(Var, Value) and every requirement is an integrity constraint, the solver can reason about your constraints — which is what makes the minimal unsatisfiable core computable. Read the deep dive on reading an unsat core, or the honest scope on the FAQ.