Публикация научных работ

05.00.00 Технические науки

ИСПОЛЬЗОВАНИЕ МНОГОЯДЕРНЫХ УСКОРИТЕЛЕЙ ДЛЯ РЕШЕНИЯ ЗАДАЧИ ПРОПОЗИЦИОНАЛЬНОЙ ВЫПОЛНИМОСТИ

Кирюшин Н.К., Михалев И.В.

Email: Адрес электронной почты защищен от спам-ботов. Для просмотра адреса в вашем браузере должен быть включен Javascript.

Кирюшин Никита Константинович – магистрант;

Михалев Илья Викторович – магистрант,

кафедра вычислительной техники,

Национальный исследовательский университет

Московский институт электронной техники,

г. Москва

Аннотация: проведено экспериментальное исследование применимости различных многоядерных аппаратных ускорителей для решения задачи выполнимости булевых формул. Для проведения экспериментальных исследований разработаны решатели, учитывающие особенности исследуемых аппаратных платформ. В данной работе рассматривалось применение графических ускорителей и универсальных многоядерных ускорителей Intel Xeon Phi. Представленные результаты дают понятие об алгоритмах, применимых для решения задачи выполнимости булевых формул с использованием многоядерных аппаратных ускорителей, а также о группах задач, относящихся к задаче выполнимости булевых формул, для которых использование многоядерных ускорителей обосновано.

Ключевые слова: пропозициональная выполнимость, выполнимость булевых формул, многоядерные ускорители, графические ускорители, DPLL, SLS, GPU, CUDA, Xeon Phi.

USING MANYCORE HARDWARE ACCELERATORS FOR BOOLEAN SATISFIABILITY SOLVING

Kiryushin N.K., Mikhalev I.V.

Kiryushin Nikita Konstantinovich – Undergraduate;

Mikhalev Ilya Viktorovich – Undergraduate,

COMPUTER ENGINEERING DEPARTMENT

NATIONAL RESEARCH UNIVERSITY OF ELECTRONIC TECHNOLOG,Y

MOSCOW

Abstract: аn experimental study of the applicability of various manycore hardware accelerators to solve Boolean satisfiability (SAT) problem is carried out. Solvers, taking into account features of researched hardware platforms are developed to be used in the experimental researches. In this paper, we considered the use of GPU and Intel Xeon Phi coprocessors. The presented results give an idea of algorithms that are applicable for solving the problem of satisfiability of Boolean formulas using multi-core hardware accelerators, as well as groups of problems related to the problem of satisfiability of Boolean formulas for which the use of manycore accelerators is justified.

Keywords: propositional satisfiability, Boolean satisfiability, manycore coprocessors, graphic processing unit, DPLL, SLS, GPU, CUDA, Xeon Phi.

Список литературы / References

1. Davis M., Logemann G., Loveland D. A Machine Program for Theorem-proving. Commun. ACM 5(7) (July 1962). Р. 394-397.
2. Selman В., Levesque Н. and Mitchell D.G. A new method for solving hard satisfiability problems. In 10th National Conference on Artificial Intelligence, pages 440–446. AAAI Press / The MIT Press. Menlo Park. CA, 1992.
3. CUDA Toolkit Documentation v8.0 — NVIDIA corp., 2017. [Электронный ресурс]. Режим доступа: http://docs.nvidia.com/cuda/ (дата обращения: 03.06.2017).
4. Costa C. Parallelization of SAT Algorithms on GPUs. Technical report, Instituto Superior T´ecnico, Lisboa, Portugal (Feb 2013).
5. The Glucose SAT Solver—LaBRI. [Электронный ресурс]. Режим доступа: http://www.labri.fr/perso/lsimon/glucose/ (дата обращения: 03.06.2017).
6. Intel Xeon Phi X100 Family Coprocessor. The Architecture Intel Software. [Электронный ресурс]. Режим доступа: https://software.intel.com/en-us/articles/intel-xeon-phi-coprocessor-codename-knights-corner/ (дата обращения: 03.06.2017).

Ссылка для цитирования данной статьи

		Тип лицензии на данную статью – CC BY 4.0. Это значит, что Вы можете свободно цитировать данную статью на любом носителе и в любом формате при указании авторства.
Кирюшин Н.К., Михалев И.В. ИСПОЛЬЗОВАНИЕ МНОГОЯДЕРНЫХ УСКОРИТЕЛЕЙ ДЛЯ РЕШЕНИЯ ЗАДАЧИ ПРОПОЗИЦИОНАЛЬНОЙ ВЫПОЛНИМОСТИ // Проблемы современной науки и образования  №22 (104), 2017. - С. {см. журнал}.

Поделитесь данной статьей, повысьте свой научный статус в социальных сетях