Logic puzzles

Logic puzzles are pure finite-domain constraint satisfaction, which makes them a satisfying demonstration of what Savanty does: every clue is a hard rule, and the solver deduces the only assignment consistent with all of them.

Clues become integrity constraints

Take a small “who owns the fish” style puzzle. Each attribute (house colour, pet, drink) is assigned once per position, and each clue forbids the assignments it rules out:

1 { assign(H, red); assign(H, blue); assign(H, green) } 1 :- house(H).
:- assign(H, red), assign(H, green).           % a house is one colour
:- assign(h1, C), assign(h2, C).               % neighbours differ
:- not assign(h2, red).                         % clue: house 2 is red
#show assign/2.

The LLM turns each natural-language clue into one of these constraints; Clingo does the deduction.

Sound deduction, not plausible guessing

Ask a language model to solve a zebra puzzle directly and it will produce an answer that looks right and often is not — there is no mechanism forcing every clue to hold simultaneously. Savanty routes the deduction through Clingo, which is sound and complete: the returned assignment satisfies every clue, and if the clues contradict each other you get UNSAT with the conflicting subset named.

Puzzles are also a good way to feel out the pipeline before pointing it at production scheduling — the encodings are small and the generated ASP is easy to read.