GPU-based implementation of DPLL algorithm with limited non-chronological backtracking
A new GPU-based SAT solver named ngsat is presented. The solver employs DPLL algorithm with limited version of non-chronological backtracking without Clause Learning. Some new techniques are developed and applied to increase the effectiveness of DPLL algorithm on SIMD. Ngsat's performance is demonstrated in application to the problems of search for pairs of orthogonal Latin squares.
Download file
Counter downloads: 266
Keywords
GPU, алгоритм DPLL, SAT, параллельные вычислительные архитектуры, CUDA, SIMD, GPU, DPLL algorithm, SAT, parallel computer architectures, CUDA, SIMDAuthors
| Name | Organization | |
| Bulavintsev V.G. | Institute of System Dynamics and Control Theory, Siberian Branch of the Russian Academy of Sciences (Irkutsk) | ichorid@mail.ru |
| Semenov A. A. | Institute of System Dynamics and Control Theory, Siberian Branch of the Russian Academy of Sciences (Irkutsk) | biclop.rambler@yandex.ru |
References
Беспалов Д. В., Булавинцев В. Г., Семенов А. А. Использование графических ускорителей в решении задач криптоанализа // Прикладная дискретная математика. Приложение. 2010. №3. С. 86-87.
Biere A., Heule M., van Maaren H., and Walsh T. (eds.). Handbook of satisfiability. IOS Press, 2009.
Een N. and Sorensson N. An extensible SAT-solver // LNCS. 2003. V. 2919. P. 502-518.
Marques-Silva J. P. and Sakallah K. A. GRASP: A search algorithm for propositional satisfiability // IEEE Trans. Comp. 1999. V.48. No. 5. P. 506-521.
Moskewicz M. W. et al. Chaff: Engineering an efficient SAT solver // Proc. 38th Design Automation Conference. Las Vegas, NV, USA: ACM, 2001. P. 530-535.
Beame P., Kautz H. A., and Sabharwal A. Towards understanding and harnessing the potential of clause learning // J. Artif. Intell. Res. (JAIR). 2004. V.22. P. 319-351.
Zhang H. Combinatorial designs by SAT solvers // Handbook of satisfiability. IOS Press, 2009. P. 533-568.
http://minisat.se/
