Learning with Enumeration: Neural-Guided SAT Framework for Cryptographic Key Recovery

Boolean satisfiability (SAT) provides a foundation tool for cryptographic key recovery by encoding ciphers into CNF or ANF representations. However, heuristic solvers and their neural-enhanced variants often degrade significantly on cryptographic instances due to pronounced structural symmetry, a large number of intermediate variables, and complex algebraic dependencies. Existing neural approaches—ranging from end-to-end prediction to solver-integrated heuristics—face challenges in scalability, assignment accuracy, or computational efficiency. In this paper, we propose a unified neural-guided enumerative SAT framework for cryptographic key recovery. It performs a single forward neural guidance to identify a subset of $k$ critical variables, followed by enumeration over their assignments before invoking a heuristic SAT solver. This design effectively reduces the combinatorial search space while keeping neural overhead minimal. We further introduce a taxonomy of neural guidance across data and model capability regimes, including supervised selection with cryptographic priors, uncertainty-driven selection with assignment prediction, and robust fallback strategies using the model trained on general SAT datasets. Experiments on 10 SAT solvers and 2 cube-and-conquer strategies over SAT4CryptoBench and SAT Competition benchmarks demonstrate up to $5\times$ speedup and approximately 2× average improvement on cryptographic instances, while maintaining better performance on general SAT datasets. These results highlight the effectiveness and generalization of this framework, illustrating its potential to bridge machine learning and SAT solving in cryptanalysis tasks.