Original title: SAT Solver akcelerovaný pomocí GPU
Translated title: GPU Accelerated SAT Solver
Authors: Izrael, Petr ; Šimek, Václav (referee) ; Jaroš, Jiří (advisor)
Document type: Master’s theses
Year: 2013
Language: cze
Publisher: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstract: [cze] [eng]
Práce se zabývá návrhem a implementací kompletního SAT solveru akcelerovaného na GPU. V první části práce je popsána architektura grafických karet a možnosti platformy CUDA. Následuje popis algoritmů a technik pro řešení problému booleovské splnitelnosti (SAT problému). Je představena zejména rodina kompletních algoritmů založených na DPLL. Právě varianta DPLL, známa jako 3SAT-DC je kompletně převedena na GPU. Práce popisuje problémy s tímto převodem spojené, stejně jako několik optimalizací a analýz. Velkým problémem je nemožnost využít v paralelním prostředí mnohé sofistikované metody známé ze sekvenčních solverů. Řešení bylo porovnáno s obdobným algoritmem implementovaným pro CPU a bylo ukázáno, že může být až 21x rychlejší. Uvedeny jsou i návrhy, jak algoritmus dále rozšířit a akcelerovat. This thesis is concerned with design and implementation of a complete SAT solver accelerated on GPU. The achitecture of modern graphics cards is described as well as the CUDA platform and a list of common algorithms used for solving the boolean satisfiability problem (the SAT problem). The presented solution is based on the 3-SAT DC alogirthm, which belongs to the family of well-known DPLL based algorithms. This work describes problems encountered during the design and implementation. The resulting application was then analyzed and optimized. The presented solver cannot compete with state of the art solvers, but proves that it can be up to 21x faster than an equivalent sequential version. Unfortunately, the current implementation can only handle formulas of a limited size. Suggestions on further improvements are given in final sections.
Keywords: CUDA; DPLL; GPGPU; GPU; SAT; CUDA; DPLL; GPGPU; GPU; SAT

Institution: Brno University of Technology (web)
Document availability information: Fulltext is available in the Brno University of Technology Digital Library.
Original record: http://hdl.handle.net/11012/53479

Permalink: http://www.nusl.cz/ntk/nusl-558155


The record appears in these collections:
Universities and colleges > Public universities > Brno University of Technology
Academic theses (ETDs) > Master’s theses