savanty

Overview

savanty tests whether natural language can be a reliable front end to a formal solver, and the result so far is a clear split rather than a clean yes or no. Language models translate a problem statement into a formal encoding competently. They cannot be trusted to solve the encoding they produced. Those two findings point at an architecture rather than at a verdict.

The pipeline puts the model at the front and the solver behind it. An English description goes in. A DSPy-orchestrated model, GPT-4o by default, translates it into a canonical Answer Set Programming encoding in which every decision appears as an assign(Var, Value) atom. Clingo then searches the finite domain exhaustively. If a solution exists, it is found; if none exists, that is a proof rather than a failure to find one.

The canonical encoding is what makes the rest possible. By constraining the model to one shape of output rather than letting it write arbitrary ASP, the generated program becomes checkable, comparable across runs, and repairable. A free-form encoding would be more expressive and would remove every one of those properties.

The self-repair loop is typed, which matters more than it sounds. A syntax error, an unsatisfiable program and an empty answer set are three different problems and demand three different responses. A syntax error is handed back with the parser's complaint attached. An unsatisfiable program triggers minimal-unsat-core localisation, so the user is told which small set of constraints conflict rather than being told there is no solution. An empty result means the program ran but emitted no assign atoms — usually a missing choice rule — so the repair step asks for one; that is a modelling error, not a solver error.

The fit is stated narrowly on purpose: discrete constraint satisfaction, which covers scheduling, assignment, timetabling and graph colouring. It is not for continuous optimisation, not for statistical estimation, not for machine learning and not for simulation. Pointing it at a problem of the wrong class produces an encoding that runs and answers the wrong question, which is the worst available failure mode and the reason the boundary is stated so bluntly.

Where it loses: Z3, OR-Tools, MiniZinc and Gurobi are far more capable solvers with decades of engineering behind them, and anyone who can already write a formal encoding should use one directly rather than going through a translation layer. savanty is for the case where the encoding is the barrier.

A practical note on failure. The most common problem in use is not a solver error but a modelling one: the English description omitted a constraint the author considered obvious, and the encoding faithfully reproduced the omission. The system cannot detect this, because the encoding is internally consistent and the answer it produces is genuinely optimal for the problem that was stated. Reading the generated assign atoms before trusting the result is therefore part of the workflow rather than a debugging step, which is why the encoding is exposed at all.