<div class="csl-bib-body">
<div class="csl-entry">Zisser, M. (2018). <i>Solving the #SAT problem on the GPU with dynamic programming and OpenCL</i> [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2018.52062</div>
</div>
-
dc.identifier.uri
https://doi.org/10.34726/hss.2018.52062
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/1825
-
dc.description.abstract
null
de
dc.description.abstract
There are many computational hard problems in computer science and a variety of these problems can be expressed via Boolean formulas. For some of these problems, the number of satisfying assignments can be directly linked to the solution. The task to compute the number of solutions of a Boolean formula is called the #SAT problem. Algorithms in artificial intelligence and machine learning tasks have profited from the massive parallelism provided by Graphic Processing Units (GPUs). However many current #SAT solvers rely on techniques from Satisfiability solving or approximate solving based on sampling of the search space. A central method for solving the Satisfiability problem is Conflict Driven Clause Learning (CDCL), but CDCL contains parts which are hard to or not parallelizable at all. CDCL does not work well on the GPU since parallelization on the GPU requires an algorithm with many similar independent steps. Dynamic Programming (DP) on tree decompositions on the other hand parallelizes well as we can execute many similar operations which are independent from another. For DP we need tree decompositions with a sufficiently small width. In the course of this thesis we developed gpusat, a #SAT solver which is based on dynamic programming on tree decompositions with OpenCL, an open standard that can be used to parallelize tasks on the GPU. We use tree decompositions of the primal, incidence and dual graph as base for our dynamic programming algorithms. gpusat is also able to solve Weighted Model Counting (WMC) where a weight is assigned to every literal and the weight of a solution is the product of its literal weights. To compare gpusat with other solvers we collected #SAT and WMC instances from different sources, and generated tree decompositions of the primal, incidence and dual graph for each of these instances. Then we compared the runtime of gpusat with other state of the art #SAT and WMC solvers on our instances. To get a better understanding of our benchmark set we also generated an overview of the tree width for our benchmark instances. Our experiments have shown that gpusat is competitive with other solvers for a tree width of up to 30. We were also able to solve some instances with a tree width of up to 45. About half of the instances had a width of 30 or below.
en
dc.language
English
-
dc.language.iso
en
-
dc.rights.uri
http://rightsstatements.org/vocab/InC/1.0/
-
dc.subject
Propositional Logic
de
dc.subject
#SAT
de
dc.subject
Dynamic Programming
de
dc.subject
Tree Decompositions
de
dc.subject
GPU
de
dc.subject
Propositional Logic
en
dc.subject
#SAT
en
dc.subject
Dynamic Programming
en
dc.subject
Tree Decompositions
en
dc.subject
GPU
en
dc.title
Solving the #SAT problem on the GPU with dynamic programming and OpenCL
en
dc.type
Thesis
en
dc.type
Hochschulschrift
de
dc.rights.license
In Copyright
en
dc.rights.license
Urheberrechtsschutz
de
dc.identifier.doi
10.34726/hss.2018.52062
-
dc.contributor.affiliation
TU Wien, Österreich
-
dc.rights.holder
Markus Zisser
-
dc.publisher.place
Wien
-
tuw.version
vor
-
tuw.thesisinformation
Technische Universität Wien
-
dc.contributor.assistant
Fichte, Johannes Klaus
-
dc.contributor.assistant
Hecher, Markus
-
tuw.publication.orgunit
E184 - Institut für Informationssysteme
-
dc.type.qualificationlevel
Diploma
-
dc.identifier.libraryid
AC15055950
-
dc.description.numberOfPages
85
-
dc.identifier.urn
urn:nbn:at:at-ubtuw:1-109782
-
dc.thesistype
Diplomarbeit
de
dc.thesistype
Diploma Thesis
en
dc.rights.identifier
In Copyright
en
dc.rights.identifier
Urheberrechtsschutz
de
tuw.advisor.staffStatus
staff
-
tuw.assistant.staffStatus
staff
-
tuw.assistant.staffStatus
staff
-
tuw.assistant.orcid
0000-0002-8681-7470
-
tuw.assistant.orcid
0000-0003-0131-6771
-
item.languageiso639-1
en
-
item.mimetype
application/pdf
-
item.openairecristype
http://purl.org/coar/resource_type/c_bdcc
-
item.fulltext
with Fulltext
-
item.openairetype
master thesis
-
item.grantfulltext
open
-
item.openaccessfulltext
Open Access
-
item.cerifentitytype
Publications
-
crisitem.author.dept
E192-02 - Forschungsbereich Databases and Artificial Intelligence