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

Описан новый решатель ngsat, предназначенный для решения SAT-задач на GPU (Graphic Processor Unit). Данный решатель основан на ограниченном варианте нехронологического DPLL без процедуры Clause Learning; в нём использованы специальные приемы, позволяющие повысить эффективность исполнения DPLL на SIMD-архитектуре. Приводятся результаты тестирования ngsat на задачах поиска систем ортогональных латинских квадратов.