Options
IGMaxHS - An Incremental MaxSAT Solver with Support for XOR Clauses
Citation Link: https://doi.org/10.15480/882.13563
Publikationstyp
Conference Paper not in Proceedings
Date Issued
2024-10-21
Sprache
English
Author(s)
TORE-DOI
Citation
15th International Workshop on Pragmatics of SAT, PoS 2024
Contribution to Conference
ArXiv ID
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.
Subjects
Incremental MaxSAT
XOR Constraints
Fuzz Testing
DDC Class
003: Systems Theory
Publication version
publishedVersion
Loading...
Name
2410.15897v1.pdf
Type
Main Article
Size
798.77 KB
Format
Adobe PDF