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

• URL: http://arxiv.org/abs/2606.12445v1
• Date: Fri, 29 May 2026 15:34:33 GMT
• Title: SAT, MaxSAT, and SMT for QLDPC Distance Computation: A Large-Scale Empirical Study
• Abstract summary: We conduct a systematic study of SAT- and MaxSAT-based formulations for exact QLDPC distance computation across representative codes.<n>We refine several prevailing intuitions about exact QLDPC distance computation.<n>Branch-and-bound MaxSAT significantly outperforms unsat-core-based MaxSAT on challenging benchmarks.
• Score: 6.170087143925186
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• Towards Tensor-Network SAT-Solvers for Quantum-Classical Workflows [1.1916225387199697]
  Integrated HPC/QC systems aim to combine classical high-performance computing with quantum processors.<n>An integrated architecture must support aspects such as observability, which cannot be implemented using QPUs alone.
  arXiv  Detail & Related papers  (2026-08-03T10:36:30Z)
• Evaluating the Formal Reasoning Capabilities of Large Language Models through Chomsky Hierarchy [62.32144504442516]
  It is unknown whether SOTA LLMs can grasp the structured, hierarchical complexity of formal languages.<n>ChomskyBench is a benchmark for systematically evaluating LLMs through the lens of Chomsky Hierarchy.<n>ChomskyBench is composed of a comprehensive suite of language recognition and generation tasks designed to test capabilities at each level.
  arXiv  Detail & Related papers  (2026-04-03T04:06:39Z)
• ECCentric: An Empirical Analysis of Quantum Error Correction Codes [40.10865338207471]
  We introduce ECCentric, an end-to-end benchmarking framework for evaluating quantum error correction codes.<n>We conduct the first systematic benchmarking of major QEC code families against realistic, mid-term quantum device parameters.<n>Our findings suggest that trapped-ion architectures with qubit shuttling are the most promising near-term platforms.
  arXiv  Detail & Related papers  (2025-11-02T20:01:43Z)
• Unlocking Symbol-Level Precoding Efficiency Through Tensor Equivariant Neural Network [84.22115118596741]
  We propose an end-to-end deep learning (DL) framework with low inference complexity for symbol-level precoding.<n>We show that the proposed framework captures substantial performance gains of optimal SLP, while achieving an approximately 80-times speedup over conventional methods.
  arXiv  Detail & Related papers  (2025-10-02T15:15:50Z)
• Decoded Quantum Interferometry Requires Structure [1.121518046252855]
  We study the performance of Decoded Quantum Interferometry (DQI) on typical instances of MAX-$k$-XOR-SAT.<n>We prove that DQI is approximately Lipschitz under the quantum Wasserstein metric over many standard ensembles of codes.
  arXiv  Detail & Related papers  (2025-09-18T00:51:36Z)
• Extractors: QLDPC Architectures for Efficient Pauli-Based Computation [39.98920557126034]
  We propose a new primitive that can augment any QLDPC memory into a computational block well-suited for Pauli-based computation.<n>In particular, any logical Pauli operator supported on the memory can be fault-tolerantly measured in one logical cycle.<n>Our architecture can implement universal quantum circuits via parallel logical measurements.
  arXiv  Detail & Related papers  (2025-03-13T14:07:40Z)
• Performance of Parity QAOA for the Signed Max-Cut Problem [0.0]
  We investigate the performance of the Quantum Approximate Algorithm Optimization on the Parity architecture (Parity QAOA)<n>By comparing the algorithms at fixed circuit depth, we demonstrate that Parity QAOA outperforms conventional QAOA implementations based on SWAP networks.
  arXiv  Detail & Related papers  (2024-09-23T08:00:03Z)
• Provably Efficient UCB-type Algorithms For Learning Predictive State Representations [55.00359893021461]
  The sequential decision-making problem is statistically learnable if it admits a low-rank structure modeled by predictive state representations (PSRs) This paper proposes the first known UCB-type approach for PSRs, featuring a novel bonus term that upper bounds the total variation distance between the estimated and true models. In contrast to existing approaches for PSRs, our UCB-type algorithms enjoy computational tractability, last-iterate guaranteed near-optimal policy, and guaranteed model accuracy.
  arXiv  Detail & Related papers  (2023-07-01T18:35:21Z)
• Qubit efficient quantum algorithms for the vehicle routing problem on NISQ processors [48.68474702382697]
  Vehicle routing problem with time windows (VRPTW) is a common optimization problem faced within the logistics industry. In this work, we explore the use of a previously-introduced qubit encoding scheme to reduce the number of binary variables.
  arXiv  Detail & Related papers  (2023-06-14T13:44:35Z)
• End-to-end resource analysis for quantum interior point methods and portfolio optimization [63.4863637315163]
  We provide a complete quantum circuit-level description of the algorithm from problem input to problem output. We report the number of logical qubits and the quantity/depth of non-Clifford T-gates needed to run the algorithm.
  arXiv  Detail & Related papers  (2022-11-22T18:54:48Z)
• Logical blocks for fault-tolerant topological quantum computation [55.41644538483948]
  We present a framework for universal fault-tolerant logic motivated by the need for platform-independent logical gate definitions. We explore novel schemes for universal logic that improve resource overheads. Motivated by the favorable logical error rates for boundaryless computation, we introduce a novel computational scheme.
  arXiv  Detail & Related papers  (2021-12-22T19:00:03Z)
• Approximation Algorithms for Sparse Principal Component Analysis [57.5357874512594]
  Principal component analysis (PCA) is a widely used dimension reduction technique in machine learning and statistics. Various approaches to obtain sparse principal direction loadings have been proposed, which are termed Sparse Principal Component Analysis. We present thresholding as a provably accurate, time, approximation algorithm for the SPCA problem.
  arXiv  Detail & Related papers  (2020-06-23T04:25:36Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.