Glossary
The vocabulary of Answer Set Programming and the Savanty pipeline, in plain terms.
- Answer Set Programming (ASP)
- A declarative logic-programming paradigm for combinatorial search. You state facts, rules, and constraints; a solver finds "answer sets" (stable models) that satisfy all of them. ASP is sound and complete over finite domains.
- Clingo
- The ASP grounder and solver from the Potassco project. Clingo grounds a logic program (expanding rules over the domain) and searches for answer sets. It is the component that provides Savanty's correctness guarantee.
- Answer set
- A stable model of a logic program: an assignment of atoms that satisfies every rule and integrity constraint. If Clingo returns an answer set, every constraint holds; if it returns none, the program is unsatisfiable.
- Integrity constraint
- An ASP rule with an empty head, written starting with :-. It forbids any answer set in which its body is true. In Savanty every requirement ("no nurse works two shifts in a day") becomes an integrity constraint.
- Choice rule
- An ASP rule of the form n { ... } m :- body that selects between n and m atoms from a set. Savanty uses a choice rule to make each decision variable take exactly one value from its domain.
- assign(Var, Value)
- Savanty's canonical decision relation. Every decision the solver makes is expressed as an assign/2 atom. Constraining the generator to this single relation is what makes the unsat-core repair loop tractable.
- Unsatisfiable (UNSAT)
- The state where no answer set exists — the constraints are jointly contradictory. Clingo reports UNSAT; Savanty then localizes why with a minimal unsatisfiable core.
- Minimal unsatisfiable core
- The smallest subset of integrity constraints that are jointly unsatisfiable. Savanty computes it by deletion filtering: iteratively removing constraints and re-solving until removing any more would make the program satisfiable. It tells you exactly which requirements conflict.
- Sound and complete
- Two guarantees of a search procedure. Sound: every answer it returns is correct (satisfies all constraints). Complete: if a valid answer exists, it will be found. ASP over finite domains is both — which is why a returned assignment is trustworthy and an UNSAT is definitive.
- Finite domain
- A variable whose possible values form a finite, enumerable set (e.g. a nurse assigned to one of 6 shifts). Savanty and ASP handle finite-domain problems; continuous variables are out of scope and get redirected to cvxpy/scipy.
- DSPy
- A framework for programming (not just prompting) language models via typed Signature classes and Predict modules. Savanty defines each LLM step — suitability, gap identification, generation, repair — as a DSPy signature.
- Suitability check
- The first LLM call in the pipeline. It decides whether a problem is a discrete constraint problem at all; if not, it returns not_suitable with a suggested_tool (scipy, cvxpy, sklearn, pandas).
- Self-repair loop
- The feedback loop that runs when Clingo rejects a generated program. Savanty classifies the failure (syntax_error, unsat, empty) and feeds typed diagnostics back to the LLM to regenerate — rather than pasting a raw error message.