Fermihedral: On the Optimal Compilation for Fermion-to-Qubit Encoding

To simulate electrons and other fermions on a quantum computer you must translate them into the language of qubits, and that translation — the fermion-to-qubit encoding — is not unique, with different choices producing wildly different circuit costs; this work from Penn and AWS recasts the hairy problem of finding the cheapest valid encoding, tangled in linear algebra and number theory, into a plain Boolean satisfiability problem a solver can crack, then drops the one constraint that is almost never binding to scale up — cutting gate counts by up to 35 percent and circuit depth by up to 60 percent, and sharpening real quantum simulations on IonQ hardware.

The argument in one glance

Problem

Fermions must be translated to qubits, and the translation is costly

Simulating fermionic systems — electrons in molecules, particles in materials and field theory — is a marquee use of quantum computers. But quantum computers are made of qubits, which follow different statistical rules than fermions, so a fermionic system cannot be mapped onto qubits directly. It must be translated by a fermion-to-qubit encoding into strings of qubit operations. That encoding is not unique, and the choice strongly determines how many gates and how much depth the resulting circuit needs.
What people did

Use a hand-constructed encoding like Jordan-Wigner or Bravyi-Kitaev

The standard approach is to reach for a known encoding — Jordan-Wigner, Bravyi-Kitaev, or an asymptotically-optimal construction — each derived theoretically, once and for all, from the mathematics of fermionic operators. These are correct, general, and widely implemented in quantum toolkits.
Why it fell short

Fixed encodings ignore the actual system and are far from optimal

These encodings are built in a Hamiltonian-independent way, without regard to the specific system being simulated, so even the asymptotically-optimal ones are far from the actual cheapest circuit for a given molecule or model, since Hamiltonians from different domains differ enormously. Finding the truly optimal encoding is a highly complex constrained optimization whose constraints mix linear algebra and number theory, and how to even unify and formalize them together was an open problem.
This paper's idea

Recast finding the optimal encoding as a Boolean SAT problem

Fermihedral uses Pauli algebra to rewrite all the encoding constraints and the cost objective into Boolean variables and expressions, turning the search for the optimal fermion-to-qubit encoding into a Boolean satisfiability problem that a fast SAT solver can crack. To scale past the exponential blowup of clauses, it drops the one constraint that is almost never binding (with exponentially small failing probability) and adds simulated annealing — yielding encodings with up to 35 percent fewer gates and 60 percent less depth, and sharper simulations on real IonQ hardware.

Why this problem is worth solving

The reason a translation is even needed comes down to a deep difference between fermions and qubits.

Fermions obey the Pauli exclusion principle and a peculiar rule: exchanging two of them flips the sign of the whole quantum state. Qubits do not behave this way — swapping two qubits changes nothing. So a fermionic mode cannot simply be identified with a qubit; the fermionic statistics have to be reproduced on the qubits by hand. This is done through a fermion-to-qubit encoding, which represents the operators that describe a fermionic system as Pauli strings — tensor products of the single-qubit operations X, Y, Z, and identity, one per qubit. Concretely, the encoding must find Pauli strings for a set of Majorana operators (two per fermionic mode) that together satisfy a group of constraints: any two must anticommute, they must be algebraically independent, and, optionally, they must map the fermionic vacuum to the all-zero qubit state. These constraints are what guarantee that the qubit system faithfully reproduces the fermionic one. And here is the crux: many different sets of Pauli strings satisfy the constraints, so the encoding is not unique — and different valid encodings, when compiled into an actual quantum circuit, can have wildly different gate counts and circuit depths. On today’s noisy quantum hardware, where every extra gate adds error, choosing the encoding that yields the cheapest circuit can be the difference between a usable simulation and noise.

To turn “cheapest circuit” into something a solver can optimize, the paper uses a clean proxy for cost.

A quantum simulation ultimately has to implement the time-evolution of the system’s Hamiltonian, and the standard way to do that (Trotterization) breaks the Hamiltonian into its Pauli strings and implements the evolution of each one as a small circuit. The key fact is that a Pauli string’s circuit only touches the qubits whose operator is non-identity: a qubit assigned the identity operator gets no gates at all. So the number of gates needed to implement a Pauli string is roughly proportional to its Pauli weight — the count of non-identity operators in it. A string like identity-identity-X-X has weight two and costs about two qubits’ worth of gates. This gives the optimization a concrete target: an encoding whose Pauli strings have the smallest total Pauli weight will produce the fewest gates when the Hamiltonian is compiled, before any downstream optimization. Minimizing total Pauli weight is therefore a faithful, tractable stand-in for minimizing the real circuit cost, and it is exactly what Fermihedral sets out to minimize — either for the generic Majorana operators (Hamiltonian-independent) or for the specific target system’s Hamiltonian (Hamiltonian-dependent), which gives the truly optimal encoding for that system.

What people did before, and where it broke

Jordan-Wigner and Bravyi-Kitaev encodings. Use a fixed, hand-derived transformation from fermionic operators to Pauli strings, implemented in every quantum toolkit. Where it broke. They are constructed without any knowledge of the specific system, so their circuit cost is generic, not tailored, and far from optimal for a given molecule or model.
Asymptotically-optimal encodings. Derive encodings whose Pauli weight scales optimally as the system grows. Where it broke. Optimal asymptotic scaling still leaves large gaps in the actual cost for real, finite systems, because Hamiltonians from chemistry, materials, and field theory differ enormously and none is the target of the construction.
Generic quantum-compiler optimization passes. Run gate-cancellation, gate-rewrite, and routing passes to shrink the circuit after the encoding is chosen. Where it broke. These are small, local circuit transformations; they cannot change the encoding, which shapes the entire Hamiltonian-simulation circuit, so a poor encoding cannot be fixed downstream.
The gap. No method found the actual optimal encoding for a specific Hamiltonian, because the constraints — anticommutativity, algebraic independence, vacuum preservation, and implementation cost — live in a tangle of linear algebra and number theory that no one had unified into a single solvable formulation. Recasting the whole thing as Boolean satisfiability is what closes that gap.

How Fermihedral works

From a linear-algebra tangle to a SAT problem a solver can crack

↓ →
new
↓ →
new
↓ →
new
↓ →
new
↓ →
new

The idea

Recast a tangled domain problem as a plain SAT problem and let a solver do the work. The constraints on a valid encoding were scattered across linear algebra and number theory, with no unified formulation, until Fermihedral used Pauli algebra to rewrite every one of them — and the cost objective — as Boolean expressions, so that finding the optimal encoding becomes Boolean satisfiability, a problem decades of fast solvers already crush. Reducing an awkward, bespoke problem to a classic, well-tooled one and inheriting its mature machinery is the same move the concurrency data-structure work covered elsewhere on this site makes, casting a specialized reachability question into the textbook problem of suffix minima so a standard efficient structure solves it directly.

Drop the expensive constraint that is almost never binding. The single biggest cost in the formulation is the algebraic-independence constraint, which spawns an exponential number of clauses — yet a randomly chosen valid encoding violates it only with an exponentially small probability, confirmed numerically. So Fermihedral simply omits it at scale, trading a provable guarantee for a negligible chance of an invalid answer, and removes the bottleneck. Discarding work whose omission fails only with a tiny, bounded probability, rather than paying for a guarantee that is almost always vacuous, is exactly the bargain the hyperdimensional early-termination work covered elsewhere on this site strikes, stopping a computation the moment a statistical test says the remaining work would almost surely not change the result.

Fix the global structure up front, because local passes cannot. The encoding is a global choice that reshapes the entire simulation circuit, so no amount of local gate-cancellation or routing afterward can rescue a bad one; the leverage is in getting the encoding right before compilation even begins. Attacking the one global decision that determines everything downstream, rather than optimizing the pieces locally, is the same principle the permutable-operator quantum-compilation work covered elsewhere on this site follows, choosing a global structured schedule that local search over the circuit could never reach at scale.

Following the search for an optimal encoding

Finding a minimal-weight encoding with a SAT solver

Tracing the search shows constraints, objective, and solver working together.

Step 1 of 5

State the goal in terms of Pauli strings

For a target fermionic system with N modes, the goal is to find 2N Majorana operators — each a Pauli string of qubit operators — that anticommute pairwise and are independent, while making the total Pauli weight (the count of non-identity operators) as small as possible.

Smaller total weight means fewer gates in the compiled simulation circuit.

Why it works

Pauli algebra makes the constraints Boolean. The encoding’s constraints are tangled in linear algebra and number theory → but Pauli algebra lets each be rewritten as Boolean expressions over two-bit operators → so the whole search becomes a plain SAT problem a mature solver can crack.
Pauli weight is the real cost. A Pauli string’s circuit only touches its non-identity operators → so minimizing the total Pauli weight minimizes the gate count of the simulation circuit → so the solver optimizes the very thing that makes the circuit expensive.
Tailoring beats generic constructions. Existing encodings are built without knowing the specific Hamiltonian → but SAT can encode that Hamiltonian’s actual cost directly → so Fermihedral finds the encoding optimal for that system, not merely asymptotically optimal.
The exponential constraint is almost never needed. Algebraic independence generates exponentially many clauses → but a random valid encoding violates it with only exponentially small probability → so dropping it removes the bottleneck while keeping the answer almost surely correct.
A pure Boolean formulation stays fast. Casting everything as Booleans avoids slow number-theory reasoning → and a linear-time normal-form conversion keeps the clause count from blowing up → so a fast SAT solver handles systems up to around 19 fermionic modes.

What it costs (trade-offs and scope)

SAT is NP-complete, so scale is the ceiling. Solving times grow fast and are long even at modest sizes; the prototype used a single-threaded solver on a small machine, and reaching much larger systems would need distributed solving on a cluster, which is untested.
Large-scale results are approximate, not provably optimal. Beyond the sizes where the exact solver runs, the scaling techniques (dropping algebraic independence, simulated annealing) return near-optimal encodings, with a small, exponentially-decreasing chance of an invalid one that must be checked.
The cost model is a proxy applied before downstream compilation. Pauli weight predicts gate count only before the compiler’s later routing and cancellation passes; Fermihedral optimizes the encoding, which those local passes cannot fix, but the final circuit still depends on them.
It optimizes the encoding, not the whole pipeline. The method finds the best fermion-to-qubit map and its Trotterized circuit; connectivity-aware routing, error mitigation, and gate synthesis remain separate stages that still apply.
Evaluated to modest sizes and one real device. The exact solver was used up to 8 fermionic modes and the scaled method up to 19, and real-hardware validation was limited to a small molecule on one IonQ device by current fidelity.
The failing-probability guarantee rests on a statistical assumption. Ignoring algebraic independence is justified by assuming the Pauli operators are distributed uniformly and independently per index — well-supported numerically, but an assumption.

The evaluation

Three ways to choose a fermion-to-qubit encoding

Property	Fixed encodings (JW / BK)	Asymptotically-optimal encodings
Tailored to the specific Hamiltonian		No
How the encoding is found	Hand-constructed theory	Theoretical construction
Optimality	Not cost-optimal
Circuit cost versus standard	Baseline	Better scaling, not actual cost

Three ways to choose a fermion-to-qubit encoding, evaluated across electronic-structure, Fermi-Hubbard, and SYK systems against the Jordan-Wigner and Bravyi-Kitaev baselines. By recasting the search as Boolean satisfiability, Fermihedral finds encodings with 10 to 60 percent lower Hamiltonian implementation cost, 15 to 35 percent fewer gates, and 15 to 60 percent less circuit depth — for example about 20 percent fewer single-qubit gates and 35 percent fewer two-qubit gates than Bravyi-Kitaev — and its scaling techniques hold up to 19 fermionic modes with negligible failing probability. On the IonQ Aria-1 device, its encoding gave the most accurate hydrogen-molecule simulation, closest to the true energy with the smallest variance.Underlined values explain themselves when clicked.

Where this stops working

What to keep in mind

Fermihedral is a clever reframing: it takes a problem that mixed linear algebra, number theory, and combinatorial search — finding the cheapest fermion-to-qubit encoding — and shows that Pauli algebra collapses all of it into Boolean satisfiability, where decades of fast solvers apply. The payoff is concrete and, unlike prior encodings, tailored to the actual system: 10 to 60 percent lower implementation cost, up to 35 percent fewer gates and 60 percent less depth, and measurably sharper simulations on a real IonQ device. The two scaling techniques — dropping the almost-never-binding algebraic-independence constraint and adding simulated annealing — extend it well past what an exact solver alone could reach. Read it with its scope. SAT is NP-complete, so scale is fundamentally limited (the exact method reaches 8 fermionic modes, the approximate one 19, on a single-threaded solver); the large-scale answers are approximate, with a small statistical chance of invalidity that must be checked; and the guarantee rests on an assumption about how Pauli operators distribute. It optimizes the encoding as a proxy (Pauli weight) before downstream compilation, not the entire circuit pipeline, and real-hardware validation was one small molecule on one device. The durable lesson is that a hard, domain-specific optimization can sometimes be dissolved by finding the right formal language for it — and that once a problem is expressed as satisfiability, you can even afford to discard the expensive constraints that almost never matter.

Background

Why the compiler is where quantum simulation is won

It helps to see Fermihedral within the reality of near-term quantum computing: hardware is noisy and small, so the circuits that actually produce useful answers are the shortest, lowest-gate-count ones, and enormous leverage sits in the compilation choices that determine circuit size before a single gate runs. The fermion-to-qubit encoding is one such choice, and because it shapes the whole simulation circuit, getting it right can matter more than any downstream optimization. The work on synthesizing quantum error-correcting codes covered elsewhere on this site sits in the same spirit, treating the search for an optimal quantum structure as a formal optimization or search problem to be solved by machine rather than constructed by hand, and letting a solver discover structures better than human-derived ones. The broad lesson is that as quantum hardware inches toward usefulness, some of the biggest wins come not from more qubits but from formalizing the design choices around them — encodings, codes, schedules — as problems that automated tools can optimize, so the scarce, precious resource of reliable circuit depth is spent as efficiently as possible.

If you remember only three things

1. Simulating fermionic systems (electrons in molecules, particles in materials and field theory) is a leading use of quantum computers, but qubits obey different statistics than fermions, so a fermion-to-qubit encoding must translate the fermionic operators into Pauli strings (products of single-qubit operators) that preserve fermionic behavior via constraints like pairwise anticommutativity and algebraic independence. The encoding is not unique, and the choice strongly determines circuit gate count and depth. Existing encodings (Jordan-Wigner, Bravyi-Kitaev, asymptotically-optimal ones) are built without regard to the specific Hamiltonian, so they are far from the actual cheapest circuit, and finding the optimal one is a constrained optimization tangled across linear algebra and number theory.
2. Fermihedral recasts the search as Boolean satisfiability. Each Pauli operator becomes two Boolean bits, and Pauli algebra rewrites the constraints and the cost objective (total Pauli weight — the count of non-identity operators, roughly proportional to gate count) as Boolean expressions, so a fast pure-SAT solver finds the provably minimal-weight encoding by iteratively tightening a target weight. Because the algebraic-independence constraint generates an exponential number of clauses but is violated with only exponentially small probability, Fermihedral drops it at scale (verified numerically), and adds simulated annealing for the largest systems — extending the method with negligible failing probability. It can optimize for the generic operators (Hamiltonian-independent) or the specific system (Hamiltonian-dependent).
3. Across electronic-structure, Fermi-Hubbard, and SYK systems, Fermihedral beats the Bravyi-Kitaev and Jordan-Wigner baselines with 10 to 60 percent lower implementation cost, 15 to 35 percent fewer gates (about 20 percent single-qubit and 35 percent two-qubit gates), and 15 to 60 percent less depth, with more accurate noisy simulations and a real IonQ Aria-1 run giving the closest hydrogen-molecule energy at smallest variance. Its limits: SAT is NP-complete so scale is capped (exact to 8 modes, approximate to 19, single-threaded); large-scale answers are approximate with a small checkable chance of invalidity; the guarantee assumes a Pauli-operator distribution; and it optimizes the encoding proxy, not the full downstream compilation pipeline.

Check yourself

Check your understanding

1. Why must a fermionic system be translated by an encoding rather than mapped directly onto qubits?
2. What is "Pauli weight," and why does Fermihedral minimize it?
3. How does Fermihedral turn the problem into something solvable, and how does it scale up?
4. Which statement best reflects the results and limitations of Fermihedral?

Sources

The paper is “Fermihedral: On the Optimal Compilation for Fermion-to-Qubit Encoding” by Yuhao Liu, Shize Che, Junyu Zhou, Yunong Shi, and Gushu Li, published at ASPLOS 2024, DOI 10.1145/3620666.3651371. The authors are at the University of Pennsylvania and AWS Quantum Technologies.

This explainer is written from the full text of the paper (the author-posted arXiv version, 2403.17794, matching the ASPLOS proceedings). Everything above comes from the paper’s own sections: the introduction motivating fermionic simulation and the fermion-to-qubit encoding gap; the background on Pauli strings, the Pauli-string-to-circuit conversion via Trotterization, and Pauli weight as a gate-count proxy; the fermionic-system description with Majorana operators and the four encoding constraints (anticommutativity, linear independence, algebraic independence, vacuum-state preservation) and the two objectives (Hamiltonian-independent and dependent); the SAT formulation (two-bit Pauli-operator encoding, Boolean multiplication and anticommutativity truth tables, the weight-minimization loop starting from the Bravyi-Kitaev baseline, and the pure-SAT conversion via the Tseitin transformation with its variable and clause counts); the two scaling techniques (ignoring algebraic independence with its one-over-four-to-the-N failing probability and numerical validation, and simulated annealing); and the evaluation against Jordan-Wigner and Bravyi-Kitaev — the per-operator Pauli-weight reductions (11.16 percent small-scale, 17.36 percent at 9-19 modes, with a projected 36.38 percent), the Hamiltonian-dependent reductions (37.26 percent Full SAT, 21.63 to 23.71 percent with annealing, up to 40 percent), the compiled gate-count reductions (about 20 percent single-qubit, 35 percent CNOT), and the noisy-simulation and real-system IonQ Aria-1 hydrogen-molecule results.