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.
| Identifer | oai:union.ndltd.org:nusl.cz/oai:invenio.nusl.cz:236336 |
| Date | January 2013 |
| Creators | Izrael, Petr |
| Contributors | Šimek, Václav, Jaroš, Jiří |
| Publisher | Vysoké učení technické v Brně. Fakulta informačních technologií |
| Source Sets | Czech ETDs |
| Language | Czech |
| Detected Language | English |
| Type | info:eu-repo/semantics/masterThesis |
| Rights | info:eu-repo/semantics/restrictedAccess |
Page generated in 0.002 seconds