On this page

Introduction

Last week, LymphoSAT, the solver I submitted to the SAT Competition 2026, won the SAT track! It beat 27 other entrants, including 10 other AI-enhanced solvers.1

But LymphoSAT is not just one solver: it is an ensemble of 126 different, specially crafted solvers, each targeted for a different class of problem. These specialists are not just variants of the same core, and in fact many of them do not even implement traditional SAT algorithms at all!

The actual specialists are remarkably diverse. One reconstructs feed-forward lookup-table circuits and enumerates their primary inputs with AVX-512 (random-circuits); another extracts a hidden 64-bit product, factors it with Miller–Rabin and Pollard Rho, and propagates the factors back into a SAT model (fermat). A third rebuilds an encoded 5×5 sliding puzzle and solves it with IDA* (sliding-puzzle), while another recovers physical lock charts and searches directly over mechanical key bittings (mechanical-master-key). Others recognize SNCF railway bounded-model-checking formulas as circuit DAGs (railway-safety) or recover a factored Tower-of-Hanoi planning encoding, generate the canonical 2ⁿ−1 move sequence, and map every move back to its action variables (hanoi).

Browse the full list of specialists below:

Such an ensemble would have taken months of human expert software engineering to build by hand, but I was able to do it in just a few days with \$10,000 worth of LLM spend (mostly GPT-5.5 in Codex) and about \$5,000 of Google Cloud usage for parallelized solver evaluations.

While such an approach has always been theoretically possible, it has only recently become economically viable as frontier coding agents can completely replace expert human labor with token expenditure.

In this post, I’ll explain the importance of SAT, how it acts as a common interface for constraint problems, and how the traditional methodology of SAT solver development might be fundamentally limited. Then I’ll explain how LymphoSAT exploits this gap through AI-driven domain-specific hyperspecialization and why this might be the future of SAT solving, and perhaps other areas of software engineering.

P.S. I’m currently working on a long-form paper with more thorough evaluations and analysis. Stay tuned!

P.P.S. I’m also building an LLM benchmark related to this concept; if you work at a lab and want to see your model evaluated, please reach out.

One problem, many shapes

Boolean satisfiability, usually abbreviated as SAT, is the problem of deciding whether a given Boolean formula is satisfiable.

Given some variables $a$, $b$, $c$, etc., which can either be true or false, we can create a formula by combining them with logical connectors $\land$ (AND), $\lor$ (OR), and $\neg$ (NOT).

$$ F := (a \lor \neg b) \land (b \lor c) \land (\neg a \lor \neg c) $$

We can ask whether2 there is some assignment of values to these variables that makes the whole formula true. In this case, there is: $a = \text{true}, b = \text{true}, c = \text{false}$.

A formula with such an assignment is satisfiable. If no assignment works, it is unsatisfiable.

So SAT is about solving Boolean formulas; how often does that actually come up in the real world?

Well the mind-bending thing is that SAT is just one embodiment of a universal class of problems3 that appear all the time in the real world!

It turns out that there are many problems that despite surface-level semantic differences, are all actually the same computational problem4 just framed in a different way:

Graph coloring

Ccolors to every vertex so no connected pair has the same color.

Bin packing

Bfixed-capacity bins without letting any bin overflow.

Generalized Sudoku

n² × n²grid so every row, column, and box uses each symbol exactly once.

Traveling salesperson

L, is there a tour that visits every city once, returns home, and stays within budget?

Partition

Set cover

k, choose at most

ksets whose union contains every element.

Furthermore, these problems can be efficiently5 converted to and from each other, so an efficient solver for one problem can be used to solve all of them efficiently.

SAT as a constraint problem IR

Compilers once needed to be written from scratch for each new programming language and target architecture. Modern compilers instead translate source code to a shared intermediate language like LLVM IR. Code that optimizes the IR and lowers it to target architectures is written once and can be reused for any high level language frontend.

In much the same way, SAT is now used as a sort of intermediate representation for constraint problems.

Instead of writing a bunch of separate domain-specific solvers (which is very complex and error-prone), we simply build a new way to encode our problem as a SAT formula6 and we get the rest for free!

This is a great success! A common representation gives us shared parsers, shared proof formats, shared checkers, shared benchmarks, a dedicated conference, an annual competition, and decades’ worth of research and development in ever-more capable solvers.

This is why Donald Knuth calls SAT the “killer app” of computer science. Improving general purpose SAT solving is generally seen as a way to improve the entire field of constraint solving and solve lots of import real world problems.

In particular, SAT problems now have a well-defined, fairly standardized interface:

Input: DIMACS CNF

SAT problems are conventionally represented in conjunctive normal form (CNF) in a particular serialization format called DIMACS7 CNF (with extension .cnf).

A formula in conjunctive normal form is a collection of clauses, each of which is a disjunction of literals:

$$ \begin{aligned} F^{\text{cnf}} &= (C_1 \land C_2 \land C_3 \land \cdots) \ C_k &= (l_1 \lor l_2 \lor l_3 \lor \cdots) \ l &\in { v, \neg v } \end{aligned} $$

This means the top-level “gate” is always just a big AND-gate and each of the sub-gates are OR-gates over variables (or their negations).

It turns out that any (even arbitrarily-nested) Boolean formula can be efficiently8 converted to conjunctive normal form (CNF).

On-disk, we replace variable names with integer ids and encode each clause as a new 0-terminated line. Formula $F$ would be encoded as:

p cnf 3 3 1 -2 0 2 3 0 -1 -3 0
The header line p cnf 3 3 indicates that there are 3 variables and 3 clauses. A line like 1 -2 0 describes the clause $(a \lor \neg b)$.

Output: Models and Proofs

A SAT solver when provided with a DIMACS CNF file may output a satisfying assignment:

s SATISFIABLE v 1 2 -3 0
Here the SAT solver reports that the assignment $a = \text{true}, b = \text{true}, c = \text{false}$ satisfies the formula, which we can easily check by plugging in those values.

Alternatively, if the formula is unsatisfiable, the solver will output:

s UNSATISFIABLE
While very early solvers were simple enough algorithmically to reason about their correctness formally, modern solvers are way too complicated. So instead solvers generate certificates9 of unsatisfiability that can be checked efficiently.

The concept is basically to output a series of formula transformations (such as adding a new clause or new variables). Each step should be logically justifiable (we can’t turn a satisfiable formula into an unsatisfiable one). If we can show that you can derive the empty clause (i.e. false) from the original formula, then we have a valid proof.

Critically, this allows us to shift trust to a smaller, formally verified checker. We do not need to trust that the solver is correct, and we do not even care how it works internally.

No free lunch

Given this computational equivalence and the well-established shared representation of SAT problems, you might be tempted to think that there is some clean, elegant algorithm that can efficiently solve all formulas. And indeed, there might be if P=NP (but most people think otherwise10).

In practice, SAT solver development is a messy, empirical endeavor. Most modern solvers11 descend from the DPLL search procedure[1], now extended with the machinery of conflict-driven clause learning[2].
Within this framework, gains come from developing and assembling a canon of techniques: two-watched-literal propagation and VSIDS branching[3], rapid restarts[4], phase saving[5], and aggressive deletion of less useful learned clauses[6]. Much of traditional solver development therefore consists not of replacing the underlying search algorithm, but of engineering these mechanisms to interact well—making propagation cache-efficient, keeping the hot path small, and tuning when the solver branches, restarts, simplifies the formula, or forgets learned information.
Solvers further reshape the search space through variable and clause elimination[7], preprocessing formulas[8], or breaking symmetries[9].

The specific choices of which features to enable and how to configure them are driven by empirical observation: “does it make the solver faster on formulas I care about?” Typically the formulas developers care about usually include a broad range of real-world and crafted instances.

But we know that one solver does not fit all. In fact, quite the opposite. It is not surprising to see cases where solver A returns an answer in seconds while solver B takes hours on the same problem, yet see these rankings reversed for a different problem.

Sometimes we can pinpoint specific features that enable superior performance. For example CryptoMiniSat uses Gauss-Jordan Elimination to efficiently solve constraints that involve GF(2) arithmetic and thus works well on XOR-heavy (usually cryptography-related) formulas.

But this overhead (trying to identify suitable places to run Gauss-Jordan Elimination) is wasted12 on other formulas, so much so that the authors intentionally disabled Gauss-Jordan elimination when submitting CryptoMiniSat to the 2019 SAT competition.

Implementing such techniques in mainline solvers like Kissat is further hindered by non-trivial code complexity, especially considering that solvers will need to justify such transformations through checkable certificates of unsatisfiability.

To summarize, building general purpose solvers is fundamentally limited by the need to be good on average across a lot of differently shaped problems. This imposes a hard filter on the types of heuristics and algorithms that can be applied.

What a shame! How can we fix this?

A solution: LymphoSAT

LymphoSAT takes a radically different approach to SAT solver development: a technique which I’m tentatively calling domain-specific hyperspecialization.

We take some inspiration from the immune system (please humor my biologist framing). Humans have two forms of immunity: innate immunity is our general-purpose baseline defense system that provides defense against a wide range of pathogens, and adaptive immunity is a highly-specialized form of immunity that is tailored to a specific pathogen.

Adaptive immunity is essentially a form of (data-driven) memory that allows us to remember a specific pathogen and quickly mount a strong immune response if we encounter it again.

If current SAT solvers are the innate immune system, then LymphoSAT 13 is the adaptive immune system.

The key idea is to relax the requirement that a particular solver must be general-purpose and instead build a portfolio of highly-specialized solvers, each of which will only run on a specific shape of problem.

Intuitively, if we can guarantee that a particular solver will always encounter XOR-heavy formulas (i.e. fit to a particular domain), then suddenly it might make sense to enable Gauss-Jordan elimination and other specialized techniques that only work well on that domain (hyperspecialization).

Once we get creative, this is only the tip of the iceberg. We can start to implement not just better SAT heuristics, but we can completely redesign the whole solver algorithm and architecture if we limit ourselves to problems with specific shapes.

To give some examples:

  • for problems with consistent clause width, we can highly optimize our DIMACS parsing and data structure layout
  • for problems that have existing known good techniques, we can recover the high level structure and then deploy those techniques directly
  • for some problems we can recover semantic variables and use that to guide our search or tune SAT algorithms (i.e. picking important variables to branch on)
  • and so on…

Coding agents make domain-fit hyperspecialization viable

The idea of domain-fit hyperspecialization has always been theoretically possible, but before strong coding agents we would need to hand-write and tune all of these individual solvers (an incredibly complex and expensive task).

The key enabling factor that makes this possible now is that the economics of software engineering have changed. Building software (even complex software) no longer requires a supply of human engineers (notoriously slow, expensive, and not scalable). Now, in this ~~dystopian~~ beautiful world of coding agents, we can replace this requirement with tokens and compute, both of which are incredibly scalable, and in fact at least for SAT, it appears that the cost of such processes is already cheaper than what it would cost to employ humans.

SAT is particularly well suited to AI-driven domain-fit hyperspecialization because of the (relatively concise) input/output interface and the strong guarantees on correctness. We can verify generated models and proofs in lieu of trusting the code.14

LymphoSAT Architecture

In short, LymphoSAT consists of both detector modules function predicates that recognize specific problem shapes, and specialized solvers which run on a specific domain of problems and are responsible for generating models and proofs. Both of these are fully generated by AI agents (primarily GPT-5.5 in Codex) and evaluated on a withheld validation set. Solvers/detectors were generated for each of the 189 families in the Global Benchmark Database at the time of evaluation and the best ones were selected to be used in the composite solver. Kissat was deployed as a fallback solver if no specialized solver matched.

For more details about the architecture and implementation, see the LymphoSAT System Description. Source code will be released along with the paper.

The Future & Closing Thoughts

How should we build SAT solvers?

The vision of LymphoSAT is not that our future solvers will be ever-larger bundled portfolios15, but rather that a-priori general-purpose solvers are not necessary when we can generalize the process of construction itself.

Our future solvers may not be fixed codebases, but rather meta-solvers composed of code that is generated on the fly through LLM-powered agents.

How should we evaluate SAT solvers?

Traditional SAT competition evaluation is not well-suited for properly evaluating domain-fit hyperspecialization.

The vision of hyperspecialization is that upfront work (synthesizing a solver) is amortized over enough instances to make it worthwhile. Online specialization for unseen families is not possible in the current framework because:

  • solvers are run independently on each formula
  • there is no ability to invoke an LLM during evaluation

The only reason LymphoSAT works at all is because recent competitions sample 50% of formulas from historical families (in the global benchmark database) and thus we can “pre-specialize” and freeze these solvers for submission.

My recommendation for a future competition format would be to run solvers per-task rather than per-formula and to allow for online LLM invocation during evaluation, and to utilize only newly submitted formulas.

For example, provide 100 instances from a new family F to a solver and ask it to solve all of them. In some cases, specialization pays off within this batch: for example it may be more efficient to first invoke a coding agent to analyze and synthesize a solver and then run the specialized solver compared to simply running a general-purpose solver sequentially.

A similar kind of format has been tried before (the Configurable SAT Solver Challenge (CSSC)[10]) but was designed for solvers that performed family-specific tuning rather than full LLM-driven hyperspecialization.

How should we think about SAT research?

The emergence of hyperspecialization does not preclude the need for research in solving techniques, if anything it lowers the threshold at which a new technique becomes useful (because we can selectively enable/disable techniques). Furthermore, areas such as verified encodings (translating high-level problems into SAT) and improvements to proof systems (more expressible, more compact, more efficiently checkable) are still very much relevant.

In my observation, the dominant strategy during specialization was not to synthesize entirely novel techniques, but rather to interpolate, tune, and combine existing techniques. Thus (for now) agents still need a basis of knowledge to work from.

Why retain SAT as an IR?

A reasonable question is: why retain SAT as an IR if we are abandoning general-purpose solvers?

For now, I believe that consistent input/output and proof checking infrastructure remains valuable. Without that, it becomes more complex to validate the correctness of solutions.

However, we can also imagine extending the SAT IR on a case-by-case basis to allow for hints or metadata that do not influence proof checking. For example, right now when you encode to SAT, you throw away lots of semantic information which the (specialized) solver must re-infer. Why not just encode that information as comments in the DIMACS file? What other kind of information might be useful?

Generating UNSAT Proofs Programmatically

In recent news, LLMs have been used to prove or disprove conjectures, often capable of synthesizing long formal proofs.

An interesting aspect of creating specialized solvers is that for UNSAT problems, the challenge is not directly writing a proof, but writing a solver that programmatically generates a proof in the language of the proof system (e.g. DRAT/VeriPB). Such proofs are perhaps structurally simpler than open-ended formal proofs (e.g. in Lean) due to the restricted set of allowed operations, however the act of programmatically generating such proofs still appears to be a difficult task for frontier models.16

I believe this is one of the main aspects that would make SAT specialization an interesting benchmark problem for AI research.

Thanks for reading! Reach out if you have comments, questions, feedback, or if you’re interested in SAT as an LLM benchmark problem!

  • one based on a NVIDIA paper! ↩︎
  • typically we care about not just the answer (yes/no) but the actual model (i.e. assignment) that works. ↩︎
  • namely NP-complete problems ↩︎
  • as a decision problem ↩︎
  • in polynomial-time ↩︎
  • Of course, we could have decided to pick any other NP-complete problem as our “canonical problem” instead. My hunch is that the CNF representation of SAT is just so clean that it simplifies a lot of data structures. ↩︎
  • named after the Center for Discrete Mathematics and Theoretical Computer Science, created for one of the earliest SAT competitions ↩︎
  • in linear time if you allow introduction of auxiliary variables, see Tseytin Transformation ↩︎
  • there are several formats, DRAT / LRAT / VeriPB / … ↩︎
  • every overall winner of the SAT competition since at least 2015 has used CDCL as the core search algorithm. ↩︎
  • I have a hunch that there might be a fundamental reason why making a solver faster on some formulas might necessarilyincur overhead elsewhere, perhaps analogous to theno free lunch theoremin optimization. ↩︎
  • The name LymphoSAT comes from lymphocyte, the name for certain types of white blood cells in the immune system. ↩︎
  • Interestingly, in practice the concern of buggy solvers was already quite low: generated solvers rarely produced incorrect proofs. ↩︎
  • the need to bundle specialized solvers was only really necessary for the SAT Competition format ↩︎
  • Consider for example, that in many problems the size of the UNSAT proof may be many times larger than the context window of the LLM itself. ↩︎

References

  •     “A Machine Program for Theorem-Proving.” *Communications of the ACM*5(7), 394–397 (1962). doi:10.1145/368273.368557↩

    • “GRASP: A Search Algorithm for Propositional Satisfiability.” *IEEE Transactions on Computers*48(5), 506–521 (1999). doi:10.1109/12.769433↩

      • “Chaff: Engineering an Efficient SAT Solver.” Proceedings of the 38th Design Automation Conference, 530–535 (2001). doi:10.1145/378239.379017↩

        “The Effect of Restarts on the Efficiency of Clause Learning.” Proceedings of the 20th International Joint Conference on Artificial Intelligence, 2318–2323 (2007). paper↩

        “A Lightweight Component Caching Scheme for Satisfiability Solvers.” Theory and Applications of Satisfiability Testing – SAT 2007, 294–299. Springer (2007). doi:10.1007/978-3-540-72788-0_28↩

        “An Extensible SAT-solver.” Theory and Applications of Satisfiability Testing, 502–518 (2003).↩

        “Effective Preprocessing in SAT Through Variable and Clause Elimination.” Theory and Applications of Satisfiability Testing – SAT 20053569, 61–75. Springer (2005). doi:10.1007/11499107_5↩

        “Effective Auxiliary Variables via Structured Reencoding.” 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)271, 11:1–11:19. Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik (2023). doi:10.4230/LIPIcs.SAT.2023.11↩

        “Satsuma: Structure-Based Symmetry Breaking in SAT.” 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)305, 4:1–4:23. Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik (2024). doi:10.4230/LIPIcs.SAT.2024.4↩

        “The configurable SAT solver challenge (CSSC).” Artificial Intelligence243, 1–25. Elsevier (2017).↩