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.