Document Open Access Logo

Satisfiability for Large Weight Syndrome Decoding

Authors Carl Berton , Sami Cherif , Claire Delaplace

PDF

File

Thumbnail PDF
PDF
LIPIcs.CP.2026.5.pdf
  • Filesize: 0.85 MB
  • 17 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Constraint and logic programming
  • Security and privacy → Cryptography
Keywords
  • Large Weight Syndrome Decoding
  • Satisfiability
  • Cryptography

Metrics

Abstract

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.

Cite As Get BibTex

Carl Berton, Sami Cherif, and Claire Delaplace. Satisfiability for Large Weight Syndrome Decoding. In 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 379, pp. 5:1-5:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CP.2026.5

Author Details

Carl Berton
  • MIS UR 4290, Université de Picardie Jules Verne, Amiens, France
Sami Cherif
  • MIS UR 4290, Université de Picardie Jules Verne, Amiens, France
Claire Delaplace
  • MIS UR 4290, Université de Picardie Jules Verne, Amiens, France

Funding

This work is supported by the projects ANR-24-CE23-6126 (BforSAT) and 22-PECY-0010 (CRYPTANALYSE), funded by the French National Research Agency. It was also granted access to HPC resources of "Plateforme MatriCS" within University of Picardie Jules Verne, co-funded by the European Union with the European Regional Development Fund (FEDER) and the Hauts-De-France Regional Council.

Supplementary Materials

References

  1. Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, and Enric Rodríguez-Carbonell. Cardinality networks and their applications. In Oliver Kullmann, editor, SAT 2009, volume 5584 of LNCS, pages 167-180. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02777-2_18.
  2. Anja Becker, Antoine Joux, Alexander May, and Alexander Meurer. Decoding random binary linear codes in 2 n/20: How 1 + 1 = 0 improves information set decoding. In David Pointcheval and Thomas Johansson, editors, Advances in Cryptology - EUROCRYPT 2012 - 31st Annual International Conference on the Theory and Applications of Cryptographic Techniques, Cambridge, UK, April 15-19, 2012. Proceedings, volume 7237 of Lecture Notes in Computer Science, pages 520-536. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-29011-4_31.
  3. Elwyn R. Berlekamp. Algebraic coding theory. McGraw-Hill series in systems science. McGraw-Hill, 1968. URL: https://www.worldcat.org/oclc/00256659.
  4. Elwyn R. Berlekamp, Robert J. McEliece, and Henk C. A. van Tilborg. On the inherent intractability of certain coding problems (corresp.). IEEE Trans. Inf. Theory, 24(3):384-386, 1978. URL: https://doi.org/10.1109/TIT.1978.1055873.
  5. Carl Berton, Sami Cherif, and Claire Delaplace. Satisfiabilité pour le décodage par syndrome. In Journées Francophones de Programmation par Contraintes (JFPC 2025), Dijon, France, June 2025. URL: https://hal.science/hal-05208088.
  6. Carl Berton, Sami Cherif, and Claire Delaplace. Sat-based syndrome decoding and low-weight codewords. In Proceedings of 27th International Symposium on Formal Methods (FM 2026), Tokyo, Japan, 2026. To appear. Google Scholar
  7. Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, and Florian Pollitt. Cadical 2.0. In Arie Gurfinkel and Vijay Ganesh, editors, Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I, volume 14681 of Lecture Notes in Computer Science, pages 133-152. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-65627-9_7.
  8. Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA336.
  9. Rémi Bricout, André Chailloux, Thomas Debris-Alazard, and Matthieu Lequesne. Ternary syndrome decoding with large weight. In Kenneth G. Paterson and Douglas Stebila, editors, Selected Areas in Cryptography - SAC 2019 - 26th International Conference, Waterloo, ON, Canada, August 12-16, 2019, Revised Selected Papers, volume 11959 of Lecture Notes in Computer Science, pages 437-466. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-38471-5_18.
  10. Lily Chen, Lily Chen, Stephen Jordan, Yi-Kai Liu, Dustin Moody, Rene Peralta, Ray A Perlner, and Daniel Smith-Tone. Report on post-quantum cryptography, volume 12. US Department of Commerce, National Institute of Standards and Technology …, 2016. Google Scholar
  11. Stephen A. Cook. The complexity of theorem-proving procedures. In Michael A. Harrison, Ranan B. Banerji, and Jeffrey D. Ullman, editors, STOC 1971, pages 151-158. ACM, 1971. URL: https://doi.org/10.1145/800157.805047.
  12. Nicolas T. Courtois and Gregory V. Bard. Algebraic cryptanalysis of the data encryption standard. In Steven D. Galbraith, editor, Cryptography and Coding, 11th IMA International Conference, Cirencester, UK, December 18-20, 2007, Proceedings, volume 4887 of Lecture Notes in Computer Science, pages 152-169. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-77272-9_10.
  13. Joan Daemen and Vincent Rijmen. The Design of Rijndael: AES - The Advanced Encryption Standard. Information Security and Cryptography. Springer, 2002. URL: https://doi.org/10.1007/978-3-662-04722-4.
  14. Thomas Debris-Alazard, Nicolas Sendrier, and Jean-Pierre Tillich. Wave: A new code-based signature scheme. IACR Cryptol. ePrint Arch., page 996, 2018. URL: https://eprint.iacr.org/2018/996.
  15. Andre Esser and Emanuele Bellini. Syndrome decoding estimator. In Goichiro Hanaoka, Junji Shikata, and Yohei Watanabe, editors, IACR 2022, volume 13177 of LNCS, pages 112-141. Springer, 2022. URL: https://doi.org/10.1007/978-3-030-97121-2_5.
  16. Aarti Gupta, Malay K. Ganai, and Chao Wang. Sat-based verification methods and applications in hardware verification. In Marco Bernardo and Alessandro Cimatti, editors, SFM 2006, Advanced Lectures, volume 3965 of LNCS, pages 108-143. Springer, 2006. URL: https://doi.org/10.1007/11757283_5.
  17. Frédéric Lafitte, Jorge Nakahara Jr., and Dirk Van Heule. Applications of SAT solvers in cryptanalysis: Finding weak keys and preimages. J. Satisf. Boolean Model. Comput., 9(1):1-25, 2014. URL: https://doi.org/10.3233/SAT190099.
  18. Norbert Manthey, Tobias Philipp, and Peter Steinke. A more compact translation of pseudo-boolean constraints into CNF such that generalized arc consistency is maintained. In Carsten Lutz and Michael Thielscher, editors, KI 2014, volume 8736 of LNCS, pages 123-134. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-11206-0_13.
  19. R. J. McEliece. A Public-Key Cryptosystem Based On Algebraic Coding Theory. Deep Space Network Progress Report, 44:114-116, January 1978. Google Scholar
  20. Carlos Aguilar Melchor, Nicolas Aragon, Slim Bettaieb, Loıc Bidoux, Olivier Blazy, Jean-Christophe Deneuville, Philippe Gaborit, Edoardo Persichetti, Gilles Zémor, and IC Bourges. Hamming quasi-cyclic (hqc). NIST PQC Round, 2(4):13, 2018. Google Scholar
  21. Ilya Mironov and Lintao Zhang. Applications of SAT solvers to cryptanalysis of hash functions. In Armin Biere and Carla P. Gomes, editors, Theory and Applications of Satisfiability Testing - SAT 2006, 9th International Conference, Seattle, WA, USA, August 12-15, 2006, Proceedings, volume 4121 of Lecture Notes in Computer Science, pages 102-115. Springer, 2006. URL: https://doi.org/10.1007/11814948_13.
  22. Shintaro Narisada, Shusaku Uemura, Hiroki Okada, Hiroki Furue, Yusuke Aikawa, and Kazuhide Fukushima. Solving mceliece-1409 in one day - cryptanalysis with the improved BJMM algorithm. In Nicky Mouha and Nick Nikiforakis, editors, ISC 2024, volume 15258 of LNCS, pages 3-23. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-75764-8_1.
  23. Eugene Prange. The use of information sets in decoding cyclic codes. IRE Trans. Inf. Theory, 8(5):5-9, 1962. URL: https://doi.org/10.1109/TIT.1962.1057777.
  24. Jussi Rintanen. Planning and SAT. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 765-789. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA201003.
  25. Olivier Roussel and Vasco Manquinho. Pseudo-boolean and cardinality constraints. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability - Second Edition, Frontiers in Artificial Intelligence and Applications, pages 1087-1129. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA201012.
  26. Claude E. Shannon. A mathematical theory of communication. Bell Syst. Tech. J., 27(3):379-423, 1948. URL: https://doi.org/10.1002/J.1538-7305.1948.TB01338.X.
  27. Peter W. Shor. Polynomial-time algorithms for prime factorization and discrete logarithms on a quantum computer. SIAM Rev., 41(2):303-332, 1999. URL: https://doi.org/10.1137/S0036144598347011.
  28. João P. Marques Silva and Karem A. Sakallah. GRASP - a new search algorithm for satisfiability. In Rob A. Rutenbar and Ralph H. J. M. Otten, editors, ICCAD 1996, pages 220-227. IEEE Computer Society / ACM, 1996. URL: https://doi.org/10.1109/ICCAD.1996.569607.
  29. Mate Soos, Karsten Nohl, and Claude Castelluccia. Extending SAT solvers to cryptographic problems. In Oliver Kullmann, editor, SAT 2009, volume 5584 of LNCS, pages 244-257. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02777-2_24.
  30. Jacques Stern. A method for finding codewords of small weight. In Gérard D. Cohen and Jacques Wolfmann, editors, Coding Theory and Applications, 3rd International Colloquium, Toulon, France, November 2-4, 1988, Proceedings, volume 388 of Lecture Notes in Computer Science, pages 106-113. Springer, 1988. URL: https://doi.org/10.1007/BFB0019850.
  31. Monika Trimoska, Gilles Dequen, and Sorina Ionica. Logical cryptanalysis with wdsat. In Chu-Min Li and Felip Manyà, editors, Theory and Applications of Satisfiability Testing - SAT 2021 - 24th International Conference, Barcelona, Spain, July 5-9, 2021, Proceedings, volume 12831 of Lecture Notes in Computer Science, pages 545-561. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-80223-3_37.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact