Geodesic
GPU-based implementation of DPLL algorithm with limited non-chronological backtracking
Prikladnaya Diskretnaya Matematika. Supplement, no. 6 (2013), pp. 111-112

Voir la notice de l'article provenant de la source Math-Net.Ru

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.
Keywords: GPU, DPLL algorithm, SAT, parallel computer architectures, CUDA, SIMD. 
@article{PDMA_2013_6_a49,
     author = {V. G. Bulavintsev and A. A. Semenov},
     title = {GPU-based implementation of {DPLL} algorithm with limited non-chronological backtracking},
     journal = {Prikladnaya Diskretnaya Matematika. Supplement},
     pages = {111--112},
     publisher = {mathdoc},
     number = {6},
     year = {2013},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/PDMA_2013_6_a49/}
}
TY  - JOUR
AU  - V. G. Bulavintsev
AU  - A. A. Semenov
TI  - GPU-based implementation of DPLL algorithm with limited non-chronological backtracking
JO  - Prikladnaya Diskretnaya Matematika. Supplement
PY  - 2013
SP  - 111
EP  - 112
IS  - 6
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/PDMA_2013_6_a49/
LA  - ru
ID  - PDMA_2013_6_a49
ER  - 
%0 Journal Article
%A V. G. Bulavintsev
%A A. A. Semenov
%T GPU-based implementation of DPLL algorithm with limited non-chronological backtracking
%J Prikladnaya Diskretnaya Matematika. Supplement
%D 2013
%P 111-112
%N 6
%I mathdoc
%U http://geodesic.mathdoc.fr/item/PDMA_2013_6_a49/
%G ru
%F PDMA_2013_6_a49
V. G. Bulavintsev; A. A. Semenov. GPU-based implementation of DPLL algorithm with limited non-chronological backtracking. Prikladnaya Diskretnaya Matematika. Supplement, no. 6 (2013), pp. 111-112. http://geodesic.mathdoc.fr/item/PDMA_2013_6_a49/