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.

翻译：量子 LDPC (QLDPC) 码的精确距离计算在验证候选容错量子码构造中扮演核心角色，然而该问题的计算结构仍未被充分理解。尽管近期在 QLDPC 设计方面取得了显著进展，但控制精确距离计算实际可扩展性的算法原理，以及最适合此任务的精确求解器类别仍不明确。为回答这些问题，我们针对代表性码字，对基于 SAT 和 MaxSAT 的 QLDPC 精确距离计算公式进行了系统性研究。我们进一步将这些公式与若干已有的精确距离方法进行比较，以更好地理解精确 QLDPC 距离计算的算法全景。我们的研究挑战并修正了关于精确 QLDPC 距离计算的若干流行直觉。首先，尽管 QLDPC 奇偶校验具有丰富的异或（XOR）结构，但实际可扩展性似乎更多地受限于基数约束和优化边界的处理，而不仅仅是奇偶推理。因此，在我们的基准测试套件中，XOR 感知推理并未提供系统性优势。其次，长期以来被视为稀疏经典码精确距离计算基准范式的 Brouwer-Zimmermann 式搜索，在 QLDPC 场景中不再保持其传统的可扩展性优势。这一发现挑战了“对稀疏经典码成功的技术在 QLDPC 码中仍将占主导地位”的预期。第三，即使在不同 MaxSAT 求解器之间也存在显著的质性差异。在具有挑战性的基准测试上，分支定界 MaxSAT 显著优于基于不可满足核心的 MaxSAT，这表明求解器架构和优化策略在决定实际可扩展性方面起着关键作用。