Domain-specific hyperspecialization (for SAT)

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¹

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 exchange expert human labor for token costs.

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 more 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 a 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 solving Boolean formulas.

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 whether² there is some assignment of values to these variables that make the whole formula true. In this case, there is : $a = \text{true}, b = \text{true}, c = \text{false}$ makes $F$ true.

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 problems³ 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 problem⁴ just framed in a different way:

Furthermore, these problems can be efficiently⁵ 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 formula⁶ 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 DIMACS⁷ 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_k &\in \{ v_k, \neg v_k \} \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 efficiently⁸ 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 certificates⁹ 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 offload trust into a (much 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 otherwise¹⁰).

In practice, SAT solver development is a messy, empirical endeavor. Most modern solvers 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 “cared about formulas” broadly covers different 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 wasted¹¹ 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-fit 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¹² 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 specific-shaped problems.

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) 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 we get strong guarantees on correctness. We can verify generated models and proofs in lieu of trusting the code.¹³

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.

Note that the specific form-factor of bundling a bunch of specialized solvers into a single pseudo-general-purpose solver is solely motivated by the competition format.

For more details about the architecture and implementation, see the LymphoSAT System Description.

I’m currently working on a long form paper with more details and experiments and will release the source code along with that paper.