Тема выпускной квалификационной работы: «Исследование и оптимизация решения задачи выполнимости булевых формул на базе реконфигурируемых аппаратных ускорителей». Данная работа посвящена реализации на базе реконфигурируемого аппаратного ускорителя, используя стандарт OpenCL, решения задачи выполнимости булевых формул (задачи SAT), исследованию существующих вариантов реализации и их оптимизации с целью повышения эффективности. Задачи, которые решались в ходе исследования: проведение анализа существующих алгоритмов для решения задачи SAT, архитектурных особенностей современных реконфигурируемых ускорителей, возможностей инструментальных средств компании Xilinx, существующих аппаратных решений на базе SIMD и FPGA ускорителей; реализация решателя задачи SAT на базе реконфигурируемого аппаратного ускорителя Alveo компании Xilinx; проведение исследования, сравнительного анализа и оптимизации реализованного решателя, а также проведение сравнительного анализа созданного решателя с существующими реализациями решателя. При проведении исследования были использованы: имитационное моделирование с использованием возможностей пакета SDAccel компании Xilinx и сравнительный анализ результатов моделирования. В результате был реализован решатель задачи SAT и было произведено сравнение результатов моделирования, показавшее повышение эффективности решения задачи SAT, по сравнению с рассмотренными существующими решениями.

The subject of the graduate qualification work is “Research and optimization of the solution of the feasibility problem for Boolean formulas based on reconfigurable hardware accelerators”. The given work is devoted to the implementation on the basis of a reconfigurable hardware accelerator, using the OpenCL standard, to solve the feasibility problem of Boolean formulas (SAT problems), to study existing implementation options and their optimization in order to increase efficiency. Tasks that were solved during the study: analysis of existing algorithms to solve the SAT problem, architectural features of modern reconfigurable accelerators, the capabilities of Xilinx tools, existing hardware solutions based on SIMD and FPGA accelerators; implementation of the SAT problem solver based on Xilinx reconfigurable hardware accelerator Alveo; conducting research, comparative analysis and optimization of the implemented solver, as well as conducting a comparative analysis of the created solver with existing solver implementations. During the study, the following were used: simulation using the capabilities of the Xilinx SDAccel package and a comparative analysis of the simulation results. As a result, the SAT problem solver was implemented and the simulation results were compared, which showed an increase in the efficiency of solving the SAT problem, compared with the existing solutions considered.