|
| |
|
|
SAT Solver akcelerovaný pomocí GPU
Izrael, Petr ; Šimek, Václav (oponent) ; Jaroš, Jiří (vedoucí práce)
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.
|
|
| |
|
|
SAT Solver akcelerovaný pomocí GPU
Izrael, Petr ; Šimek, Václav (oponent) ; Jaroš, Jiří (vedoucí práce)
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.
|
host ::
RSS.