Reading a minimal unsatisfiable core when UNSAT
When Clingo returns UNSAT, Savanty hands you the smallest set of constraints that conflict. Here is how to read that core and decide whether to fix a constraint or accept infeasibility.
UNSAT is not an error. It is Clingo telling you, with certainty, that no assignment satisfies every constraint you gave it. Because ASP is sound and complete over finite domains, that verdict is definitive — there is no answer to find. The useful question is why, and that is what the minimal unsatisfiable core answers.
What the core is
A minimal unsatisfiable core is the smallest subset of your integrity constraints that are jointly contradictory. “Minimal” means every constraint in it is load-bearing: drop any one and the remaining set becomes satisfiable. Savanty computes it by deletion filtering — removing integrity constraints one at a time and re-solving until it lands on an irreducible conflicting set.
Consider a graph-colouring problem where the core comes back as:
:- assign(n1, C), assign(n2, C).
:- assign(n2, C), assign(n3, C).
:- assign(n1, C), assign(n3, C).with only two colours in the domain. Three mutually-adjacent nodes and two colours cannot be coloured — the core is exactly the three adjacency constraints that clash. Nothing else in the program is implicated.
Two questions the core lets you answer
Once you can see the conflicting constraints, there are only two possibilities, and Savanty asks the LLM to choose between them:
- A constraint mis-formalizes the problem. Maybe the third adjacency was a translation mistake, or a third colour was omitted from the domain. Then the fix is to correct the encoding and re-solve. This is the case the repair loop handles automatically.
- The problem is genuinely infeasible. The constraints faithfully capture what you asked for, and what you asked for has no solution. Then the honest answer is to report infeasibility — and Savanty is explicitly instructed not to silently weaken a constraint to manufacture a solution.
Why this beats a raw error message
A Logic-LM-style baseline feeds the solver’s raw “UNSATISFIABLE” line back to the model with no localization. The model then has to guess which of a dozen constraints to touch, and it often edits the wrong one — or quietly deletes a real requirement to make the red go away. Savanty’s generic repair mode reproduces exactly that baseline so you can measure the difference; the benchmark/ harness in the repo exists to check whether typed cores actually win. Give the model the three constraints that conflict, and the revision is targeted instead of speculative.
When you inspect result.asp_code after an UNSAT, read the core first. It tells you the smallest true story about why your problem has no answer.
Frequently asked questions
Is an UNSAT always a bug in my problem statement?
No. Sometimes the constraints are correctly formalized and the problem genuinely has no solution. The value of the core is that it lets the LLM — and you — distinguish an over-constrained encoding from a genuinely infeasible request, instead of guessing.
How is the core computed?
By deletion filtering: Savanty iteratively removes integrity constraints and re-solves until removing any further constraint would make the program satisfiable. What remains is a minimal jointly-conflicting subset.