A presentation-style walkthrough of the paper’s motivation, formulations, benchmark design, and the main empirical takeaways for exact QLDPC distance computation.
Modern fault-tolerant code families need exact distance certification, but the solver landscape is still poorly understood.
Compare SAT, SMT, MaxSAT, and strong non-SAT baselines on a shared benchmark suite and identify what actually drives scalability.
The hard part is not just finding a candidate logical operator, but proving there is no better one below a target weight.
Encode stabilizer checks such as even-parity XOR relations.
Enforce that the candidate is not generated by stabilizer rows.
Use a cardinality constraint to ask whether wt(x) ≤ w.
Exact distance is found by solving a sequence of SAT instances for increasing thresholds.
Suppose a row of HX touches qubits 1, 2, and 4, and we test whether there is a logical operator of weight at most 2.
Parity and nontriviality constraints must always hold.
Each variable gets a soft clause favoring 0, so the solver minimizes operator weight directly.
This avoids repeated threshold search and turns the task into an optimization problem.
For four qubits, keep parity and nontriviality as hard clauses, then add one soft clause per variable:
The paper studies not only solver families, but also how the encoding interface changes solver behavior on the same QLDPC task.
| Family | Representative instances | Count | Row wt. | Col wt. | Structural character |
|---|---|---|---|---|---|
| BB / GB | BB 72 12 6, BB 144 12 12, BB 288 12 ?, GB 144 12 8, GB 144 12 12 | 9 | 6-8 | 3-5 | Algebraically regular, sparse circulant-style structure |
| LP | LP 34 20 2, LP 238 44 6, LP 544 80 12, LP 1768 224 ? | 8 | 8 | 5 | Larger lifted-product search spaces with weaker regularity |
| TN | TN 36 8 3, TN 72 8 8, TN 144 2 13, TN 250 10 15, TN 360 4 ? | 10 | 6-12 | 4-9 | Expander/Tanner style structure and difficult transition-region behavior |
The naming convention is roughly {family} {n} {k} {d}, where ? denotes a distance not yet certified in the source benchmark collection.
Across all three families, the paper evaluates 27 total instances spanning small easy cases through hard transition-region benchmarks.
| Axis | What varies | Role in the study |
|---|---|---|
| Benchmarks | 27 QLDPC instances across BB/GB, LP, and TN families | Expose easy, moderate, and transition-region behavior |
| Solvers | 21 tools spanning SAT, SMT, MaxSAT, and non-SAT baselines | Compare paradigms rather than one solver line |
| Configurations | 46 representative configurations in the full heatmap | Separate solver-family effects from encoding effects |
| Timeouts | 3-minute pre-evaluation, 2-hour main evaluation | Filter dominated encodings before large-scale comparison |
| Encoding | Solved | Timeout | Fastest |
|---|---|---|---|
| Sequential-counter | 218 | 79 | 133 |
| Totalizer | 224 | 73 | 92 |
| Binary | 151 | 146 | 0 |
Binary encoding is empirically dominated, so the main experiments focus on sequential-counter and totalizer as the competitive formulations.
The paper’s central claim is that the practical bottleneck is not parity reasoning alone. The harder part is handling cardinality constraints and proving optimality.
Even though the formulation is rich in XOR constraints, native XOR-aware SAT did not show a systematic advantage across the benchmark suite.
This challenges the intuition that “more XOR support” should automatically translate into better QLDPC distance solving.
This visual is a presentation summary of the paper’s empirical conclusion, not a literal chart from the paper.
Easy instances make many solvers look good. The informative cases are the transition-region benchmarks, where some methods still solve and others start timing out.
Branch-and-bound MaxSAT, MIP, and a few strong exact baselines.
Conventional SAT, SMT, XOR-aware SAT, and unsat-core-guided MaxSAT.
Not all MaxSAT solvers behave alike. Solver architecture itself is a major explanatory variable.
Finding a low-weight logical operator and certifying optimality are computationally different tasks.
The paper argues these transition-region instances are the most discriminative for future solver comparisons.
The hardest part is tied to cardinality management and optimality certification.
Especially branch-and-bound MaxSAT and strong MIP-based baselines.
Branch-and-bound and unsat-core-guided approaches behave qualitatively differently.
Transition-region instances are far more informative than uniformly easy or hopeless ones.
For exact QLDPC distance computation, solver success is driven less by parity reasoning than by how well the method handles optimization structure, cardinality constraints, and proof of optimality.
For a public-facing website version, we can later shorten the table-heavy slides and keep this fuller version as the seminar deck.