A Study of the Parallelization of Hybrid SAT Solver using CUDA

Taeill Yoo, Sangpil Kim, Yongjin Yeom, Jusung Kang
Department of Mathematics, Cryptography and Information Security Institute, Kookmin University, Seoul, Republic of Korea
Advanced Science and Technology Letters (ASTL), Vol.48, pp.19-24, 2014


   title={A Study of the Parallelization of Hybrid SAT Solver using CUDA},

   author={Yoo, Taeill and Kim, Sangpil and Yeom, Yongjin and Kang, Jusung},



Download Download (PDF)   View View   Source Source   



SAT solver is an algorithm for finding the solution of a given problem by using CNF (Conjunctive Normal Form). Recently SAT solver studies have focused on the aspect of cryptography. The purpose of this paper is to construct the framework of a parallel SAT solver that can be applied to cryptanalysis. First, we transform an algebraic equation of the reduced AES(Advanced Encryption Standard) into CNF and then, analyze its properties and design a parallel SAT solver for cryptanalysis. Second, we implement a hybrid SAT solver that combines a complete SAT solver and an incomplete SAT solver. minisat-2.2.0 is used by the complete SAT solver and greedy SAT, by the incomplete SAT solver. Finally, we parallelize the hybrid SAT solver using NVIDIA’s CUDA to analyze the CNF of the reduced AES. In conclusion, we have constructed a framework that can develop various SAT solver applied parallelization strategies by using CUDA in the hybrid SAT solver. We will apply to this method for CNFs of small-scale AESs.
No votes yet.
Please wait...

* * *

* * *

HGPU group © 2010-2018 hgpu.org

All rights belong to the respective authors

Contact us: