Pith. Sign in

REVIEW

Satisfying Quantum Codes: Physics-Informed and Hardware-Aware Code Design with SAT Solvers

PaperPDF from arXiv

data files

ReviewThe objections and verdict, as JSON Paper breakdownThe authors' claims, conditions and measurements, as JSON Signed receiptProof this review has not been altered
X Bluesky LinkedIn Reddit Hacker News
Ben DalFavero, William M. Watkins, Margarite L. LaBorde, Vincent Russo, Ethan Egger, Gregory Quiroz, Ryan LaRose

Quantum Physics · Submitted 24 Aug 2026 · 76 references

Pith's verdict: A useful SAT-based code design framework with credible numerical results, but the NP-completeness proof has a repairable gap and one key figure is under-specified.

T0 · AI review

How this review was made: An AI referee (deepseek-v4-flash) read the paper on August 28, 2026 and answered a fixed list of questions about it. T0 is the starting level every paper gets. The levels describe how deeply Pith has checked the paper, never the authors.

  1. T0 AI review An AI read the paper and answered a fixed list of questions.
  2. T1 Audit Automatic checks that the references and files the paper relies on exist and match.
  3. T2 Compute The paper's code or calculations re-run with the same results.
  4. T3 Formal statement The claims written out in a formal math language a computer can read.
  5. T4 Proof Those claims proved, and the proof checked by computer.

How Pith checks papers →

· 2 major objections · 6 minor · Ask about this paper · The compiled record · Read the full review →
Challenge this review Comment (0) Read on arXiv ↗
Cite ▾
arXiv ID2608.23460 (version 1)
Pith IDDZARECRW, Pith's permanent record of this paper and its review
CitationBen DalFavero, Ethan Egger, Gregory Quiroz, Margarite L. LaBorde, Ryan LaRose, Vincent Russo, William M. Watkins. "Satisfying Quantum Codes: Physics-Informed and Hardware-Aware Code Design with SAT Solvers." arXiv:2608.23460 (2026). https://pith.science/paper/DZARECRW
Cite this reviewBibTeX for Pith's review of this paper
Claim paper

Why Pith says this

Highlight any text to comment on it.

Referee report

How Pith checks papers → · Full audit of this paper →

The paper

The paper claims

Quantum code design is NP-complete, yet a SAT-solver formulation makes it practical and finds surface codes that beat the XZZX code under biased noise.

The reading

Quantum code design — choosing a stabilizer group that detects a specified set of errors — is, in general, NP-complete, so no efficient algorithm can cover every instance. However, the paper shows that the same problem, written as a Boolean satisfiability (SAT) instance, is solvable in practice for many relevant cases: modern SAT solvers find physics-inspired codes with up to 100 physical qubits in minutes and hardware-aware surface codes whose logical error rate under biased noise is lower than that of the XZZX surface code. The framework treats code discovery, code extension, and extension-with-mutation in one language, and can incorporate physical symmetries or measured error models as constraints. If right, it converts quantum code design from a hand-crafted art into an automated search, while explaining why better-than-surface codes have been so hard to find.

What carries the argument

The load-bearing object is the binary symplectic representation of Pauli strings: each n-qubit Pauli operator becomes a 2n-bit vector, multiplication is XOR, and commutation is a bilinear form over F2. In the SAT encoding, the unknown stabilizer generators are variables in that space; pairwise commutation of generators becomes clauses forbidding non-zero inner products, detection of each error becomes a disjunction of syndrome bits, and membership of an error in the stabilizer group becomes an XOR-style linear-system condition with slack variables. A maximum-satisfiability variant with clause weights from the device error model implements hardware-aware design, and a locality constraint (identity on qubits outside a given graph face) restricts the search to surface-code-like codes.

Extended reading notes

Core claim

On the paper's own terms, the central claim is that the k-code-design decision problem—given candidate Pauli stabilizers, an error set, and a target number of logical qubits, does a valid error-detecting stabilizer code exist—is NP-complete, via a polynomial-time reduction from k-set cover. The accompanying practical claim is that this worst-case hardness does not bind in practice: by encoding the unknown stabilizer generators in binary symplectic form as Boolean variables, all code criteria (abelian group, error detection, group membership) become CNF clauses, and modern SAT solvers solve instances at 100-qubit scale. Applying that solver to the Fermi-Hubbard symmetries yields distance-2 and distance-3 extensions that improve error-detected expectation values, and applying it to surface-code locality produces a family of codes whose maximum-likelihood logical error rate is lower than the XZZX surface code in the biased-noise regime.

Load-bearing premise

The proof that code design is NP-complete rests on a padding step in which one extra bit per candidate stabilizer is claimed to make the candidate set linearly independent; if duplicate candidate stabilizers need more than one extra bit, or the padding breaks commutativity, the hardness result does not follow as written.

Editorial extensions

If this is right

  • No polynomial-time algorithm can solve general quantum code design unless P = NP, so the search for better codes must rely on heuristics, specialized cases, or exact solvers with exponential worst case.
  • SAT-based code discovery is practical at 100 physical qubits, reaching a parameter regime that prior automated code-design methods did not reach.
  • Physics-inspired extensions raise the distance of symmetry-based detectors, improving error-mitigated expectation values with modest shot overhead.
  • Hardware-aware surface codes found by the solver have lower logical error rate than the XZZX surface code under biased noise, giving a concrete path to better memories on bias-dominated devices.
  • The empirical SAT–UNSAT transition predicts code existence in the region between the Gilbert-Varshamov and Singleton bounds, offering a runtime-based existence test for finite blocklengths.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • A direct, testable extension is to feed full measured device noise (including correlated or non-Pauli errors) into the max-SAT clause weights; the same search would then produce codes optimized for a specific machine, which the paper's simple bias model only approximates.
  • Since the solver samples satisfying assignments, one could add a secondary objective inside or after the search—such as decoder-friendliness or logical-operator structure—to rank the many valid codes the current framework treats as equally good.
  • The NP-completeness of the unconstrained problem suggests that constrained design goals the paper leaves open (e.g., prescribed logical operators or transversal gates) are at least as hard, so SAT-style search is likely the right tool there as well.
  • The fitted critical-error scaling, if validated at larger n, could be used as a cheap pre-filter to decide whether to attempt a given [[n,k,d]] design before committing solver time.
Original abstract

Although quantum error correction is widely believed to be necessary for impactful applications of quantum computers, the design of quantum error correction codes is largely done by hand, without respect to problem or hardware constraints. In this work, we present a highly general and flexible framework for the computational design of both physics-inspired and hardware-aware quantum codes. To do so, we formulate code design as a Boolean satisfiability (SAT) problem and show how to incorporate all required error correction criteria. We prove that code design is NP-complete, ruling out any efficient algorithm for designing codes in general. Nonetheless, we show that state-of-the-art SAT solvers are able to effectively find solutions for many practical problems. Notably, we are able to design physics-inspired codes with up to 100 physical qubits in minutes, and we design new hardware-aware codes for biased noise which have a lower logical error rate than state-of-the-art surface codes.

The compiled record

The paper's own sentences, arranged, kept beside the review and separate from it. Each label is drawn from a closed vocabulary; the number beside it is the probability the classifier gave that label. Numbers in the tables are the authors', checked by code. No sentence in this record was written by a model.

Compiled by classifier-1.13.0 via TypeSafe API, question bank abstract-p1-20260923, 2026-09-23: 1 request, 4,949 input tokens.

What the abstract itself states, as probabilities: claims first 0.08 · states limitation 0.90 · human participants 0.02 · controlled comparison 0.56 · randomized assignment 0.01 · states quantitative result 0.97 · compares with prior results 0.93 · mentions code or data availability 0.03.

The abstract, sentence by sentence

arXiv listing abstract v1. Results and the main claim are underlined; .

Although quantum error correction is widely believed to be necessary for impactful applications of quantum computers, the design of quantum error correction codes is largely done by hand, without respect to problem or hardware constraints. In this work, we present a highly general and flexible framework for the computational design of both physics-inspired and hardware-aware quantum codes. To do so, we formulate code design as a Boolean satisfiability (SAT) problem and show how to incorporate all required error correction criteria. We prove that code design is NP-complete, ruling out any efficient algorithm for designing codes in general. Nonetheless, we show that state-of-the-art SAT solvers are able to effectively find solutions for many practical problems. Notably, we are able to design physics-inspired codes with up to 100 physical qubits in minutes, and we design new hardware-aware codes for biased noise which have a lower logical error rate than state-of-the-art surface codes.

background contribution method result interpretation main claim

What the classifier reports for each sentence. The number is the probability it gave the label.
#sentencerolethe authors' own workstates the main conclusionstrength
s0 Although quantum error correction is widely believed to be necessary for impactful applications of quantum computers, the design of quantum error correction codes is largely done by hand, without respect to problem or hardware constraints. background 0.61 0.04 0.02 asserted 0.71
s1 In this work, we present a highly general and flexible framework for the computational design of both physics-inspired and hardware-aware quantum codes. contribution 1.00 0.89 0.11 asserted 1.00
s2 To do so, we formulate code design as a Boolean satisfiability (SAT) problem and show how to incorporate all required error correction criteria. method 0.98 0.94 0.07 asserted 1.00
s3 We prove that code design is NP-complete, ruling out any efficient algorithm for designing codes in general. result 0.68 0.90 0.13 asserted 1.00
s4 Nonetheless, we show that state-of-the-art SAT solvers are able to effectively find solutions for many practical problems. result 0.96 0.92 0.24 asserted 1.00
s5 Notably, we are able to design physics-inspired codes with up to 100 physical qubits in minutes, and we design new hardware-aware codes for biased noise which have a lower logical error rate than state-of-the-art surface codes. result 0.99 0.96 0.66 asserted 1.00

What kind of paper the classifier reports this is: method or tool 1.00 · evidence from simulation or computation 0.98.

What was examined, and what was not

sources read
  • arXiv listing abstract v1
not examined
  • full text
  • figures and tables
  • references and citing sentences
  • relations to other papers
levels run
  • P abstract
not run
  • S sections
  • T body sentences
  • C citations
  • R cross-paper relations

Every quoted sentence on this record is the authors'. Every label is from Pith's closed vocabulary, with the probability shown beside it. Every number in the measurements table is the authors', checked by code. Record as JSON

Figures
Figure 1. Overview of our quantum code design framework. Our framework enables two categories of code design: code
Figure 2. Illustration of distance-increasing extensions of
Figure 3. Demonstration of the SAT–UNSAT phase tran
Figure 4. Predicted existence of [[n, k, 3]] stabilizer codes as a function of the number of physical qubits n and logical qubits k. Dark blue denotes parameters for which code existence is guaranteed by the quantum Gilbert–Varshamov bound, while dark red denotes parameters excluded by the quantum Singleton bound. In the intermediate region, the empirical scaling model for the critical error-set size mb c(n, k, w), with w = d − 1 = 2, predicts satisfiable (light blue) and unsatisfi￾able (light red) k-Code Design instances. new codes, we study their performance relative to the baseline codes.…
Figure 5. Demonstration of improved accuracy in error
Figure 6. Time to extend the Fermi-Hubbard code (46) from distance d = 1 to distance d = 3 vs. the number of qubits/stabilizers m added. Timing is shown for both n = 48 and n = 100 physical qubits. As discussed in Sec. VII and demonstrated in
Figure 7. Sum of the rates of all undetectable weight-two
Figure 9. Relationship between the natural code-design density
Figure 10. Finite-size SAT–UNSAT transitions for random code-design instances with
Figure 12. Comparison of the observed critical mc, ob￾tained from individual logistic fits, with the values predicted by the empirical finite-size scaling model. Agreement with the dashed y = x line indicates accurate prediction of the lo￾cation of the SAT–UNSAT crossover across different (n, k, w) for training and validation sets. Appendix E: Additional Numerical Results and Discussion for Physics-Informed Code Design With the simple noise model detailed in Section VIII, the result for the distance-3 code is almost perfect (see
Figure 13. Collapse of the satisfiability transitions under
Figure 14. (top) Expectation value of logical observable
Figure 15. Time to use SAT to increase the FH code from dis

Showing 13 of the paper's 15 figures. See all figures in the PDF ↗ Figures reproduced from arXiv:2608.23460 by the authors.

References
How the literature uses it

What this paper does with the arXiv papers it cites

Each citing sentence is taken from the citing paper's LaTeX source and typed by Pith's classifier. A label appears at probability 0.8 or more (0.95 for support), a contest at 0.7 or more; the quoted words are the citing authors'. How each label was checked · JSON

What it cites · 11 sentences without a confident label

Builds on 1 paper
  • This can be seen as a generalization of quantum error detection/symmetry verification [ref] as we show how to iteratively build new codes to increase performance as measured by accuracy of computed expectation values.

    Quantum Error Mitigation using Symmetry Expansion · Physics-Informed Code Design · 0.91

Compares with 1 paper
Cites as background 4 papers
  • The quantum Gilbert–Varshamov (QGV) bound provides a sufficient condition for the existence of an $[[n,k,d]]$ stabilizer code [ref] [equation] while the quantum Singleton bound provides a necessary condition [ref] [equation] Thus, codes satisfying Eq. [ref] are guaranteed to exist, whereas codes violating Eq. [ref] cannot exist.

    Nonbinary stabilizer codes over finite fields · Phase Transitions in the k-Code Design Problem · 0.85

  • Previously-studied approaches to designing quantum codes often employ heuristic search through the set of possible check matrices [ref] or the solution to difficult optimization problems such as game-theoretic methods [ref] , maximum clique cover [ref] , or the use of reinforcement learning to optimize a cost function [ref] .

    Game-Theoretic Discovery of Quantum Error-Correcting Codes Through Nash Equilibria · Complexity of Quantum Code Design · 0.94

  • Future work in designing entanglement-assisted codes [ref] , subsystem codes [ref] , and non-abelian codes will likely lead to additional impact.

    Correcting Quantum Errors with Entanglement · Conclusion · 0.86

Discussion

Disagree with the review, or know something it missed? Leave a comment, highlight any passage above to comment on it, or challenge this review formally.