IGMaxHS -- An Incremental MaxSAT Solver with Support for XOR Clauses

TL;DR

IGMaxHS is a novel incremental MaxSAT solver that supports XOR constraints, improving error correction in quantum computing and outperforming existing solvers in fuzz testing and quantum code decoding.

Contribution

We introduce IGMaxHS, a MaxSAT solver supporting XOR constraints with fewer restrictions, extending the incremental API, and demonstrating its effectiveness in quantum error correction.

Findings

IGMaxHS outperforms other solvers in fuzz testing with 10,000 instances.

It is capable of decoding quantum color codes in simulation.

IGMaxHS is the only solver with no incorrect verdicts or invalid models in tests.

Abstract

Recently, a novel, MaxSAT-based method for error correction in quantum computing has been proposed that requires both incremental MaxSAT solving capabilities and support for XOR constraints, but no dedicated MaxSAT solver fulfilling these criteria existed yet. We alleviate that and introduce IGMaxHS, which is based on the existing solvers iMaxHS and GaussMaxHS, but poses fewer restrictions on the XOR constraints than GaussMaxHS. IGMaxHS is fuzz tested with xwcnfuzz, an extension of wcnfuzz that can directly output XOR constraints. As a result, IGMaxHS is the only solver that reported neither incorrect unsatisfiability verdicts nor invalid models nor incoherent cost model combinations in a final fuzz testing comparison of all three solvers with 10000 instances. We detail the steps required for implementing Gaussian elimination on XOR constraints in CDCL SAT solvers, and extend the recently proposed re-entrant incremental MaxSAT solver application program interface to allow for incremental addition of XOR constraints. Finally, we show that IGMaxHS is capable of decoding quantum color codes through simulation with the Munich Quantum Toolkit.