ГлавнаяАрхивО GPU-реализации ограниченной версии нехронологического алгоритма DPLL

О GPU-реализации ограниченной версии нехронологического алгоритма DPLL | Прикладная дискретная математика. 2013. № 6 (Приложение).

Описан новый решатель ngsat, предназначенный для решения SAT-задач на GPU (Graphic Processor Unit). Данный решатель основан на ограниченном варианте нехронологического DPLL без процедуры Clause Learning; в нём использованы специальные приемы, позволяющие повысить эффективность исполнения DPLL на SIMD-архитектуре. Приводятся результаты тестирования ngsat на задачах поиска систем ортогональных латинских квадратов.
  • Title О GPU-реализации ограниченной версии нехронологического алгоритма DPLL
  • Headline О GPU-реализации ограниченной версии нехронологического алгоритма DPLL
  • Publesher Tomask State UniversityTomsk State University
  • Issue Прикладная дискретная математика 6 (Приложение)
  • Date:
  • DOI
Ключевые слова
GPU, алгоритм DPLL, SAT, параллельные вычислительные архитектуры, CUDA, SIMD, GPU, DPLL algorithm, SAT, parallel computer architectures, CUDA, SIMD
Авторы
Ссылки
Беспалов Д. В., Булавинцев В. Г., Семенов А. А. Использование графических ускорителей в решении задач криптоанализа // Прикладная дискретная математика. Приложение. 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/
О GPU-реализации ограниченной версии нехронологического алгоритма DPLL | Прикладная дискретная математика. 2013. № 6 (Приложение).
О GPU-реализации ограниченной версии нехронологического алгоритма DPLL | Прикладная дискретная математика. 2013. № 6 (Приложение).
Полнотекстовая версия