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/

[1] Bespalov D. V., Bulavintsev V. G., Semenov A. A., “Ispolzovanie graficheskikh uskoritelei v reshenii zadach kriptoanaliza”, Prikladnaya diskretnaya matematika. Prilozhenie, 2010, no. 3, 86–87 | MR

[2] Biere A., Heule M., van Maaren H., Walsh T. (eds.), Handbook of satisfiability, IOS Press, 2009 | Zbl

[3] Een N., Sorensson N., “An extensible SAT-solver”, LNCS, 2919, 2003, 502–518

[4] Marques-Silva J. P., Sakallah K. A., “GRASP: A search algorithm for propositional satisfiability”, IEEE Trans. Comp., 48:5 (1999), 506–521 | DOI | MR

[5] Moskewicz M. W. et al., “Chaff: Engineering an efficient SAT solver”, Proc. 38th Design Automation Conference (Las Vegas, NV, USA), ACM, 2001, 530–535

[6] Beame P., Kautz H. A., Sabharwal A., “Towards understanding and harnessing the potential of clause learning”, J. Artif. Intell. Res. (JAIR), 22 (2004), 319–351 | MR | Zbl

[7] Zhang H., “Combinatorial designs by SAT solvers”, Handbook of satisfiability, IOS Press, 2009, 533–568

[8] http://minisat.se/