pith. sign in

arxiv: 2606.12445 · v1 · pith:UGY5KDY4new · submitted 2026-05-29 · 🪐 quant-ph · cs.IT· cs.PL· math.IT

SAT, MaxSAT, and SMT for QLDPC Distance Computation: A Large-Scale Empirical Study

Yu-Fang Chen , Seyed Mohammad Reza Jafari , Ching-Yi Lai This is my paper

Pith reviewed 2026-06-28 22:07 UTC · model grok-4.3

classification 🪐 quant-ph cs.ITcs.PLmath.IT
keywords QLDPCdistance computationMaxSATSAT solversquantum error correctionempirical studycardinality constraintssolver comparison
0
0 comments X

The pith

Branch-and-bound MaxSAT scales best for exact distance computation in quantum LDPC codes because cardinality constraints dominate over parity reasoning.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper runs a large-scale comparison of SAT, MaxSAT, and SMT formulations on the minimum-distance problem for several representative quantum low-density parity-check codes. It concludes that solver performance is driven primarily by how well each approach handles cardinality constraints and optimization bounds, not by specialized XOR reasoning. Traditional Brouwer-Zimmermann search, effective for classical sparse codes, loses its advantage here, while branch-and-bound MaxSAT clearly outperforms unsat-core MaxSAT on the hardest instances. These distinctions matter because exact distance verification is a necessary step when checking whether a new quantum code can support fault-tolerant computation. The study therefore refines which algorithmic features actually control scalability in this setting.

Core claim

Despite the XOR-rich structure of QLDPC parity checks, practical scalability appears to be governed more by the handling of cardinality constraints and optimization bounds than by parity reasoning alone. Accordingly, XOR-aware reasoning does not provide a systematic advantage across our benchmark suite. Second, Brouwer-Zimmermann-style search no longer maintains its traditional scalability advantage in the QLDPC setting. Third, branch-and-bound MaxSAT significantly outperforms unsat-core-based MaxSAT on challenging benchmarks.

What carries the argument

SAT- and MaxSAT-based encodings of the minimum-weight nonzero codeword search problem, compared across solver families on representative QLDPC instances.

If this is right

  • Cardinality constraint handling and bound management determine practical scalability more than parity-specific reasoning.
  • XOR-aware solvers do not deliver consistent gains on QLDPC distance tasks.
  • Brouwer-Zimmermann search loses its classical-code advantage when applied to quantum LDPC codes.
  • Branch-and-bound MaxSAT is the stronger choice among MaxSAT solvers for difficult distance instances.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Solver research for quantum codes should emphasize optimization-bound techniques over further parity enhancements.
  • The same empirical methodology could be applied to other quantum tasks such as decoding or syndrome extraction to identify architecture preferences.
  • Hybrid solvers that combine strong cardinality engines with lightweight quantum-structure awareness may become practical next steps.

Load-bearing premise

The selected set of representative QLDPC codes and benchmark instances is sufficient to support general claims about which solver classes are best suited to the task across the broader space of QLDPC constructions.

What would settle it

A new QLDPC code family on which an XOR-aware solver or Brouwer-Zimmermann search computes exact distances on larger instances or faster than branch-and-bound MaxSAT.

Figures

Figures reproduced from arXiv: 2606.12445 by Ching-Yi Lai, Seyed Mohammad Reza Jafari, Yu-Fang Chen.

Figure 1
Figure 1. Figure 1: Solver-behavior heatmap. Light colors indicate faster solved runtimes, while black cells [PITH_FULL_IMAGE:figures/full_fig_p010_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Solved-instances-versus-runtime plot for the curated representative solver configurations. [PITH_FULL_IMAGE:figures/full_fig_p013_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Full solver-behavior heatmap. We separate the solver family groups with white bars and [PITH_FULL_IMAGE:figures/full_fig_p043_3.png] view at source ↗
read the original abstract

Exact distance computation for quantum LDPC (QLDPC) codes plays a central role in validating candidate fault-tolerant quantum-code constructions, yet the computational structure of this problem remains poorly understood. Despite substantial recent progress in QLDPC design, it remains unclear which algorithmic principles govern the practical scalability of exact distance computation and which classes of exact solvers are best suited to this task. To address these questions, we conduct a systematic study of SAT- and MaxSAT-based formulations for exact QLDPC distance computation across representative codes. We further compare these formulations against several established exact-distance approaches in order to better understand the algorithmic landscape of exact QLDPC distance computation. Our study challenges and refines several prevailing intuitions about exact QLDPC distance computation. First, despite the XOR-rich structure of QLDPC parity checks, practical scalability appears to be governed more by the handling of cardinality constraints and optimization bounds than by parity reasoning alone. Accordingly, XOR-aware reasoning does not provide a systematic advantage across our benchmark suite. Second, Brouwer-Zimmermann-style search, long regarded as the benchmark paradigm for exact distance computation in sparse classical codes, no longer maintains its traditional scalability advantage in the QLDPC setting. This finding challenges the expectation that techniques successful for sparse classical codes remain dominant for QLDPC codes. Third, substantial qualitative differences arise even among MaxSAT solvers themselves. Branch-and-bound MaxSAT significantly outperforms unsat-core-based MaxSAT on challenging benchmarks, demonstrating that solver architecture and optimization strategy play a decisive role in practical scalability.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The manuscript presents a large-scale empirical study of SAT, MaxSAT, and SMT formulations for exact minimum-distance computation in quantum LDPC codes. It compares these against Brouwer-Zimmermann search and other established methods across a suite of representative QLDPC codes, concluding that practical scalability is governed primarily by cardinality-constraint handling rather than XOR/parity reasoning, that Brouwer-Zimmermann search loses its traditional advantage in the QLDPC setting, and that branch-and-bound MaxSAT solvers substantially outperform unsat-core-based MaxSAT on challenging instances.

Significance. If the reported performance orderings hold under the chosen benchmarks, the work supplies concrete, actionable guidance on solver selection for QLDPC distance computation—an essential validation step for fault-tolerant quantum-code constructions. The study is notable for its scale and for directly testing prevailing intuitions from classical coding theory against the quantum setting; the empirical nature of the comparisons constitutes a strength.

major comments (2)
  1. [Abstract] Abstract: the generalization that 'XOR-aware reasoning does not provide a systematic advantage across our benchmark suite' and that 'Brouwer-Zimmermann-style search no longer maintains its traditional scalability advantage in the QLDPC setting' rests on the assumption that the selected code families adequately sample the space of parity-check structures, rates, and constraint densities. No argument or sensitivity analysis is supplied showing that the observed ordering remains stable when qualitatively different constructions (e.g., higher-girth or irregular-weight families) are added.
  2. [Abstract] The abstract reports clear comparative outcomes (branch-and-bound MaxSAT vs. unsat-core, cardinality vs. parity dominance), yet the provided description contains no detailed experimental protocol, full data tables, or statistical controls sufficient to rule out post-hoc instance selection or solver-tuning effects that could alter the reported rankings.
minor comments (1)
  1. All code parameters, instance counts, and solver configurations should be tabulated in a single, machine-readable appendix to support independent reproduction.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive feedback on our empirical study. We address each major comment below with point-by-point responses, proposing targeted revisions where they strengthen the manuscript without altering its core claims.

read point-by-point responses

  1. Referee: [Abstract] Abstract: the generalization that 'XOR-aware reasoning does not provide a systematic advantage across our benchmark suite' and that 'Brouwer-Zimmermann-style search no longer maintains its traditional scalability advantage in the QLDPC setting' rests on the assumption that the selected code families adequately sample the space of parity-check structures, rates, and constraint densities. No argument or sensitivity analysis is supplied showing that the observed ordering remains stable when qualitatively different constructions (e.g., higher-girth or irregular-weight families) are added.

    Authors: The benchmark suite was deliberately assembled from representative QLDPC constructions appearing in the recent literature, covering a range of rates (approximately 0.1–0.5), column weights (3–10), and parity-check structures including hypergraph-product, lifted-product, and bicycle codes. These families already exhibit variation in girth and irregularity. While a comprehensive sensitivity study across every conceivable variant lies outside the scope of a single empirical paper, the consistent performance ordering across the tested instances supports the reported conclusions. We will add an explicit limitations paragraph in the discussion section that qualifies the scope of the benchmark and notes the absence of exhaustive sensitivity analysis on higher-girth or highly irregular families. revision: partial

  2. Referee: [Abstract] The abstract reports clear comparative outcomes (branch-and-bound MaxSAT vs. unsat-core, cardinality vs. parity dominance), yet the provided description contains no detailed experimental protocol, full data tables, or statistical controls sufficient to rule out post-hoc instance selection or solver-tuning effects that could alter the reported rankings.

    Authors: Section 3 of the manuscript provides the full experimental protocol, including solver versions and configurations, timeout and memory limits, hardware platform, and the precise criteria used to select the code instances and problem formulations. Appendix B contains complete runtime tables for all solvers and instances, together with median and quartile statistics. Solver parameters were fixed in advance according to published defaults or prior tuning studies; no post-hoc per-instance tuning was performed. To make these controls more immediately visible, we will insert a one-sentence pointer to Section 3 and the appendix directly into the abstract. revision: partial

Circularity Check

0 steps flagged

No circularity: empirical solver comparison on fixed benchmarks

full rationale

The paper reports measured runtimes, success rates, and qualitative performance differences across SAT/MaxSAT/SMT formulations on a concrete collection of QLDPC codes. All headline claims (XOR-aware reasoning confers no systematic advantage; Brouwer-Zimmermann loses its edge; branch-and-bound MaxSAT outperforms unsat-core variants) are direct summaries of experimental outcomes rather than derivations, fitted parameters renamed as predictions, or results justified solely by self-citation. No equation or theorem reduces to its own inputs by construction, and the study is self-contained against the reported benchmark instances.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

This is an empirical benchmarking study. No mathematical derivation or model fitting is claimed; therefore the ledger contains no free parameters, axioms, or invented entities.

pith-pipeline@v0.9.1-grok · 5815 in / 1208 out tokens · 17873 ms · 2026-06-28T22:07:47.837483+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

33 extracted references · 4 canonical work pages · 1 internal anchor

  1. [1]

    Automation of reasoning: 2: Classical papers on computational logic 1967--1970 , pages=

    On the complexity of derivation in propositional calculus , author=. Automation of reasoning: 2: Classical papers on computational logic 1967--1970 , pages=. 1983 , publisher=

    1967

  2. [2]

    International conference on principles and practice of constraint programming , pages=

    Towards an optimal CNF encoding of boolean cardinality constraints , author=. International conference on principles and practice of constraint programming , pages=. 2005 , organization=

    2005

  3. [3]

    International conference on principles and practice of constraint programming , pages=

    Efficient CNF encoding of boolean cardinality constraints , author=. International conference on principles and practice of constraint programming , pages=. 2003 , organization=

    2003

  4. [4]

    International Conference on Theory and Applications of Satisfiability Testing , pages=

    A cardinality solver: more expressive constraints for free , author=. International Conference on Theory and Applications of Satisfiability Testing , pages=. 2012 , organization=

    2012

  5. [5]

    International Conference on Theory and Applications of Satisfiability Testing , pages=

    PySAT: A Python toolkit for prototyping with SAT oracles , author=. International Conference on Theory and Applications of Satisfiability Testing , pages=. 2018 , organization=

    2018

  6. [6]

    27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024) , pages=

    Towards universally accessible SAT technology , author=. 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024) , pages=. 2024 , organization=

    2024

  7. [7]

    Webster, A

    Distance-Finding Algorithms for Quantum Codes and Circuits , author=. arXiv preprint arXiv:2603.22532 , year=

    work page arXiv

  8. [8]

    2022 IEEE 63rd Annual Symposium on Foundations of Computer Science (FOCS) , pages=

    Quantum tanner codes , author=. 2022 IEEE 63rd Annual Symposium on Foundations of Computer Science (FOCS) , pages=. 2022 , organization=

    2022

  9. [9]

    Nature , volume=

    High-threshold and low-overhead fault-tolerant quantum memory , author=. Nature , volume=. 2024 , publisher=

    2024

  10. [10]

    Nature Physics , volume=

    Constant-overhead fault-tolerant quantum computation with reconfigurable atom arrays , author=. Nature Physics , volume=. 2024 , publisher=

    2024

  11. [11]

    Proceedings of the 54th annual ACM SIGACT symposium on theory of computing , pages=

    Asymptotically good quantum and locally testable classical LDPC codes , author=. Proceedings of the 54th annual ACM SIGACT symposium on theory of computing , pages=

  12. [12]

    Journal on Satisfiability, Boolean Modelling and Computation , volume=

    RC2: an efficient MaxSAT solver , author=. Journal on Satisfiability, Boolean Modelling and Computation , volume=. 2019 , publisher=

    2019

  13. [13]

    A. R. Calderbank and P. W. Shor , title =. Phys. Rev. A , year =

  14. [14]

    A. M. Steane , title =. Phys. Rev. Lett. , year =

  15. [15]

    R. K. Radebold and S. D. Bartlett and A. C. Doherty , title =. arXiv preprint arXiv:2508.0509 , year =. 2508.0509 , archivePrefix=

    work page arXiv

  16. [16]

    Webster , title =

    M. Webster , title =. 2025 , howpublished =

    2025

  17. [17]

    13-a sat solver with conflict-clause minimization , author=

    Minisat v1. 13-a sat solver with conflict-clause minimization , author=. SAT , volume=

  18. [18]

    International Journal on Artificial Intelligence Tools , volume=

    On the glucose SAT solver , author=. International Journal on Artificial Intelligence Tools , volume=. 2018 , publisher=

    2018

  19. [19]

    International Conference on Computer Aided Verification , pages=

    CaDiCaL 2.0 , author=. International Conference on Computer Aided Verification , pages=. 2024 , organization=

    2024

  20. [20]

    Proceedings of SAT competition , volume=

    Lingeling, Plingeling and Treengeling entering the SAT competition 2013 , author=. Proceedings of SAT competition , volume=

    2013

  21. [21]

    International Conference on Theory and Applications of Satisfiability Testing , pages=

    Learning rate based branching heuristic for SAT solvers , author=. International Conference on Theory and Applications of Satisfiability Testing , pages=. 2016 , organization=

    2016

  22. [22]

    International Conference on Theory and Applications of Satisfiability Testing , pages=

    The mergesat solver , author=. International Conference on Theory and Applications of Satisfiability Testing , pages=. 2021 , organization=

    2021

  23. [23]

    Proceedings of SAT Competition , volume=

    The CryptoMiniSat 5 set of solvers at SAT Competition 2016 , author=. Proceedings of SAT Competition , volume=

    2016

  24. [24]

    End-to-End Formalization of Quantum Error Correction

    End-to-End Formalization of Quantum Error Correction , author=. arXiv preprint arXiv:2605.16523 , year=

    work page internal anchor Pith review Pith/arXiv arXiv

  25. [25]

    International conference on Tools and Algorithms for the Construction and Analysis of Systems , pages=

    Z3: An efficient SMT solver , author=. International conference on Tools and Algorithms for the Construction and Analysis of Systems , pages=. 2008 , organization=

    2008

  26. [26]

    International Conference on Tools and Algorithms for the Construction and Analysis of Systems , pages=

    cvc5: A versatile and industrial-strength SMT solver , author=. International Conference on Tools and Algorithms for the Construction and Analysis of Systems , pages=. 2022 , organization=

    2022

  27. [27]

    International Conference on Theory and Applications of Satisfiability Testing , pages=

    Open-WBO: A modular MaxSAT solver , author=. International Conference on Theory and Applications of Satisfiability Testing , pages=. 2014 , organization=

    2014

  28. [28]

    arXiv preprint arXiv:2601.15446 , year=

    Check-weight-constrained quantum codes: Bounds and examples , author=. arXiv preprint arXiv:2601.15446 , year=

    work page arXiv

  29. [29]

    and Lin, Hsuan-Yin and Rosnes, Eirik and Lee, De-Shih and Lai, Ching-Yi , booktitle=

    Mostad, Olai Å. and Lin, Hsuan-Yin and Rosnes, Eirik and Lee, De-Shih and Lai, Ching-Yi , booktitle=. Advancing Finite-Length Quantum Error Correction Using Generalized Bicycle Codes , year=

  30. [30]

    27th International conference on principles and practice of constraint programming (CP 2021) , year=

    Combining clause learning and branch and bound for MaxSAT , author=. 27th International conference on principles and practice of constraint programming (CP 2021) , year=

    2021

  31. [31]

    James Kwok,

    An efficient core-guided solver for weighted partial maxsat , author=. James Kwok,

  32. [32]

    MaxSAT Evaluation , volume=

    Evalmaxsat 2023 , author=. MaxSAT Evaluation , volume=

    2023

  33. [33]

    2026 , howpublished =

    Yu-Fang Chen , title =. 2026 , howpublished =

    2026