The Large Weight Syndrome Decoding problem LWSD is a fundamental problem in coding theory. It consists in determining whether a given linear code admits a high Hamming weight vector associated with a specific syndrome. LWSD is a variant of the classical syndrome decoding problem, which conversely seeks a low Hamming weight solution for a linear system defined over the binary field 𝔽₂. In this paper, we investigate a generalization of this problem to the case of a prime finite field 𝔽_Z, referred to as LWZSD. We propose several models using Boolean Satisfiability (SAT) formulas and compare the efficiency of our approaches using state-of-the-art solvers.

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.

We present a new variant of the LLL lattice reduction algorithm, inspired by Lagrange notion of pair-wise reduction, called L4. Similar to LLL, our algorithm is polynomial in the dimension of the input lattice, as well as in \(\log M\), where \(M\) is an upper-bound on the norm of the longest vector of the input basis. We experimentally compared the norm of the first basis vector obtained with LLL and L4 up to dimension 200. On average we obtain vectors that are up to 16% shorter. We also used our algorithm as a pre-processing step for the BKZ lattice reduction algorithm with blocksize 24. In practice, up to dimension 140, this allows us to reduce the norm of the shortest basis vector on average by 3%, while the runtime does not significantly increases. In 10% of our tests, the whole process was even faster.