SAT-Based Syndrome Decoding and Low-Weight Codewords

Abstract The Syndrome Decoding Problem (SDP) for a binary linear code consists in finding a particular solution to an underdetermined linear system defined over the finite field of two elements, such that the Hamming weight of this solution is smaller than a given bound. In this paper, we explore several satisfiability-based models for solving this problem relying on XNF and classical CNF representations. We compare these approaches to assess their efficiency in solving SDP. Furthermore, we also introduce a Maximum Satisfiability (MaxSAT) model of the Low-Weight Codeword Problem (LWCP), which consists in finding a word with minimal Hamming weight in a given code. In particular, we introduce three MAX-SAT models for LWCP: an XNF model, which reuses the XOR constraints from the SDP formulations, and two CNF models, which are also based on the CNF formulations from SDP. For all three models, we add soft clauses to minimize the Hamming weight. Finally, we assess the models using state-of-the-art MaxSAT solvers, which apply different solving paradigms to compute optimal codeword weights.