A Study of the Parallelization of Hybrid SAT Solver using CUDA
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
@article{yoo2014study,
title={A Study of the Parallelization of Hybrid SAT Solver using CUDA},
author={Yoo, Taeill and Kim, Sangpil and Yeom, Yongjin and Kang, Jusung},
year={2014}
}
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.
May 10, 2014 by hgpu
