Iranian Society of Cryptology The ISC International Journal of Information Security 2008-2045 Articles in Press 2026 05 01 Evaluating CNF/SMT Encodings for SAT-Based Differential Cryptanalysis of Lightweight Block Ciphers 242936 10.22042/isecure.2026.242936 EN Marzieh Vahid Dastjerdi Department of Mathematics, Institute for Advanced Studies in Basic Sciences (IASBS), Zanjan 45137-66731, Iran Computer Science Group, Research Center for Development of Advanced Technologies (RCDAT), Tehran, Iran Majid Rahimi Computer Science Group, Research Center for Development of Advanced Technologies (RCDAT), Tehran, Iran Iman Mirzaali Mazandarani Computer Science Group, Research Center for Development of Advanced Technologies (RCDAT), Tehran, Iran CPS2 Lab, Department of Communication, Faculty of Electrical Engineering, Shahid Rajaee Teacher Training University, Tehran, Iran Sadegh Sadeghi Department of Mathematics, Institute for Advanced Studies in Basic Sciences (IASBS), Zanjan 45137-66731, Iran Journal Article 2025 10 01 This study evaluates three encoding methods for automated differential cryptanalysis: (1) SMT formulations (using CVC), (2) standard CNF, and (3) size-optimised CNF (via Logic Friday). We assess these using four SAT/SMT solver types: single-core (CryptoMiniSat-v5, CaDiCaL), multicore (Treengeling), and massively parallel Mallob—novel to cryptanalysis. Encoding-solver combinations are tested on seven lightweight block ciphers representing distinct design philosophies: SPECK-32 and CHAM-64 (ARX structure), SIMON-32 (AND-RX structure), PRESENT, GIFT-128, and MIDORI-64 (4-bit S-box in SPN structure), and LBLOCK (Feistel structure). For each cipher, SAT/SMT instances targeting specific rounds and differential weights were generated, with wall-clock solving time, parallel efficiency, and modelling effort recorded. Our results establish criteria for optimal encoding-solver pairings that strike a balance between modelling simplicity and computational performance. Crucially, Mallob emerges as the state-of-the-art framework for large-scale automated differential cryptanalysis. https://www.isecure-journal.com/article_242936_0ccd54a0135b72b482ed5d245b6180f2.pdf