SAgenT
LLM agents that turn natural-language problems into SAT encodings, solve them, and decode the answer.
What it is
Modern SAT solvers can crack scheduling, routing, graph coloring and puzzle problems very fast, but only once someone writes the problem as Boolean variables and constraints. That modeling step is the hard part. SAgenT uses LLMs as modeling agents, not as solvers: they translate a plain-English problem into a SAT encoding, a real solver does the search, and the result is decoded back into an actual answer (a coloring, a schedule, a path).
Research project at Carnegie Mellon University with Ruben Martins.
Results
A run only counts when a family-specific checker accepts the decoded solution. Pseudo-Boolean / PySAT encodings beat MiniZinc as the intermediate representation in every setup (93% vs 84% under the multi-agent architecture).
How it works
- Parallel proposals. Several specialized "slot" agents (inspired by GALA) each propose a different encoding: different variable schemas, CNF vs. pseudo-Boolean, symmetry breaking, and so on.
- Compile. Each candidate is built through structured actions into an internal representation, then compiled to CNF or pseudo-Boolean form.
- Verify and rank. A deterministic pipeline checks structure, grounding, decoder compatibility, fuzzing against truth tables, and tiny SAT/UNSAT test instances, then scores every candidate.
- Solve. The top candidates run in parallel on PySAT solvers (Glucose3, Cadical) and a weighted majority vote decides.
- Decode. The Boolean assignment becomes a real solution, which is checked independently.
What I learned
- Giving a single agent more steps does not fix a bad first model; it just keeps patching the wrong one. Exploring several encodings up front works better.
- Higher-level is not automatically better: pseudo-Boolean encodings were more reliable than MiniZinc for LLM-built models.
- The bottleneck is almost always the modeling, not the SAT solving.
Also built: Denabase
A verified case library of past SAT encodings, with Weisfeiler-Lehman graph fingerprints, hybrid structural + natural-language retrieval, and an offline "sleep cycle" that mines reusable constraint gadgets. It is a partially integrated memory layer and a future direction for the project.