Accelerating hybrid XOR–CNF Boolean satisfiability problems natively with in-memory computing

Why faster problem solving matters

Many tasks that shape our daily lives—from securing online communications to designing faster electronics—boil down to asking a computer a yes-or-no question: does there exist a combination of switches that makes this big logical rule come out true? This is the Boolean satisfiability, or SAT, problem. SAT is famously hard, and as these tasks grow in size and importance, the time and energy needed to solve them becomes a major bottleneck. This paper explores a new way to turbocharge SAT solving by redesigning both the math and the hardware so they work together inside a special type of memory chip.

Turning tangled rules into simpler building blocks

Traditional SAT solvers usually describe problems using one style of logical rule, built from “OR” conditions. But many real industrial problems—such as decoding wireless signals, testing chips for faults, or attacking certain cryptographic schemes—naturally mix “OR” with “exclusive OR” (XOR), a kind of parity check that flips when any single input flips. Today’s tools often force these XOR rules to be rewritten using only OR, which swells the size of the problem and slows everything down. The authors instead keep both types of rules, creating a hybrid description that is closer to how the problems arise in practice.

Getting more done with fewer pieces

The researchers carefully compare this hybrid description to the traditional one across several benchmark families drawn from cryptography and a classic test problem called minimal disagreement parity. By automatically reconstructing hidden XOR structure and applying smart simplifications first, they show that the mixed representation can shrink the number of variables by up to several times and cut the number of rules by roughly a factor of four to five. In other words, the same logical question can often be asked with far fewer moving parts when you allow XOR and OR to coexist. Smaller problems are easier not just for software, but also for specialized hardware that has strict limits on how many rules it can store at once.

Letting memory chips do the thinking

To exploit this leaner description, the team designs a dedicated “in-memory computing” accelerator. Instead of shuttling data back and forth between a processor and memory, this device performs much of the computation where the data reside, inside grids of tiny electronic elements called memristors. They adapt a known local-search strategy, WalkSAT, into a new variant called WalkSAT-XNF that natively handles the combined XOR–OR rules. Each step of the algorithm—checking which rules are broken, estimating how much each switch matters, adding a bit of noise to escape dead ends, and flipping the best candidate—is implemented directly in analog circuitry on the crossbar arrays, with simple support circuits choosing which variable to flip next.

Proving it works in the lab and in simulations

The authors first build a small prototype using memristor chips to demonstrate that the analog hardware can faithfully evaluate clauses and guide the search, even in the presence of manufacturing variations and electrical noise. Experiments on a modest-sized test instance show that the hardware’s behavior closely matches ideal simulations. They then model a more advanced 28-nanometer design and benchmark it on families of cryptographic and parity problems. Because the hybrid description packs more information into fewer clauses, the accelerator needs far less on-chip memory and consumes much less energy per step than a version restricted to OR-only rules. Overall, the hybrid in-memory solver achieves about a tenfold speedup and roughly a thousandfold improvement in energy efficiency compared with leading software SAT solvers running on conventional CPUs.

What this means for future computers

In plain terms, the work shows that we can solve certain notoriously tough yes-or-no problems much faster and with far less power by matching the way we write the logical rules to the way a new kind of memory-based hardware computes. By natively supporting both XOR and OR rules inside the chip, the proposed accelerator can tackle realistic cryptographic, communications, and circuit-design tasks using smaller, cooler, and quicker hardware. As computing systems increasingly strain against energy and speed limits, such problem-specific, in-memory approaches could help keep critical digital infrastructure secure and efficient.

Citation: Im, H., Böhm, F., Pedretti, G. et al. Accelerating hybrid XOR–CNF Boolean satisfiability problems natively with in-memory computing. Nat Commun 17, 2922 (2026). https://doi.org/10.1038/s41467-026-69465-2

Keywords: Boolean satisfiability, in-memory computing, memristor crossbar, hardware accelerators, cryptography