From English to Clingo: Where the Translation Breaks

Correction, 7 October 2026: an earlier version of this article said savanty uses a language model fine-tuned on optimisation problems, that it chooses between MiniZinc, OR-Tools and MIP back ends, and quoted formalisation-accuracy figures from an internal benchmark. The model is not fine-tuned, there is one solver (Clingo), and the accuracy figures had no source we can produce, so they have been withdrawn. The article has been rewritten around what the code actually does.

The gap between intent and formalism

Every organisation has constraint problems. A hospital administrator wants a staff roster that covers every shift. A university registrar wants to put courses into rooms without clashes. A team lead wants to assign tasks to people without overloading anyone. These problems have been studied for decades, and there are solvers that handle them exactly.

The catch is that these solvers do not speak English.

To use one, you must express the problem formally: decision variables, their domains, constraints as logical or arithmetic relations, and perhaps an objective. That usually takes someone trained in operations research or constraint programming. The result is a familiar bottleneck. The people who understand the problem best cannot use the tools that solve it, and the people who can write the models do not always understand the problem well enough to capture every rule.

savanty is an attempt to close that gap for one class of problem: discrete constraints over finite domains. This article is about the part of that job that is actually hard, which is not the solving. It is the translation.

Why the solver has to do the solving

A language model asked to produce a roster will produce a plausible one. Plausible is not valid. The model is sampling likely text, not searching an assignment space, and it has no step that rejects an assignment breaking constraint seven. A separate post compares that approach, and the others, with savanty in detail.

The division of labour that follows is simple to state. The language model translates English into a formal program. A solver, here Clingo, searches that program exhaustively. Clingo is sound and complete over finite domains: any answer set it returns satisfies every rule in the program, and if it reports UNSAT within its time budget, no answer set exists. Those properties hold for the program Clingo receives. Whether that program is a faithful rendering of the English is a separate question, and the rest of this article is about that question.

What the pipeline does

savanty is a Python package orchestrated with DSPy typed signatures. The default model is GPT-4o, used as-is through its API rather than fine-tuned; any OpenAI-compatible endpoint can be substituted. A request passes through these stages:

Suitability check. The first call classifies the problem. If it is continuous optimisation, statistics or simulation, savanty returns not_suitable with a suggested_tool such as scipy, cvxpy or pandas, instead of forcing it into the wrong formalism.
Gap identification. If the description is missing entities or counts, savanty returns needs_more_info with a list of questions. You answer through additional_info and call again.
Problem analysis. The model extracts the domain, variables, constraints and any objective.
Program generation. The model emits strict JSON with three fields: facts, rules, and an optional optimisation directive. Every decision must be expressed through one relation, assign(Var, Value).
Compile and solve. The runtime assembles the program, appends #show assign/2., runs Clingo, and classifies the outcome as ok, syntax_error, unsat or empty.

Any outcome other than ok triggers a repair round, described below.

A worked example

The product site’s example is a small nurse roster:

Schedule 4 nurses (Alice, Bob, Carol, Dave) across morning / evening shifts over 3 days. Each shift needs exactly 1 nurse. No nurse works two shifts on the same day.

The generated encoding looks like this:

% 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 choice rule generates candidates; each :- line rules out a class of invalid ones. Clingo returns an answer set in which every slot has one nurse and nobody works twice in a day. The encoding comes back as result.asp_code next to the solution, and that matters more than it looks. Each English sentence maps to a visibly separate rule, so a reader who has never written ASP can still check that every requirement has a line.

A preference changes the shape slightly. “Prefer to keep Dave off evenings” is not a hard rule; it belongs in the optimisation directive as something to minimise, not as an integrity constraint. Marking a preference as a hard rule is one of the easiest ways to turn a solvable problem into an unsatisfiable one.

Where translation breaks

There are two families of translation error, and the distinction is the whole design.

Errors the solver can see. savanty recognises exactly three:

syntax_error: Clingo cannot parse the program, perhaps because of a misspelt predicate or a missing full stop. The literal parse error is passed back to the model. Paraphrasing it (“there was a problem with your code”) throws away the most precise evidence the loop has.
unsat: the program parses but its constraints are jointly contradictory. Either the model added or mistranslated a constraint, or the problem really has no solution.
empty: Clingo found an answer set containing no assign/2 atoms. The model forgot the choice rule, wrote one that never grounds, or used a different predicate despite the contract.

Errors the solver cannot see. The model omits a constraint you stated; Clingo then returns a valid answer to a slightly different problem. The model turns “up to four shifts per week” into “exactly four shifts per week”; Clingo returns an answer that satisfies the wrong rule. The model adds a rule nobody asked for, the program becomes unsatisfiable, and during repair the model weakens a genuine requirement instead of removing the spurious one. None of these produce a solver error. All of them produce a correct answer to the wrong program.

Why a canonical encoding helps

Insisting that every decision is one assign(Var, Value) atom costs expressiveness, and buys three things.

It makes the empty case detectable at all. Without a fixed decision relation, the runtime could not tell “the model emitted no decisions” from “the model named its decisions differently”.

It makes cores readable. When every requirement is an integrity constraint over the same relation, a set of conflicting constraints is a set of short, similar lines rather than a tangle of auxiliary predicates.

It makes the output auditable. The decision schema given to the model uses the identifiers from your problem text, so the encoding talks about alice and d2_pm, not x17.

Reading an unsat core

When Clingo returns UNSAT, savanty computes a minimal unsatisfiable core by deletion filtering: start with all the integrity constraints, try removing each in turn, and keep the removal only if the program stays unsatisfiable. What remains is a set in which every constraint is load-bearing; drop any one and the rest become satisfiable.

The product documentation’s example is a graph-colouring problem with two colours in the domain and this core:

:- assign(n1, C), assign(n2, C).
:- assign(n2, C), assign(n3, C).
:- assign(n1, C), assign(n3, C).

Three mutually adjacent nodes cannot be coloured with two colours. The core says so directly, and nothing else in the program is implicated. There are only two readings. Either a constraint misformalises the problem (perhaps the third adjacency was a translation mistake, or a third colour was dropped from the domain), in which case the encoding should be corrected; or the constraints are faithful and the problem is infeasible, in which case the right output is “no solution exists”. savanty’s repair prompt asks the model to choose between those explicitly, and to leave the encoding unchanged in the second case rather than weakening a constraint to manufacture an answer.

The alternative, which savanty also implements as a baseline mode for comparison, sends the model only the raw “unsatisfiable” message. The model then has to guess which of perhaps dozens of constraints to touch. A localised core turns that guess into a decision about a handful of named lines.

Ambiguity, implicit rules, and problems that do not fit

Ambiguity. “No one should work too many nights” is not something a solver can enforce. The gap-identification step asks for the missing quantity rather than inventing one, but it cannot always tell that a phrase is vague.

Implicit rules. Domain experts leave out rules that are obvious to anyone in their field. savanty has no domain common sense; it encodes what you wrote. This is the most common real failure, and the only defence is reading the encoding.

Hard instances. A correct encoding can still be expensive to search. Clingo’s completeness holds within the solve timeout; a timeout is not a proof of anything.

The wrong class of problem. Continuous, stochastic and statistical problems do not belong in ASP. The suitability check exists so that these are redirected rather than encoded badly.

What we are not claiming

We have not published a formalisation-accuracy rate for savanty, and this article does not offer one. The repository includes a benchmark harness, with fixtures for problems such as graph colouring and scheduling, built to compare typed-core repair with the generic baseline. If you are deciding whether savanty translates your problems faithfully enough, run it on your own problem family; your rules are almost certainly more particular than any fixture.

Why this matters

Constraint solvers are among the most useful and underused tools in computing. The barrier has rarely been the solvers; it has been the translation between intent and formal specification. savanty’s bet is that a language model can do much of that translation, provided the output is constrained to a shape a solver can check, failures come back as typed evidence rather than vague errors, and the encoding is always exposed for a human to read. The guarantee comes from the solver. The accessibility comes from the language model. The honesty comes from showing the program in between.